Loogle!

Result

Found 124 declarations mentioning Representation.IntertwiningMap.toLinearMap.

Representation.IntertwiningMap.toLinearMap 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (self : ρ.IntertwiningMap σ) : V →ₗ[A] W
Representation.IntertwiningMap.toLinearMap_id 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : (Representation.IntertwiningMap.id ρ).toLinearMap = LinearMap.id
Representation.Equiv.toLinearMap_refl 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid V] [Module A V] {ρ : Representation A G V} : (↑(Representation.Equiv.refl ρ)).toLinearMap = LinearMap.id
Representation.IntertwiningMap.toLinearMap_injective 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : Function.Injective fun f => f.toLinearMap
Representation.IntertwiningMap.ker_toSubmodule 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) : (Representation.IntertwiningMap.ker ρ σ f).toSubmodule = f.ker
Representation.IntertwiningMap.range_toSubmodule 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) : (Representation.IntertwiningMap.range ρ σ f).toSubmodule = f.range
Representation.IntertwiningMap.toFun_injective 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : Function.Injective fun f => f.toFun
Representation.IntertwiningMap.ext 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} {f g : ρ.IntertwiningMap σ} (h : f.toLinearMap = g.toLinearMap) : f = g
Representation.IntertwiningMap.ext_iff 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} {f g : ρ.IntertwiningMap σ} : f = g ↔ f.toLinearMap = g.toLinearMap
Representation.Equiv.left_inv 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (self : ρ.Equiv σ) : Function.LeftInverse self.invFun (↑self).toFun
Representation.Equiv.right_inv 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (self : ρ.Equiv σ) : Function.RightInverse self.invFun (↑self).toFun
Representation.IntertwiningMap.coe_toLinearMap 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) : ⇑f.toLinearMap = ⇑f
Representation.Equiv.toLinearEquiv_toLinearMap 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ) : ↑φ.toLinearEquiv = (↑φ).toLinearMap
Representation.IntertwiningMap.toLinearMap_apply 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) (v : V) : f.toLinearMap v = f v
Representation.IntertwiningMap.coe_eq_toLinearMap 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) {f : ρ.IntertwiningMap σ} : ↑f = f.toLinearMap
Representation.IntertwiningMap.zero_toLinearMap 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : Representation.IntertwiningMap.toLinearMap 0 = 0
Representation.Equiv.coe_toLinearMap 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ) : ⇑(↑φ).toLinearMap = ⇑φ
Representation.IntertwiningMap.toLinearMap_sum 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) {ι : Type u_6} (s : Finset ι) (f : ι → ρ.IntertwiningMap σ) : (∑ i ∈ s, f i).toLinearMap = ∑ i ∈ s, (f i).toLinearMap
Representation.Equiv.mk' 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (toIntertwiningMap : ρ.IntertwiningMap σ) (invFun : W → V) (left_inv : Function.LeftInverse invFun toIntertwiningMap.toFun := by intro; first | rfl | ext <;> rfl) (right_inv : Function.RightInverse invFun toIntertwiningMap.toFun := by intro; first | rfl | ext <;> rfl) : ρ.Equiv σ
Representation.Equiv.toLinearMap_symm 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ) : (↑φ.symm).toLinearMap = ↑φ.toLinearEquiv.symm
Representation.IntertwiningMap.comp_toLinearMap 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) (f : σ.IntertwiningMap τ) (g : ρ.IntertwiningMap σ) : (f.comp g).toLinearMap = f.toLinearMap ∘ₗ g.toLinearMap
Representation.Equiv.toLinearMap_trans 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (φ : ρ.Equiv σ) (ψ : σ.Equiv τ) : (↑(φ.trans ψ)).toLinearMap = (↑ψ).toLinearMap ∘ₗ (↑φ).toLinearMap
Representation.IntertwiningMap.add_toLinearMap 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f g : ρ.IntertwiningMap σ) : (f + g).toLinearMap = f.toLinearMap + g.toLinearMap
Representation.IntertwiningMap.toLinearMap_lTensor 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (f : ρ.IntertwiningMap σ) : (Representation.IntertwiningMap.lTensor τ f).toLinearMap = LinearMap.lTensor U f.toLinearMap
Representation.IntertwiningMap.toLinearMap_rTensor 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (f : σ.IntertwiningMap τ) : (Representation.IntertwiningMap.rTensor ρ f).toLinearMap = LinearMap.rTensor V f.toLinearMap
Representation.IntertwiningMap.coe_mul 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) (f g : ρ.IntertwiningMap ρ) : (f * g).toLinearMap = f.toLinearMap * g.toLinearMap
Representation.IntertwiningMap.sub_toLinearMap 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} [Semiring A] [Monoid G] {V : Type u_6} {W : Type u_7} [AddCommMonoid V] [AddCommGroup W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f g : ρ.IntertwiningMap σ) : (f - g).toLinearMap = f.toLinearMap - g.toLinearMap
Representation.IntertwiningMap.toLinearMap_smul 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (a : A) (f : ρ.IntertwiningMap σ) : (a • f).toLinearMap = a • f.toLinearMap
Representation.IntertwiningMap.toLinearMap_tensor 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} {P : Type u_6} [AddCommMonoid P] [Module A P] {π : Representation A G P} (f : ρ.IntertwiningMap σ) (g : τ.IntertwiningMap π) : (f.tensor g).toLinearMap = TensorProduct.map f.toLinearMap g.toLinearMap
Representation.IntertwiningMap.isIntertwining' 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (self : ρ.IntertwiningMap σ) (g : G) : self.toLinearMap ∘ₗ ρ g = σ g ∘ₗ self.toLinearMap
Representation.TensorProduct.toLinearMap_lid 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W] (σ : Representation A G W) : (↑(Representation.TensorProduct.lid A σ)).toLinearMap = ↑(TensorProduct.lid A W)
Representation.TensorProduct.toLinearMap_rid 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W] (σ : Representation A G W) : (↑(Representation.TensorProduct.rid A σ)).toLinearMap = ↑(TensorProduct.rid A W)
Representation.TensorProduct.toLinearMap_comm 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : (↑(Representation.TensorProduct.comm ρ σ)).toLinearMap = ↑(TensorProduct.comm A V W)
Representation.IntertwiningMap.toLinearMap_mk 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : V →ₗ[A] W) (h : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f) : { toLinearMap := f, isIntertwining' := h }.toLinearMap = f
Representation.IntertwiningMap.toLinearMapl_apply 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (self : ρ.IntertwiningMap σ) : (Representation.IntertwiningMap.toLinearMapl ρ σ) self = self.toLinearMap
Representation.IntertwiningMap.isIntertwining_assoc 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) {f : ρ.IntertwiningMap σ} (g : G) (l : U →ₗ[A] V) : f.toLinearMap ∘ₗ ρ g ∘ₗ l = σ g ∘ₗ f.toLinearMap ∘ₗ l
Representation.Equiv.toLinearMap_mk' 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (e : V ≃ₗ[A] W) (he : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e) : (↑(Representation.Equiv.mk e he)).toLinearMap = ↑e
Representation.TensorProduct.toLinearMap_assoc 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) : (↑(Representation.TensorProduct.assoc ρ σ τ)).toLinearMap = ↑(TensorProduct.assoc A V W U)
Representation.TensorProduct.assoc_symm_toLinearMap 📋 Mathlib.RepresentationTheory.Intertwining
{A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) : (↑(Representation.TensorProduct.assoc ρ σ τ).symm).toLinearMap = ↑(TensorProduct.assoc A V W U).symm
Representation.LinearizeMonoidal.η_toLinearMap 📋 Mathlib.RepresentationTheory.Action
(k : Type u) (G : Type v) [Monoid G] [Semiring k] : (Representation.LinearizeMonoidal.η k G).toLinearMap = ↑(MonoidAlgebra.uniqueLinearEquiv k PUnit.{u + 1})
Representation.linearizeMap_toLinearMap 📋 Mathlib.RepresentationTheory.Action
{k : Type u} {G : Type v} [Monoid G] [Semiring k] {X Y : Action (Type w) G} (f : X ⟶ Y) : (Representation.linearizeMap f).toLinearMap = MonoidAlgebra.mapDomainLinearMap k k ⇑(CategoryTheory.ConcreteCategory.hom f.hom)
Representation.LinearizeMonoidal.ε_toLinearMap 📋 Mathlib.RepresentationTheory.Action
(k : Type u) (G : Type v) [Monoid G] [Semiring k] : (Representation.LinearizeMonoidal.ε k G).toLinearMap = ↑(MonoidAlgebra.uniqueLinearEquiv k PUnit.{w + 1}).symm
Representation.LinearizeMonoidal.μ_toLinearMap 📋 Mathlib.RepresentationTheory.Action
{G : Type v} [Monoid G] (X Y : Action (Type w) G) {k : Type u} [CommSemiring k] : (Representation.LinearizeMonoidal.μ X Y).toLinearMap = ↑(MonoidAlgebra.tensorEquiv k)
Representation.ofMulActionSubsingletonEquivTrivial_apply 📋 Mathlib.RepresentationTheory.Equiv
{k : Type u} [Semiring k] {G : Type v} [Monoid G] (H : Type w) [Subsingleton H] [MulOneClass H] [MulAction G H] (f : MonoidAlgebra k H) : (↑(Representation.ofMulActionSubsingletonEquivTrivial k G H)).toLinearMap f = f.coeff 1
Representation.ofMulActionSubsingletonEquivTrivial_symm_apply 📋 Mathlib.RepresentationTheory.Equiv
{k : Type u} [Semiring k] {G : Type v} [Monoid G] (H : Type w) [Subsingleton H] [MulOneClass H] [MulAction G H] (r : k) : (↑(Representation.ofMulActionSubsingletonEquivTrivial k G H).symm).toLinearMap r = MonoidAlgebra.single 1 r
Representation.freeLift_toLinearMap 📋 Mathlib.RepresentationTheory.Equiv
{G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {k : Type u} [CommSemiring k] [Module k V] (σ : Representation k G V) {α : Type w'} (f : α → V) : (σ.freeLift f).toLinearMap = (Finsupp.linearCombination k fun x => (σ x.2) (f x.1)) ∘ₗ ↑(Finsupp.curryLinearEquiv k).symm ∘ₗ Finsupp.mapRange.linearMap ↑(MonoidAlgebra.coeffLinearEquiv k)
Rep.mkIso_hom_hom_toLinearMap 📋 Mathlib.RepresentationTheory.Rep.Basic
{k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (e : ρ.Equiv σ) : (Rep.Hom.hom (Rep.mkIso e).hom).toLinearMap = (↑e).toLinearMap
Rep.mkIso_inv_hom_toLinearMap 📋 Mathlib.RepresentationTheory.Rep.Basic
{k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (e : ρ.Equiv σ) : (Rep.Hom.hom (Rep.mkIso e).inv).toLinearMap = (↑e.symm).toLinearMap
Rep.hom_comp_toLinearMap 📋 Mathlib.RepresentationTheory.Rep.Basic
{k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B C : Rep.{w, u, v} k G} (f : A ⟶ B) (g : B ⟶ C) : (Rep.Hom.hom (CategoryTheory.CategoryStruct.comp f g)).toLinearMap = (Rep.Hom.hom g).toLinearMap ∘ₗ (Rep.Hom.hom f).toLinearMap
Rep.mkIso_hom_hom_apply 📋 Mathlib.RepresentationTheory.Rep.Basic
{k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (e : ρ.Equiv σ) (x : X) : (Rep.Hom.hom (Rep.mkIso e).hom) x = (↑e).toLinearMap x
Rep.forget₂_moduleCat_map 📋 Mathlib.RepresentationTheory.Rep.Basic
{k : Type u} {G : Type v} [Ring k] [Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B) : (CategoryTheory.forget₂ (Rep.{w, u, v} k G) (ModuleCat k)).map f = ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap
Rep.tensorHomEquiv_apply 📋 Mathlib.RepresentationTheory.Rep.Basic
{k : Type u} [CommRing k] {G : Type v} [Group G] (A B C : Rep.{u, u, v} k G) (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C) : (A.tensorHomEquiv B C) f = Rep.ofHom { toLinearMap := (TensorProduct.curry (Rep.Hom.hom f).toLinearMap).flip, isIntertwining' := ⋯ }
Rep.ihom_coev_app_hom 📋 Mathlib.RepresentationTheory.Rep.Basic
{k : Type u} [CommRing k] {G : Type v} [Group G] (A B : Rep.{u, u, v} k G) : (Rep.Hom.hom ((CategoryTheory.ihom.coev A).app B)).toLinearMap = (TensorProduct.mk k ↑A ↑((CategoryTheory.Functor.id (Rep.{u, u, v} k G)).obj B)).flip
Rep.MonoidalClosed.linearHomEquivComm_hom 📋 Mathlib.RepresentationTheory.Rep.Basic
{k : Type u} [CommRing k] {G : Type v} [Group G] (A B C : Rep.{u, u, v} k G) (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C) : (Rep.Hom.hom ((Rep.MonoidalClosed.linearHomEquivComm A B C) f)).toLinearMap = TensorProduct.curry (Rep.Hom.hom f).toLinearMap
Rep.MonoidalClosed.linearHomEquiv_hom 📋 Mathlib.RepresentationTheory.Rep.Basic
{k : Type u} [CommRing k] {G : Type v} [Group G] (A B C : Rep.{u, u, v} k G) (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C) : (Rep.Hom.hom ((Rep.MonoidalClosed.linearHomEquiv A B C) f)).toLinearMap = (TensorProduct.curry (Rep.Hom.hom f).toLinearMap).flip
Rep.ihom_map 📋 Mathlib.RepresentationTheory.Rep.Basic
{k : Type u} [CommRing k] {G : Type v} [Group G] (A : Rep.{w, u, v} k G) {X Y : Rep.{u_1, u, v} k G} (f : X ⟶ Y) : A.ihom.map f = Rep.ofHom { toLinearMap := (LinearMap.llcomp k ↑A ↑X ↑Y) (Rep.Hom.hom f).toLinearMap, isIntertwining' := ⋯ }
Rep.tensorHomEquiv_symm_apply 📋 Mathlib.RepresentationTheory.Rep.Basic
{k : Type u} [CommRing k] {G : Type v} [Group G] (A B C : Rep.{u, u, v} k G) (f : B ⟶ A.ihom.obj C) : (A.tensorHomEquiv B C).symm f = Rep.ofHom { toLinearMap := (TensorProduct.uncurry (RingHom.id k) ↑A ↑B ↑C) (Rep.Hom.hom f).flip, isIntertwining' := ⋯ }
Rep.MonoidalClosed.linearHomEquivComm_symm_hom 📋 Mathlib.RepresentationTheory.Rep.Basic
{k : Type u} [CommRing k] {G : Type v} [Group G] (A B C : Rep.{u, u, v} k G) (f : A ⟶ B ⟹ C) : (Rep.Hom.hom ((Rep.MonoidalClosed.linearHomEquivComm A B C).symm f)).toLinearMap = (TensorProduct.uncurry (RingHom.id k) ↑A ↑B ↑C) (Rep.Hom.hom f).toLinearMap
Rep.MonoidalClosed.linearHomEquiv_symm_hom 📋 Mathlib.RepresentationTheory.Rep.Basic
{k : Type u} [CommRing k] {G : Type v} [Group G] (A B C : Rep.{u, u, v} k G) (f : B ⟶ A ⟹ C) : (Rep.Hom.hom ((Rep.MonoidalClosed.linearHomEquiv A B C).symm f)).toLinearMap = (TensorProduct.uncurry (RingHom.id k) ↑A ↑B ↑C) (Rep.Hom.hom f).flip
Rep.ihom_ev_app_hom 📋 Mathlib.RepresentationTheory.Rep.Basic
{k : Type u} [CommRing k] {G : Type v} [Group G] (A B : Rep.{u, u, v} k G) : (Rep.Hom.hom ((CategoryTheory.ihom.ev A).app B)).toLinearMap = (TensorProduct.uncurry (RingHom.id k) (↑A) (↑A →ₗ[k] ↑B) ↑B) LinearMap.id.flip
Rep.liftHomOfSurj_toLinearMap 📋 Mathlib.RepresentationTheory.Rep.Res
{k : Type u} [Semiring k] {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) {X Y : Rep.{u_1, u, v1} k G} (hf : Function.Surjective ⇑f) (f' : Rep.res f X ⟶ Rep.res f Y) : (Rep.Hom.hom (Rep.liftHomOfSurj f hf f')).toLinearMap = (Rep.Hom.hom f').toLinearMap
Rep.resMap_hom_toLinearMap 📋 Mathlib.RepresentationTheory.Rep.Res
{k : Type u} [Semiring k] {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) {M N : Rep.{u_1, u, v1} k G} (p : M ⟶ N) : (Rep.Hom.hom (Rep.resMap f p)).toLinearMap = (Rep.Hom.hom p).toLinearMap
Rep.res_map_hom_toLinearMap 📋 Mathlib.RepresentationTheory.Rep.Res
{k : Type u} [Semiring k] {G : Type v1} {H : Type v2} [Monoid G] [Monoid H] (f : H →* G) {M N : Rep.{u_1, u, v1} k G} (p : M ⟶ N) : (Rep.Hom.hom (Rep.resMap f p)).toLinearMap = (Rep.Hom.hom p).toLinearMap
Rep.invariantsAdjunction_homEquiv_apply_hom 📋 Mathlib.RepresentationTheory.Invariants
(k : Type u) (G : Type v) [CommRing k] [Group G] {X : ModuleCat k} {Y : Rep.{u_1, u, v} k G} (f : (Rep.trivialFunctor k G).obj X ⟶ Y) : ModuleCat.Hom.hom (((Rep.invariantsAdjunction k G).homEquiv X Y) f) = LinearMap.codRestrict Y.ρ.invariants (Rep.Hom.hom f).toLinearMap ⋯
Rep.invariantsAdjunction_homEquiv_symm_apply_hom 📋 Mathlib.RepresentationTheory.Invariants
(k : Type u) (G : Type v) [CommRing k] [Group G] {X : ModuleCat k} {Y : Rep.{u_1, u, v} k G} (f : X ⟶ (Rep.invariantsFunctor k G).obj Y) : (Rep.Hom.hom (((Rep.invariantsAdjunction k G).homEquiv X Y).symm f)).toLinearMap = Y.ρ.invariants.subtype ∘ₗ ModuleCat.Hom.hom f
Rep.invariantsFunctor_map_hom 📋 Mathlib.RepresentationTheory.Invariants
(k : Type u) (G : Type v) [CommRing k] [Group G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B) : ModuleCat.Hom.hom ((Rep.invariantsFunctor k G).map f) = LinearMap.codRestrict B.ρ.invariants ((Rep.Hom.hom f).toLinearMap ∘ₗ A.ρ.invariants.subtype) ⋯
Representation.coindMap_coe_apply 📋 Mathlib.RepresentationTheory.Coinduced
{k : Type u_1} {G : Type u_2} {H : Type u_3} [Semiring k] [Monoid G] [Monoid H] (φ : G →* H) {A : Type u_4} {B : Type u_5} [AddCommMonoid A] [Module k A] [AddCommMonoid B] [Module k B] (σ : Representation k G A) (ρ : Representation k G B) (f : σ.IntertwiningMap ρ) (x : ↥(Representation.coindV φ σ)) : ↑((Representation.coindMap φ f) x) = (f.compLeft H) ↑x
Rep.coind'_ext 📋 Mathlib.RepresentationTheory.Coinduced
{k : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) {A : Rep.{max u w, u, v} k G} {f g : ↑(Rep.coind' φ A)} (hfg : ∀ (h : H), (Rep.Hom.hom f).toLinearMap (MonoidAlgebra.single h 1) = (Rep.Hom.hom g).toLinearMap (MonoidAlgebra.single h 1)) : f = g
Rep.coind'_ext_iff 📋 Mathlib.RepresentationTheory.Coinduced
{k : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] {φ : G →* H} {A : Rep.{max u w, u, v} k G} {f g : ↑(Rep.coind' φ A)} : f = g ↔ ∀ (h : H), (Rep.Hom.hom f).toLinearMap (MonoidAlgebra.single h 1) = (Rep.Hom.hom g).toLinearMap (MonoidAlgebra.single h 1)
Rep.resCoindHomEquiv_symm_apply 📋 Mathlib.RepresentationTheory.Coinduced
{k : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (B : Rep.{max w t, u, w} k H) (A : Rep.{max w t, u, v} k G) (f : B ⟶ Rep.coind.{u, v, w, max t w} φ A) : (Rep.resCoindHomEquiv.{t, u, v, w} φ B A).symm f = Rep.ofHom { toLinearMap := LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Rep.Hom.hom f).toLinearMap, isIntertwining' := ⋯ }
Rep.coindVEquiv_symm_apply_coe 📋 Mathlib.RepresentationTheory.Coinduced
{k : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (A : Rep.{max u w, u, v} k G) (f : Rep.res φ (Rep.leftRegular k H) ⟶ A) (h : H) : ↑((Rep.coindVEquiv φ A).symm f) h = (Rep.Hom.hom f).toLinearMap (MonoidAlgebra.single h 1)
Rep.coinvariantsAdjunction_homEquiv_apply_hom 📋 Mathlib.RepresentationTheory.Coinvariants
(k : Type u) (G : Type v) [CommRing k] [Monoid G] {X : Rep.{w, u, v} k G} {Y : ModuleCat k} (f : (Rep.coinvariantsFunctor k G).obj X ⟶ Y) : (Rep.Hom.hom (((Rep.coinvariantsAdjunction k G).homEquiv X Y) f)).toLinearMap = ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app X) f)
Rep.quotientToCoinvariantsFunctor_map_hom_toLinearMap 📋 Mathlib.RepresentationTheory.Coinvariants
(k : Type u) {G : Type v} [CommRing k] [Group G] (S : Subgroup G) [S.Normal] {X Y : Rep.{w, u, v} k G} (f : X ⟶ Y) : (Rep.Hom.hom ((Rep.quotientToCoinvariantsFunctor k S).map f)).toLinearMap = Representation.Coinvariants.map (MonoidHom.comp X.ρ S.subtype) (MonoidHom.comp Y.ρ S.subtype) (Rep.Hom.hom (Rep.resMap S.subtype f))
Rep.indResHomEquiv_apply 📋 Mathlib.RepresentationTheory.Induced
{k : Type u} {G : Type v} {H : Type v'} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep.{max w v' u, u, v} k G) (B : Rep.{max w v' u, u, v'} k H) (f : Rep.ind φ A ⟶ B) : (Rep.indResHomEquiv φ A B) f = Rep.ofHom { toLinearMap := (Rep.Hom.hom f).toLinearMap ∘ₗ Representation.IndV.mk φ A.ρ 1, isIntertwining' := ⋯ }
Rep.indResHomEquiv_symm_apply 📋 Mathlib.RepresentationTheory.Induced
{k : Type u} {G : Type v} {H : Type v'} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep.{max w v' u, u, v} k G) (B : Rep.{max w v' u, u, v'} k H) (f : A ⟶ Rep.res φ B) : (Rep.indResHomEquiv φ A B).symm f = Rep.ofHom { toLinearMap := Representation.Coinvariants.lift (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ) (TensorProduct.lift (((Finsupp.lift (↑A →ₗ[k] ↑B) k H) fun h => B.ρ h⁻¹ ∘ₗ (Rep.Hom.hom f).toLinearMap) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k))) ⋯, isIntertwining' := ⋯ }
Rep.indCoindIso_hom_hom_toLinearMap 📋 Mathlib.RepresentationTheory.FiniteIndex
{k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] (A : Rep.{max w u, u, v} k ↥S) : (Rep.Hom.hom A.indCoindIso.hom).toLinearMap = A.indToCoind
Rep.indCoindIso_inv_hom_toLinearMap 📋 Mathlib.RepresentationTheory.FiniteIndex
{k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] (A : Rep.{max w u, u, v} k ↥S) : (Rep.Hom.hom A.indCoindIso.inv).toLinearMap = { toFun := (Representation.Equiv.mk (LinearEquiv.ofLinearMap A.indToCoind A.coindToInd ⋯ ⋯) ⋯).invFun, map_add' := ⋯, map_smul' := ⋯ }
Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination 📋 Mathlib.RepresentationTheory.Homological.FiniteCyclic
(k : Type u) {G : Type u} [CommRing k] [CommGroup G] (g : G) [Finite G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : (Rep.Hom.hom ((Rep.leftRegular k G).applyAsHom g - CategoryTheory.CategoryStruct.id (Rep.leftRegular k G))).range = ((Finsupp.linearCombination k fun x => 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker
Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm 📋 Mathlib.RepresentationTheory.Homological.FiniteCyclic
(k : Type u) {G : Type u} [CommRing k] [CommGroup G] [Fintype G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : (Rep.Hom.hom ((Rep.leftRegular k G).applyAsHom g - CategoryTheory.CategoryStruct.id (Rep.leftRegular k G))).range = (Rep.Hom.hom (Rep.leftRegular k G).norm).ker
Rep.FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub 📋 Mathlib.RepresentationTheory.Homological.FiniteCyclic
(k : Type u) {G : Type u} [CommRing k] [CommGroup G] [Fintype G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : (Rep.Hom.hom (Rep.leftRegular k G).norm).range = (Rep.Hom.hom ((Rep.leftRegular k G).applyAsHom g - CategoryTheory.CategoryStruct.id (Rep.leftRegular k G))).ker
Rep.standardComplex.d_eq 📋 Mathlib.RepresentationTheory.Homological.Resolution
(k G : Type u) [CommRing k] [Monoid G] (n : ℕ) : (Rep.Hom.hom ((Rep.standardComplex k G).d (n + 1) n)).toLinearMap = Rep.standardComplex.d k G (n + 1)
Rep.FiniteCyclicGroup.groupCohomologyπOdd 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i) : ModuleCat.of k ↥(Rep.Hom.hom A.norm).ker ⟶ groupCohomology A i
Rep.FiniteCyclicGroup.groupCohomologyIso₀ 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : groupCohomology A 0 ≅ ModuleCat.of k ↥(Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker
Rep.FiniteCyclicGroup.groupCohomologyπEven 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [NeZero i] (hi : Even i) : ModuleCat.of k ↥(Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker ⟶ groupCohomology A i
Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i) (x : ↥(Rep.Hom.hom A.norm).ker) : (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπOdd A g hg i hi)) x = 0 ↔ ↑x ∈ (Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).range
Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [NeZero i] (hi : Even i) (x : ↥(Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker) : (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπEven A g hg i hi)) x = 0 ↔ ↑x ∈ (Rep.Hom.hom A.norm).range
Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_iff 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i) (x y : ↥(Rep.Hom.hom A.norm).ker) : (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπOdd A g hg i hi)) x = (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπOdd A g hg i hi)) y ↔ ↑x - ↑y ∈ (Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).range
Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_iff 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [NeZero i] (hi : Even i) (x y : ↥(Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker) : (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπEven A g hg i hi)) x = (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπEven A g hg i hi)) y ↔ ↑x - ↑y ∈ (Rep.Hom.hom A.norm).range
groupCohomology.map_congr 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} {f g : G →* H} {φ : Rep.res f A ⟶ B} {ψ : Rep.res g A ⟶ B} (hfg : f = g) (hφψ : (Rep.Hom.hom φ).toLinearMap = (Rep.Hom.hom ψ).toLinearMap) (n : ℕ) : groupCohomology.map f φ n = groupCohomology.map g ψ n
groupCohomology.cochainsMap_id_f_hom_eq_compLeft 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
{k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) (i : ℕ) : ModuleCat.Hom.hom ((groupCohomology.cochainsMap (MonoidHom.id G) f).f i) = (Rep.Hom.hom f).compLeft (Fin i → G)
groupCohomology.cochainsMap_congr 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} {f g : G →* H} {φ : Rep.res f A ⟶ B} {ψ : Rep.res g A ⟶ B} (hfg : f = g) (hφψ : (Rep.Hom.hom φ).toLinearMap = (Rep.Hom.hom ψ).toLinearMap) : groupCohomology.cochainsMap f φ = groupCohomology.cochainsMap g ψ
groupCohomology.cochainsMap_f_hom 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (i : ℕ) : ModuleCat.Hom.hom ((groupCohomology.cochainsMap f φ).f i) = (Rep.Hom.hom φ).compLeft (Fin i → G) ∘ₗ LinearMap.funLeft k ↑A fun x => ⇑f ∘ x
groupCohomology.cochainsMap_f 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (i : ℕ) : (groupCohomology.cochainsMap f φ).f i = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (LinearMap.funLeft k ↑A fun x => ⇑f ∘ x)) (ModuleCat.ofHom ((Rep.Hom.hom φ).compLeft (Fin i → G)))
groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_apply 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↑(groupCohomology.cocycles A 0)) : (ModuleCat.Hom.hom (groupCohomology.cochainsIso₀ B).hom) ((ModuleCat.Hom.hom (groupCohomology.iCocycles B 0)) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cocyclesMap f φ 0)) x)) = (Rep.Hom.hom φ).toLinearMap ((ModuleCat.Hom.hom (groupCohomology.cochainsIso₀ A).hom) ((ModuleCat.Hom.hom (groupCohomology.iCocycles A 0)) x))
groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : (Fin 1 → H) → ↑A) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₁ B).hom) ((CategoryTheory.ConcreteCategory.hom ((groupCohomology.cochainsMap f φ).f 1)) x) = ((Rep.Hom.hom φ).compLeft G) ((LinearMap.funLeft k ↑A ⇑f) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₁ A).hom) x))
groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : (Fin 2 → H) → ↑A) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₂ B).hom) ((CategoryTheory.ConcreteCategory.hom ((groupCohomology.cochainsMap f φ).f 2)) x) = ((Rep.Hom.hom φ).compLeft (G × G)) ((LinearMap.funLeft k (↑A) (Prod.map ⇑f ⇑f)) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₂ A).hom) x))
groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : (Fin 3 → H) → ↑A) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₃ B).hom) ((CategoryTheory.ConcreteCategory.hom ((groupCohomology.cochainsMap f φ).f 3)) x) = ((Rep.Hom.hom φ).compLeft (G × G × G)) ((LinearMap.funLeft k (↑A) (Prod.map (⇑f) (Prod.map ⇑f ⇑f))) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₃ A).hom) x))
groupCohomology.map_id_comp_H0Iso_hom_apply 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
{k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) (x : ↑(groupCohomology A 0)) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.H0Iso B).hom) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id G) f 0)) x) = (LinearMap.codRestrict B.ρ.invariants ((Rep.Hom.hom f).toLinearMap ∘ₗ A.ρ.invariants.subtype) ⋯) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H0Iso A).hom) x)
groupCohomology.map_H0Iso_hom_f_apply 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k H} {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↑(groupCohomology A 0)) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.shortComplexH0 B).f) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H0Iso B).hom) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.map f φ 0)) x)) = (Rep.Hom.hom φ).toLinearMap ((CategoryTheory.ConcreteCategory.hom (groupCohomology.shortComplexH0 A).f) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H0Iso A).hom) x))
groupCohomology.mapCocycles₁_comp_i_apply 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{max u u_1, u, u} k H} {B : Rep.{max u u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↥(groupCohomology.cocycles₁ A)) : (ModuleCat.Hom.hom (groupCohomology.shortComplexH1 B).g).ker.subtype ((CategoryTheory.ConcreteCategory.hom (groupCohomology.mapCocycles₁ f φ)) x) = ((Rep.Hom.hom φ).compLeft G) ((LinearMap.funLeft k ↑A ⇑f) ((ModuleCat.Hom.hom (groupCohomology.shortComplexH1 A).g).ker.subtype x))
groupCohomology.mapCocycles₂_comp_i_apply 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u_1, u, u} k H} {B : Rep.{u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↥(groupCohomology.cocycles₂ A)) : (ModuleCat.Hom.hom (groupCohomology.shortComplexH2 B).g).ker.subtype ((CategoryTheory.ConcreteCategory.hom (groupCohomology.mapCocycles₂ f φ)) x) = ((Rep.Hom.hom φ).compLeft (G × G)) ((LinearMap.funLeft k (↑A) (Prod.map ⇑f ⇑f)) ((ModuleCat.Hom.hom (groupCohomology.shortComplexH2 A).g).ker.subtype x))
Rep.FiniteCyclicGroup.groupHomologyIso₀ 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : groupHomology A 0 ≅ ModuleCat.of k (↑A ⧸ (Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).range)
Rep.FiniteCyclicGroup.groupHomologyπOdd 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) [DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i) : ModuleCat.of k ↥(Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker ⟶ groupHomology A i
Rep.FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) [DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [NeZero i] (hi : Even i) (x : ↥(LinearMap.ker A.ρ.norm)) : (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupHomologyπEven A g hg i hi)) x = 0 ↔ ↑x ∈ (Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).range
Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) [DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i) (x : ↥(Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker) : (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupHomologyπOdd A g hg i hi)) x = 0 ↔ ↑x ∈ LinearMap.range A.ρ.norm
Rep.FiniteCyclicGroup.groupHomologyπEven_eq_iff 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) [DecidableEq G] (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [NeZero i] (hi : Even i) (x y : ↥(LinearMap.ker A.ρ.norm)) : (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupHomologyπEven A g hg i hi)) x = (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupHomologyπEven A g hg i hi)) y ↔ ↑x - ↑y ∈ (Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).range
Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_iff 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
{k G : Type u} [CommRing k] [CommGroup G] [Fintype G] [DecidableEq G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (A : Rep.{u, u, u} k G) (i : ℕ) (hi : Odd i) (x y : ↥(Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker) : (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupHomologyπOdd A g hg i hi)) x = (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupHomologyπOdd A g hg i hi)) y ↔ ↑x - ↑y ∈ LinearMap.range A.ρ.norm
groupHomology.map_congr 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} {f g : G →* H} {φ : A ⟶ Rep.res f B} {ψ : A ⟶ Rep.res g B} (hfg : f = g) (hφψ : (Rep.Hom.hom φ).toLinearMap = (Rep.Hom.hom ψ).toLinearMap) (n : ℕ) : groupHomology.map f φ n = groupHomology.map g ψ n
groupHomology.chainsMap_id_f_hom_eq_mapRange 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
{k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (i : ℕ) (φ : A ⟶ B) : ModuleCat.Hom.hom ((groupHomology.chainsMap (MonoidHom.id G) φ).f i) = Finsupp.mapRange.linearMap (Rep.Hom.hom φ).toLinearMap
groupHomology.chainsMap_congr 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} {f g : G →* H} {φ : A ⟶ Rep.res f B} {ψ : A ⟶ Rep.res g B} (hfg : f = g) (hφψ : (Rep.Hom.hom φ).toLinearMap = (Rep.Hom.hom ψ).toLinearMap) : groupHomology.chainsMap f φ = groupHomology.chainsMap g ψ
groupHomology.lsingle_comp_chainsMap_f 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (n : ℕ) (x : Fin n → G) : CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.lsingle x)) ((groupHomology.chainsMap f φ).f n) = ModuleCat.ofHom (Finsupp.lsingle (⇑f ∘ x) ∘ₗ (Rep.Hom.hom φ).toLinearMap)
groupHomology.chainsMap_f 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (i : ℕ) : (groupHomology.chainsMap f φ).f i = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.lmapDomain (↑A) k fun x => ⇑f ∘ x)) (ModuleCat.ofHom (Finsupp.mapRange.linearMap (Rep.Hom.hom φ).toLinearMap))
groupHomology.chainsMap_f_hom 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (i : ℕ) : ModuleCat.Hom.hom ((groupHomology.chainsMap f φ).f i) = Finsupp.mapRange.linearMap (Rep.Hom.hom φ).toLinearMap ∘ₗ Finsupp.lmapDomain (↑A) k fun x => ⇑f ∘ x
groupHomology.lsingle_comp_chainsMap_f_assoc 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (n : ℕ) (x : Fin n → G) {Z : ModuleCat k} (h : ModuleCat.of k ((Fin n → H) →₀ ↑B) ⟶ Z) : CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.lsingle x)) (CategoryTheory.CategoryStruct.comp ((groupHomology.chainsMap f φ).f n) h) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.lsingle (⇑f ∘ x) ∘ₗ (Rep.Hom.hom φ).toLinearMap)) h
groupHomology.chainsMap_f_1_comp_chainsIso₁_apply 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (x : (Fin 1 → G) →₀ ↑A) : (CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₁ B).hom) ((CategoryTheory.ConcreteCategory.hom ((groupHomology.chainsMap f φ).f 1)) x) = Finsupp.mapRange ⇑(Rep.Hom.hom φ) ⋯ (Finsupp.mapDomain (⇑f) ((CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₁ A).hom) x))
groupHomology.chainsMap_f_2_comp_chainsIso₂_apply 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (x : (Fin 2 → G) →₀ ↑A) : (CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₂ B).hom) ((CategoryTheory.ConcreteCategory.hom ((groupHomology.chainsMap f φ).f 2)) x) = Finsupp.mapRange ⇑(Rep.Hom.hom φ) ⋯ (Finsupp.mapDomain (Prod.map ⇑f ⇑f) ((CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₂ A).hom) x))
groupHomology.chainsMap_f_3_comp_chainsIso₃_apply 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (x : (Fin 3 → G) →₀ ↑A) : (CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₃ B).hom) ((CategoryTheory.ConcreteCategory.hom ((groupHomology.chainsMap f φ).f 3)) x) = Finsupp.mapRange ⇑(Rep.Hom.hom φ) ⋯ (Finsupp.mapDomain (Prod.map (⇑f) (Prod.map ⇑f ⇑f)) ((CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₃ A).hom) x))
groupHomology.mapCycles₁_comp_i_apply 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (x : ↥(groupHomology.cycles₁ A)) : (ModuleCat.Hom.hom (groupHomology.shortComplexH1 B).g).ker.subtype ((CategoryTheory.ConcreteCategory.hom (groupHomology.mapCycles₁ f φ)) x) = (Finsupp.mapRange.linearMap (Rep.Hom.hom φ).toLinearMap) ((Finsupp.lmapDomain (↑A) k ⇑f) ((ModuleCat.Hom.hom (groupHomology.shortComplexH1 A).g).ker.subtype x))
groupHomology.mapCycles₂_comp_i_apply 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
{k G H : Type u} [CommRing k] [Group G] [Group H] {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (x : ↥(groupHomology.cycles₂ A)) : (ModuleCat.Hom.hom (groupHomology.shortComplexH2 B).g).ker.subtype ((CategoryTheory.ConcreteCategory.hom (groupHomology.mapCycles₂ f φ)) x) = (Finsupp.mapRange.linearMap (Rep.Hom.hom φ).toLinearMap) ((Finsupp.lmapDomain (↑A) k (Prod.map ⇑f ⇑f)) ((ModuleCat.Hom.hom (groupHomology.shortComplexH2 A).g).ker.subtype x))
groupHomology.cyclesMkOfCompEqD 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
{k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hX : X.ShortExact) {i j : ℕ} {y : (Fin i → G) →₀ ↑X.X₂} {x : (Fin j → G) →₀ ↑X.X₁} (hx : (Finsupp.mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (CategoryTheory.ConcreteCategory.hom ((groupHomology.inhomogeneousChains X.X₂).d i j)) y) : ↑(groupHomology.cycles X.X₁ j)
groupHomology.δ_apply 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
{k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hX : X.ShortExact) {i j : ℕ} (hij : j + 1 = i) (z : (Fin i → G) →₀ ↑X.X₃) (hz : (CategoryTheory.ConcreteCategory.hom ((groupHomology.inhomogeneousChains X.X₃).d i j)) z = 0) (y : (Fin i → G) →₀ ↑X.X₂) (hy : (CategoryTheory.ConcreteCategory.hom ((groupHomology.chainsMap (MonoidHom.id G) X.g).f i)) y = z) (x : (Fin j → G) →₀ ↑X.X₁) (hx : (Finsupp.mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (CategoryTheory.ConcreteCategory.hom ((groupHomology.inhomogeneousChains X.X₂).d i j)) y) : (CategoryTheory.ConcreteCategory.hom (groupHomology.δ hX i j hij)) ((CategoryTheory.ConcreteCategory.hom (groupHomology.π X.X₃ i)) (groupHomology.cyclesMk i j ⋯ z ⋯)) = (CategoryTheory.ConcreteCategory.hom (groupHomology.π X.X₁ j)) (groupHomology.cyclesMkOfCompEqD hX hx)
groupHomology.mem_cycles₁_of_comp_eq_d₂₁ 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
{k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hX : X.ShortExact) {y : G × G →₀ ↑X.X₂} {x : G →₀ ↑X.X₁} (hx : (Finsupp.mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (CategoryTheory.ConcreteCategory.hom (groupHomology.d₂₁ X.X₂)) y) : x ∈ groupHomology.cycles₁ X.X₁
groupHomology.δ₀_apply 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
{k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hX : X.ShortExact) (z : ↥(groupHomology.cycles₁ X.X₃)) (y : G →₀ ↑X.X₂) (hy : (Finsupp.mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z) (x : ↑X.X₁) (hx : (Rep.Hom.hom X.f) x = (CategoryTheory.ConcreteCategory.hom (groupHomology.d₁₀ X.X₂)) y) : (CategoryTheory.ConcreteCategory.hom (groupHomology.δ hX 1 0 ⋯)) ((CategoryTheory.ConcreteCategory.hom (groupHomology.H1π X.X₃)) z) = (CategoryTheory.ConcreteCategory.hom (groupHomology.H0π X.X₁)) x
groupHomology.δ₁_apply 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
{k G : Type u} [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hX : X.ShortExact) (z : ↥(groupHomology.cycles₂ X.X₃)) (y : G × G →₀ ↑X.X₂) (hy : (Finsupp.mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z) (x : G →₀ ↑X.X₁) (hx : (Finsupp.mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (CategoryTheory.ConcreteCategory.hom (groupHomology.d₂₁ X.X₂)) y) : (CategoryTheory.ConcreteCategory.hom (groupHomology.δ hX 2 1 ⋯)) ((CategoryTheory.ConcreteCategory.hom (groupHomology.H2π X.X₃)) z) = (CategoryTheory.ConcreteCategory.hom (groupHomology.H1π X.X₁)) ⟨x, ⋯⟩

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.
You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59