feat(RepresentationTheory/Coinvariants): more API about the coinvariants of a representation (#21735)

In this PR we add more API for the coinvariants of a representation `(V, ρ)`:

* `Representation.coinvariantsFinsuppLEquiv ρ α`: given a type `α`, this is the `k`-linear
equivalence between `(α →₀ V)_G` and `α →₀ V_G`.

* `Representation.coinvariantsTprodLeftRegularLEquiv ρ`: the `k`-linear equivalence between
`(V ⊗[k] k[G])_G` and `V` sending `⟦v ⊗ single g r⟧ ↦ r • ρ(g⁻¹)(v)`.

* `Rep.coinvariantsTensor k G`: the functor sending representations `A, B` to `(A ⊗[k] B)_G`. This
is naturally isomorphic to the functor sending `A, B` to `A ⊗[k[G]] B`, where we give `A` the
`k[G]ᵐᵒᵖ`-module structure defined by `g • a := A.ρ g⁻¹ a`.

* `Rep.coinvariantsTensorFreeLEquiv A α`: given a representation `A` and a type `α`, this is the
`k`-linear equivalence between `(A ⊗ (α →₀ k[G]))_G` and `α →₀ A` sending
`⟦a ⊗ single x (single g r)⟧ ↦ single x (r • ρ(g⁻¹)(a))`. This is useful for group homology.



Co-authored-by: 101damnations <al3717@ic.ac.uk>

Author: Amelia Livingston

Mathlib/RepresentationTheory/Coinvariants.lean

@@ -16,6 +16,22 @@ of the form `ρ g x - x` for `x : V`, `g : G`. Then the coinvariants of `(V, ρ)
 `V` by this submodule. We show that the functor sending a representation to its coinvariants is
 left adjoint to the functor equipping a module with the trivial representation.
 
+## Main definitions
+
+* `Representation.Coinvariants ρ`: the coinvariants of a representation `ρ`.
+* `Representation.coinvariantsFinsuppLEquiv ρ α`: given a type `α`, this is the `k`-linear
+  equivalence between `(α →₀ V)_G` and `α →₀ V_G`.
+* `Representation.coinvariantsTprodLeftRegularLEquiv ρ`: the `k`-linear equivalence between
+  `(V ⊗ k[G])_G` and `V` sending `⟦v ⊗ single g r⟧ ↦ r • ρ(g⁻¹)(v)`.
+* `Rep.coinvariantsAdjunction k G`: the adjunction between the functor sending a representation to
+  its coinvariants and the functor equipping a module with the trivial representation.
+* `Rep.coinvariantsTensor k G`: the functor sending representations `A, B` to `(A ⊗[k] B)_G`. This
+  is naturally isomorphic to the functor sending `A, B` to `A ⊗[k[G]] B`, where we give `A` the
+  `k[G]ᵐᵒᵖ`-module structure defined by `g • a := A.ρ g⁻¹ a`.
+* `Rep.coinvariantsTensorFreeLEquiv A α`: given a representation `A` and a type `α`, this is the
+  `k`-linear equivalence between `(A ⊗ (α →₀ k[G]))_G` and `α →₀ A` sending
+  `⟦a ⊗ single x (single g r)⟧ ↦ single x (r • ρ(g⁻¹)(a))`. This is useful for group homology.
+
 -/
 
 universe u v
@@ -124,7 +140,105 @@ lemma map_comp (φ : V →ₗ[k] W) (ψ : W →ₗ[k] X)
       ext x; have : φ _ = _ := congr($(H g) x); have : ψ _ = _ := congr($(h g) (φ x)); simp_all) :=
   hom_ext rfl
 
-end Representation.Coinvariants
+end Coinvariants
+
+section Finsupp
+
+open Finsupp Coinvariants
+
+variable {k G V : Type*} [CommRing k] [Group G] [AddCommGroup V] [Module k V]
+  (ρ : Representation k G V) (α : Type*)
+
+/-- Given a `G`-representation `(V, ρ)` and a type `α`, this is the map `(α →₀ V)_G →ₗ (α →₀ V_G)`
+sending `⟦single a v⟧ ↦ single a ⟦v⟧`. -/
+noncomputable def coinvariantsToFinsupp :
+    Coinvariants (ρ.finsupp α) →ₗ[k] α →₀ Coinvariants ρ :=
+  Coinvariants.lift _ (mapRange.linearMap (Coinvariants.mk _)) <| fun _ => by ext; simp
+
+variable {ρ α}
+
+@[simp]
+lemma coinvariantsToFinsupp_mk_single (x : α) (a : V) :
+    coinvariantsToFinsupp ρ α (Coinvariants.mk _ (single x a)) =
+      single x (Coinvariants.mk _ a) := by
+  simp [coinvariantsToFinsupp]
+
+variable (ρ α) in
+/-- Given a `G`-representation `(V, ρ)` and a type `α`, this is the map `(α →₀ V_G) →ₗ (α →₀ V)_G`
+sending `single a ⟦v⟧ ↦ ⟦single a v⟧`. -/
+noncomputable def finsuppToCoinvariants :
+    (α →₀ Coinvariants ρ) →ₗ[k] Coinvariants (ρ.finsupp α) :=
+  lsum (R := k) k fun a => Coinvariants.lift _ (Coinvariants.mk _ ∘ₗ lsingle a) fun g =>
+    LinearMap.ext fun x => (mk_eq_iff _).2 <| mem_ker_of_eq g (single a x) _ <| by simp
+
+@[simp]
+lemma finsuppToCoinvariants_single_mk (a : α) (x : V) :
+    finsuppToCoinvariants ρ α (single a <| Coinvariants.mk _ x) =
+      Coinvariants.mk _ (single a x) := by
+  simp [finsuppToCoinvariants]
+
+variable (ρ α) in
+/-- Given a `G`-representation `(V, ρ)` and a type `α`, this is the linear equivalence
+`(α →₀ V)_G ≃ₗ (α →₀ V_G)` sending `⟦single a v⟧ ↦ single a ⟦v⟧`. -/
+@[simps! symm_apply]
+noncomputable def coinvariantsFinsuppLEquiv :
+    Coinvariants (ρ.finsupp α) ≃ₗ[k] α →₀ Coinvariants ρ :=
+  LinearEquiv.ofLinear (coinvariantsToFinsupp ρ α) (finsuppToCoinvariants ρ α)
+    (by ext; simp) (by ext; simp)
+
+@[simp]
+lemma coinvariantsFinsuppLEquiv_apply (x : Coinvariants (ρ.finsupp α)) :
+    coinvariantsFinsuppLEquiv ρ α x = coinvariantsToFinsupp ρ α x := by rfl
+
+end Finsupp
+
+section TensorProduct
+
+open TensorProduct Coinvariants Finsupp
+
+variable {k G V W : Type*} [CommRing k] [Group G] [AddCommGroup V] [Module k V]
+  [AddCommGroup W] [Module k W] (ρ : Representation k G V) (τ : Representation k G W)
+
+-- the next two lemmas eliminate inverses
+
+@[simp]
+lemma Coinvariants.mk_inv_tmul (x : V) (y : W) (g : G) :
+    Coinvariants.mk (ρ.tprod τ) (ρ g⁻¹ x ⊗ₜ[k] y) = Coinvariants.mk (ρ.tprod τ) (x ⊗ₜ[k] τ g y) :=
+  (mk_eq_iff _).2 <| mem_ker_of_eq g⁻¹ (x ⊗ₜ[k] τ g y) _ <| by simp
+
+@[simp]
+lemma Coinvariants.mk_tmul_inv (x : V) (y : W) (g : G) :
+    Coinvariants.mk (ρ.tprod τ) (x ⊗ₜ[k] τ g⁻¹ y) = Coinvariants.mk (ρ.tprod τ) (ρ g x ⊗ₜ[k] y) :=
+  (mk_eq_iff _).2 <| mem_ker_of_eq g⁻¹ (ρ g x ⊗ₜ[k] y) _ <| by simp
+
+/-- Given a `k`-linear `G`-representation `V, ρ`, this is the map `(V ⊗ k[G])_G →ₗ[k] V` sending
+`⟦v ⊗ single g r⟧ ↦ r • ρ(g⁻¹)(v)`. -/
+noncomputable def ofCoinvariantsTprodLeftRegular :
+    Coinvariants (ρ.tprod (leftRegular k G)) →ₗ[k] V :=
+  Coinvariants.lift _ (TensorProduct.lift (Finsupp.linearCombination _ fun g => ρ g⁻¹) ∘ₗ
+    (TensorProduct.comm _ _ _).toLinearMap) fun _ => by ext; simp
+
+@[simp]
+lemma ofCoinvariantsTprodLeftRegular_mk_tmul_single (x : V) (g : G) (r : k) :
+    ofCoinvariantsTprodLeftRegular ρ (Coinvariants.mk _ (x ⊗ₜ Finsupp.single g r)) = r • ρ g⁻¹ x :=
+  congr($(Finsupp.linearCombination_single k (v := fun g => ρ g⁻¹) r g) x)
+
+/-- Given a `k`-linear `G`-representation `(V, ρ)`, this is the linear equivalence
+`(V ⊗ k[G])_G ≃ₗ[k] V` sending `⟦v ⊗ single g r⟧ ↦ r • ρ(g⁻¹)(v)`. -/
+@[simps! symm_apply]
+noncomputable def coinvariantsTprodLeftRegularLEquiv :
+    Coinvariants (ρ.tprod (leftRegular k G)) ≃ₗ[k] V :=
+  LinearEquiv.ofLinear (ofCoinvariantsTprodLeftRegular ρ)
+    (Coinvariants.mk _ ∘ₗ (TensorProduct.mk k V (G →₀ k)).flip (single 1 1))
+    (by ext; simp) (by ext; simp)
+
+@[simp]
+lemma coinvariantsTprodLeftRegularLEquiv_apply (x : (ρ.tprod (leftRegular k G)).Coinvariants) :
+    coinvariantsTprodLeftRegularLEquiv ρ x = ofCoinvariantsTprodLeftRegular ρ x := by
+  rfl
+
+end TensorProduct
+end Representation
 
 namespace Rep
 
@@ -198,4 +312,100 @@ theorem coinvariantsAdjunction_homEquiv_symm_apply_hom {X : Rep k G} {Y : Module
 instance : (coinvariantsFunctor k G).PreservesZeroMorphisms where
 instance : (coinvariantsFunctor k G).IsLeftAdjoint := (coinvariantsAdjunction k G).isLeftAdjoint
 
+/-- The functor sending `A, B` to `(A ⊗[k] B)_G`. This is naturally isomorphic to the functor
+sending `A, B` to `A ⊗[k[G]] B`, where we give `A` the `k[G]ᵐᵒᵖ`-module structure defined by
+`g • a := A.ρ g⁻¹ a`. -/
+noncomputable abbrev coinvariantsTensor : Rep k G ⥤ Rep k G ⥤ ModuleCat k :=
+  (Functor.postcompose₂.obj (coinvariantsFunctor k G)).obj (MonoidalCategory.curriedTensor _)
+
+variable {k G} (A B)
+
+/-- The bilinear map sending `a : A, b : B` to `⟦a ⊗ₜ b⟧` in `(A ⊗[k] B)_G`. -/
+noncomputable abbrev coinvariantsTensorMk :
+    A →ₗ[k] B →ₗ[k] ((coinvariantsTensor k G).obj A).obj B :=
+  (TensorProduct.mk k A B).compr₂ (Coinvariants.mk _)
+
+variable {A B}
+
+lemma coinvariantsTensorMk_apply (a : A) (b : B) :
+  coinvariantsTensorMk A B a b = Coinvariants.mk _ (a ⊗ₜ[k] b) := rfl
+
+@[ext]
+lemma coinvariantsTensor_hom_ext {M : ModuleCat k}
+    {f g : ((coinvariantsTensor k G).obj A).obj B ⟶ M}
+    (hfg : (coinvariantsTensorMk A B).compr₂ f.hom = (coinvariantsTensorMk A B).compr₂ g.hom) :
+    f = g := coinvariantsFunctor_hom_ext <| ModuleCat.hom_ext <| TensorProduct.ext <| hfg
+
+instance (A : Rep k G) : ((coinvariantsTensor k G).obj A).Additive where
+instance (A : Rep k G) : ((coinvariantsTensor k G).obj A).Linear k where
+
+section Finsupp
+
+variable {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (α : Type u) [DecidableEq α]
+
+open MonoidalCategory Finsupp Representation ModuleCat.MonoidalCategory
+
+/-- Given a `k`-linear `G`-representation `(A, ρ)` and a type `α`, this is the map
+`(A ⊗ (α →₀ k[G]))_G →ₗ[k] (α →₀ A)` sending
+`⟦a ⊗ single x (single g r)⟧ ↦ single x (r • ρ(g⁻¹)(a)).` -/
+noncomputable def coinvariantsTensorFreeToFinsupp :
+    (A ⊗ free k G α).ρ.Coinvariants →ₗ[k] (α →₀ A) :=
+  (coinvariantsFinsuppLEquiv _ α ≪≫ₗ lcongr (Equiv.refl α)
+    (coinvariantsTprodLeftRegularLEquiv A.ρ)).toLinearMap ∘ₗ
+    ((coinvariantsFunctor k G).map (finsuppTensorRight A (leftRegular k G) α).hom).hom
+
+variable {A α}
+
+@[simp]
+lemma coinvariantsTensorFreeToFinsupp_mk_tmul_single (x : A) (i : α) (g : G) (r : k) :
+    DFunLike.coe (F := (A.ρ.tprod (Representation.free k G α)).Coinvariants →ₗ[k] α →₀ A.V)
+      (coinvariantsTensorFreeToFinsupp A α) (Coinvariants.mk _ (x ⊗ₜ single i (single g r))) =
+      single i (r • A.ρ g⁻¹ x) := by
+  simp [tensorObj_def, ModuleCat.MonoidalCategory.tensorObj, coinvariantsTensorFreeToFinsupp,
+    Coinvariants.map, finsuppTensorRight, TensorProduct.finsuppRight]
+
+variable (A α)
+
+/-- Given a `k`-linear `G`-representation `(A, ρ)` and a type `α`, this is the map
+`(α →₀ A) →ₗ[k] (A ⊗ (α →₀ k[G]))_G` sending `single x a ↦ ⟦a ⊗ₜ single x 1⟧.` -/
+noncomputable def finsuppToCoinvariantsTensorFree :
+    (α →₀ A) →ₗ[k] Coinvariants (A ⊗ (free k G α)).ρ :=
+  ((coinvariantsFunctor k G).map ((finsuppTensorRight A (leftRegular k G) α)).inv).hom ∘ₗ
+    (coinvariantsFinsuppLEquiv _ α ≪≫ₗ
+    lcongr (Equiv.refl α) (coinvariantsTprodLeftRegularLEquiv A.ρ)).symm.toLinearMap
+
+variable {A α}
+
+@[simp]
+lemma finsuppToCoinvariantsTensorFree_single (i : α) (x : A) :
+    DFunLike.coe (F := (α →₀ A.V) →ₗ[k] (A.ρ.tprod (Representation.free k G α)).Coinvariants)
+      (finsuppToCoinvariantsTensorFree A α) (single i x) =
+      Coinvariants.mk _ (x ⊗ₜ single i (single (1 : G) (1 : k))) := by
+  simp [finsuppToCoinvariantsTensorFree, Coinvariants.map, ModuleCat.MonoidalCategory.tensorObj,
+    tensorObj_def]
+
+variable (A α)
+
+/-- Given a `k`-linear `G`-representation `(A, ρ)` and a type `α`, this is the linear equivalence
+`(A ⊗ (α →₀ k[G]))_G ≃ₗ[k] (α →₀ A)` sending
+`⟦a ⊗ single x (single g r)⟧ ↦ single x (r • ρ(g⁻¹)(a)).` -/
+@[simps! symm_apply]
+noncomputable abbrev coinvariantsTensorFreeLEquiv :
+    Coinvariants (A ⊗ free k G α).ρ ≃ₗ[k] (α →₀ A) :=
+  LinearEquiv.ofLinear (coinvariantsTensorFreeToFinsupp A α) (finsuppToCoinvariantsTensorFree A α)
+    (lhom_ext fun i x => by
+      simp [finsuppToCoinvariantsTensorFree_single i,
+        coinvariantsTensorFreeToFinsupp_mk_tmul_single x]) <|
+    Coinvariants.hom_ext <| TensorProduct.ext <| LinearMap.ext fun a => lhom_ext' fun i =>
+      lhom_ext fun g r => by
+        simp [coinvariantsTensorFreeToFinsupp_mk_tmul_single a,
+          finsuppToCoinvariantsTensorFree_single (A := A) i, TensorProduct.smul_tmul]
+
+@[simp]
+lemma coinvariantsTensorFreeLEquiv_apply (x : (A ⊗ free k G α).ρ.Coinvariants) :
+    DFunLike.coe (F := (A.ρ.tprod (Representation.free k G α)).Coinvariants →ₗ[k] α →₀ A)
+      (A.coinvariantsTensorFreeToFinsupp α) x = coinvariantsTensorFreeToFinsupp A α x := by
+  rfl
+
+end Finsupp
 end Rep