Coinvariants of a group representation

Given a commutative ring k and a monoid G, this file introduces the coinvariants of a k-linear G-representation (V, ρ).

We first define Representation.Coinvariants.ker, the submodule of V generated by elements of the form ρ g x - x for x : V, g : G. Then the coinvariants of (V, ρ) are the quotient of 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.

def Representation.Coinvariants.ker {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : Submodule k V

The submodule of a representation generated by elements of the form ρ g x - x.

def Representation.Coinvariants {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : Type u_3

The coinvariants of a representation, V ⧸ ⟨{ρ g x - x | g ∈ G, x ∈ V}⟩.

instance Representation.Coinvariants.instAddCommGroup {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : AddCommGroup ρ.Coinvariants

instance Representation.Coinvariants.instModule {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : Module k ρ.Coinvariants

theorem Representation.Coinvariants.sub_mem_ker {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} (g : G) (x : V) : (ρ g) x - x ∈ ker ρ

theorem Representation.Coinvariants.mem_ker_of_eq {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} (g : G) (x a : V) (h : (ρ g) x - x = a) : a ∈ ker ρ

def Representation.Coinvariants.mk {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : V →ₗ[k] ρ.Coinvariants

The quotient map from a representation to its coinvariants as a linear map.

theorem Representation.Coinvariants.mk_eq_iff {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) {x y : V} : (mk ρ) x = (mk ρ) y ↔ x - y ∈ ker ρ

theorem Representation.Coinvariants.mk_eq_zero {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) {x : V} : (mk ρ) x = 0 ↔ x ∈ ker ρ

theorem Representation.Coinvariants.mk_surjective {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : Function.Surjective ⇑(mk ρ)

@[simp]

theorem Representation.Coinvariants.mk_self_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (g : G) (x : V) : (mk ρ) ((ρ g) x) = (mk ρ) x

theorem Representation.Coinvariants.induction_on {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} {motive : ρ.Coinvariants → Prop} (x : ρ.Coinvariants) (h : ∀ (v : V), motive ((mk ρ) v)) : motive x

def Representation.Coinvariants.lift {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (ρ : Representation k G V) (f : V →ₗ[k] W) (h : ∀ (x : G), f ∘ₗ ρ x = f) : ρ.Coinvariants →ₗ[k] W

A G-invariant linear map induces a linear map out of the coinvariants of a G-representation.

@[simp]

theorem Representation.Coinvariants.lift_comp_mk {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (ρ : Representation k G V) (f : V →ₗ[k] W) (h : ∀ (x : G), f ∘ₗ ρ x = f) : lift ρ f h ∘ₗ mk ρ = f

@[simp]

theorem Representation.Coinvariants.lift_mk {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (ρ : Representation k G V) (f : V →ₗ[k] W) (h : ∀ (x : G), f ∘ₗ ρ x = f) (x : V) : (lift ρ f h) ((mk ρ) x) = f x

theorem Representation.Coinvariants.hom_ext {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {ρ : Representation k G V} {f g : ρ.Coinvariants →ₗ[k] W} (H : f ∘ₗ mk ρ = g ∘ₗ mk ρ) : f = g

theorem Representation.Coinvariants.hom_ext_iff {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {ρ : Representation k G V} {f g : ρ.Coinvariants →ₗ[k] W} : f = g ↔ f ∘ₗ mk ρ = g ∘ₗ mk ρ

noncomputable def Representation.Coinvariants.map {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (ρ : Representation k G V) (τ : Representation k G W) (f : V →ₗ[k] W) (hf : ∀ (g : G), f ∘ₗ ρ g = τ g ∘ₗ f) : ρ.Coinvariants →ₗ[k] τ.Coinvariants

Given G-representations on k-modules V, W, a linear map V →ₗ[k] W commuting with the representations induces a k-linear map between the coinvariants.

@[simp]

theorem Representation.Coinvariants.map_comp_mk {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {ρ : Representation k G V} {τ : Representation k G W} (f : V →ₗ[k] W) (hf : ∀ (g : G), f ∘ₗ ρ g = τ g ∘ₗ f) : map ρ τ f hf ∘ₗ mk ρ = mk τ ∘ₗ f

@[simp]

theorem Representation.Coinvariants.map_mk {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {ρ : Representation k G V} {τ : Representation k G W} (f : V →ₗ[k] W) (hf : ∀ (g : G), f ∘ₗ ρ g = τ g ∘ₗ f) (x : V) : (map ρ τ f hf) ((mk ρ) x) = (mk τ) (f x)

@[simp]

theorem Representation.Coinvariants.map_id {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : map ρ ρ LinearMap.id ⋯ = LinearMap.id

@[simp]

theorem Representation.Coinvariants.map_comp {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {X : Type u_5} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] [AddCommGroup X] [Module k X] {ρ : Representation k G V} {τ : Representation k G W} (υ : Representation k G X) (φ : V →ₗ[k] W) (ψ : W →ₗ[k] X) (H : ∀ (g : G), φ ∘ₗ ρ g = τ g ∘ₗ φ) (h : ∀ (g : G), ψ ∘ₗ τ g = υ g ∘ₗ ψ) : map τ υ ψ h ∘ₗ map ρ τ φ H = map ρ υ (ψ ∘ₗ φ) ⋯

theorem Representation.Coinvariants.le_comap_ker {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] (g : G) : ker (MonoidHom.comp ρ S.subtype) ≤ Submodule.comap (ρ g) (ker (MonoidHom.comp ρ S.subtype))

@[reducible, inline]

noncomputable abbrev Representation.toCoinvariantsKer {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] : Representation k G ↥(Coinvariants.ker (MonoidHom.comp ρ S.subtype))

Given a normal subgroup S ≤ G, a G-representation ρ restricts to a G-representation on the kernel of the quotient map to the coinvariants of ρ|_S.

noncomputable def Representation.toCoinvariants {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] : Representation k G (Coinvariants (MonoidHom.comp ρ S.subtype))

Given a normal subgroup S ≤ G, a G-representation ρ induces a G-representation on the coinvariants of ρ|_S.

@[simp]

theorem Representation.toCoinvariants_mk {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] (g : G) (x : V) : ((ρ.toCoinvariants S) g) ((Coinvariants.mk (MonoidHom.comp ρ S.subtype)) x) = (Coinvariants.mk (MonoidHom.comp ρ S.subtype)) ((ρ g) x)

instance Representation.instIsTrivialSubtypeMemSubgroupCoinvariantsCompLinearMapIdSubtypeToCoinvariants {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] : IsTrivial (MonoidHom.comp (ρ.toCoinvariants S) S.subtype)

@[reducible, inline]

noncomputable abbrev Representation.quotientToCoinvariants {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] : Representation k (G ⧸ S) (Coinvariants (MonoidHom.comp ρ S.subtype))

Given a normal subgroup S ≤ G, a G-representation ρ induces a G ⧸ S-representation on the coinvariants of ρ|_S.

noncomputable def Representation.coinvariantsToFinsupp {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (α : Type u_9) : (ρ.finsupp α).Coinvariants →ₗ[k] α →₀ ρ.Coinvariants

Given a G-representation (V, ρ) and a type α, this is the map (α →₀ V)_G →ₗ (α →₀ V_G) sending ⟦single a v⟧ ↦ single a ⟦v⟧.

@[simp]

theorem Representation.coinvariantsToFinsupp_mk_single {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} {α : Type u_9} (x : α) (a : V) : (ρ.coinvariantsToFinsupp α) ((Coinvariants.mk (ρ.finsupp α)) fun₀ | x => a) = fun₀ | x => (Coinvariants.mk ρ) a

noncomputable def Representation.finsuppToCoinvariants {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (α : Type u_9) : (α →₀ ρ.Coinvariants) →ₗ[k] (ρ.finsupp α).Coinvariants

Given a G-representation (V, ρ) and a type α, this is the map (α →₀ V_G) →ₗ (α →₀ V)_G sending single a ⟦v⟧ ↦ ⟦single a v⟧.

@[simp]

theorem Representation.finsuppToCoinvariants_single_mk {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} {α : Type u_9} (a : α) (x : V) : ((ρ.finsuppToCoinvariants α) fun₀ | a => (Coinvariants.mk ρ) x) = (Coinvariants.mk (ρ.finsupp α)) fun₀ | a => x

noncomputable def Representation.coinvariantsFinsuppLEquiv {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (α : Type u_9) : (ρ.finsupp α).Coinvariants ≃ₗ[k] α →₀ ρ.Coinvariants

Given a G-representation (V, ρ) and a type α, this is the linear equivalence (α →₀ V)_G ≃ₗ (α →₀ V_G) sending ⟦single a v⟧ ↦ single a ⟦v⟧.

@[simp]

theorem Representation.coinvariantsFinsuppLEquiv_symm_apply {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (α : Type u_9) (a : α →₀ ρ.Coinvariants) : (ρ.coinvariantsFinsuppLEquiv α).symm a = (ρ.finsuppToCoinvariants α) a

@[simp]

theorem Representation.coinvariantsFinsuppLEquiv_apply {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] {ρ : Representation k G V} {α : Type u_9} (x : (ρ.finsupp α).Coinvariants) : (ρ.coinvariantsFinsuppLEquiv α) x = (ρ.coinvariantsToFinsupp α) x

@[simp]

theorem Representation.Coinvariants.mk_inv_tmul {k : Type u_6} {G : Type u_7} {V : Type u_8} {W : Type u_9} [CommRing k] [Group G] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (ρ : Representation k G V) (τ : Representation k G W) (x : V) (y : W) (g : G) : (mk (ρ.tprod τ)) ((ρ g⁻¹) x ⊗ₜ[k] y) = (mk (ρ.tprod τ)) (x ⊗ₜ[k] (τ g) y)

@[simp]

theorem Representation.Coinvariants.mk_tmul_inv {k : Type u_6} {G : Type u_7} {V : Type u_8} {W : Type u_9} [CommRing k] [Group G] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (ρ : Representation k G V) (τ : Representation k G W) (x : V) (y : W) (g : G) : (mk (ρ.tprod τ)) (x ⊗ₜ[k] (τ g⁻¹) y) = (mk (ρ.tprod τ)) ((ρ g) x ⊗ₜ[k] y)

noncomputable def Representation.ofCoinvariantsTprodLeftRegular {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : (ρ.tprod (leftRegular k G)).Coinvariants →ₗ[k] V

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).

@[simp]

theorem Representation.ofCoinvariantsTprodLeftRegular_mk_tmul_single {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (x : V) (g : G) (r : k) : ρ.ofCoinvariantsTprodLeftRegular ((Coinvariants.mk (ρ.tprod (leftRegular k G))) (x ⊗ₜ[k] fun₀ | g => r)) = r • (ρ g⁻¹) x

noncomputable def Representation.coinvariantsTprodLeftRegularLEquiv {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : (ρ.tprod (leftRegular k G)).Coinvariants ≃ₗ[k] V

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).

@[simp]

theorem Representation.coinvariantsTprodLeftRegularLEquiv_symm_apply {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (a : V) : ρ.coinvariantsTprodLeftRegularLEquiv.symm a = (Coinvariants.mk (ρ.tprod (leftRegular k G))) (a ⊗ₜ[k] fun₀ | 1 => 1)

@[simp]

theorem Representation.coinvariantsTprodLeftRegularLEquiv_apply {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (x : (ρ.tprod (leftRegular k G)).Coinvariants) : ρ.coinvariantsTprodLeftRegularLEquiv x = ρ.ofCoinvariantsTprodLeftRegular x

@[reducible, inline]

abbrev Rep.toCoinvariantsKer {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] : Rep k G

Given a normal subgroup S ≤ G, a G-representation A restricts to a G-representation on the kernel of the quotient map to the S-coinvariants A_S.

@[reducible, inline]

abbrev Rep.toCoinvariants {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] : Rep k G

Given a normal subgroup S ≤ G, a G-representation A induces a G-representation on the S-coinvariants A_S.

def Rep.toCoinvariantsMkQ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] : A ⟶ A.toCoinvariants S

The quotient map A → A_S as a representation morphism.

@[simp]

theorem Rep.toCoinvariantsMkQ_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] : ModuleCat.Hom.hom (A.toCoinvariantsMkQ S).hom = Representation.Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)

@[reducible, inline]

abbrev Rep.quotientToCoinvariants {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] : Rep k (G ⧸ S)

Given a normal subgroup S ≤ G, a G-representation ρ induces a G ⧸ S-representation on the coinvariants of ρ|_S.

def Rep.coinvariantsShortComplex {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] : CategoryTheory.ShortComplex (Rep k G)

Given a normal subgroup S ≤ G, a G-representation A induces a short exact sequence of G-representations 0 ⟶ Ker(mk) ⟶ A ⟶ A_S ⟶ 0 where mk is the quotient map to the S-coinvariants A_S.

@[simp]

theorem Rep.coinvariantsShortComplex_X₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] : (A.coinvariantsShortComplex S).X₂ = A

@[simp]

theorem Rep.coinvariantsShortComplex_f {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] : (A.coinvariantsShortComplex S).f = A.subtype (Representation.Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)) ⋯

@[simp]

theorem Rep.coinvariantsShortComplex_X₃ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] : (A.coinvariantsShortComplex S).X₃ = A.toCoinvariants S

@[simp]

theorem Rep.coinvariantsShortComplex_X₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] : (A.coinvariantsShortComplex S).X₁ = A.toCoinvariantsKer S

@[simp]

theorem Rep.coinvariantsShortComplex_g {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] : (A.coinvariantsShortComplex S).g = A.toCoinvariantsMkQ S

theorem Rep.coinvariantsShortComplex_shortExact {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] : (A.coinvariantsShortComplex S).ShortExact

noncomputable def Rep.coinvariantsFunctor (k G : Type u) [CommRing k] [Monoid G] : CategoryTheory.Functor (Rep k G) (ModuleCat k)

The functor sending a representation to its coinvariants.

@[simp]

theorem Rep.coinvariantsFunctor_obj_carrier (k G : Type u) [CommRing k] [Monoid G] (A : Rep k G) : ↑((coinvariantsFunctor k G).obj A) = A.ρ.Coinvariants

@[simp]

theorem Rep.coinvariantsFunctor_map_hom (k G : Type u) [CommRing k] [Monoid G] {X✝ Y✝ : Rep k G} (f : X✝ ⟶ Y✝) : ModuleCat.Hom.hom ((coinvariantsFunctor k G).map f) = Representation.Coinvariants.map X✝.ρ Y✝.ρ (ModuleCat.Hom.hom f.hom) ⋯

noncomputable def Rep.coinvariantsMk (k G : Type u) [CommRing k] [Monoid G] : Action.forget (ModuleCat k) G ⟶ coinvariantsFunctor k G

The quotient map from a representation to its coinvariants induces a natural transformation from the forgetful functor Rep k G ⥤ ModuleCat k to the coinvariants functor.

@[simp]

theorem Rep.coinvariantsMk_app_hom (k G : Type u) [CommRing k] [Monoid G] (X : Rep k G) : ModuleCat.Hom.hom ((coinvariantsMk k G).app X) = Representation.Coinvariants.mk X.ρ

instance Rep.instEpiModuleCatAppActionCoinvariantsMk (k G : Type u) [CommRing k] [Monoid G] (X : Rep k G) : CategoryTheory.Epi ((coinvariantsMk k G).app X)

theorem Rep.coinvariantsFunctor_hom_ext {k G : Type u} [CommRing k] [Monoid G] {A : Rep k G} {M : ModuleCat k} {f g : (coinvariantsFunctor k G).obj A ⟶ M} (hfg : CategoryTheory.CategoryStruct.comp ((coinvariantsMk k G).app A) f = CategoryTheory.CategoryStruct.comp ((coinvariantsMk k G).app A) g) : f = g

theorem Rep.coinvariantsFunctor_hom_ext_iff {k G : Type u} [CommRing k] [Monoid G] {A : Rep k G} {M : ModuleCat k} {f g : (coinvariantsFunctor k G).obj A ⟶ M} : f = g ↔ CategoryTheory.CategoryStruct.comp ((coinvariantsMk k G).app A) f = CategoryTheory.CategoryStruct.comp ((coinvariantsMk k G).app A) g

@[reducible, inline]

noncomputable abbrev Rep.desc {k G : Type u} [CommRing k] [Monoid G] {A B : Rep k G} [B.ρ.IsTrivial] (f : A ⟶ B) : (coinvariantsFunctor k G).obj A ⟶ B.V

The linear map underlying a G-representation morphism A ⟶ B, where B has the trivial representation, factors through A_G.

instance Rep.instAdditiveModuleCatCoinvariantsFunctor (k G : Type u) [CommRing k] [Monoid G] : (coinvariantsFunctor k G).Additive

instance Rep.instLinearModuleCatCoinvariantsFunctor (k G : Type u) [CommRing k] [Monoid G] : CategoryTheory.Functor.Linear k (coinvariantsFunctor k G)

noncomputable def Rep.coinvariantsAdjunction (k G : Type u) [CommRing k] [Monoid G] : coinvariantsFunctor k G ⊣ trivialFunctor k G

The adjunction between the functor sending a representation to its coinvariants and the functor equipping a module with the trivial representation.

@[simp]

theorem Rep.coinvariantsAdjunction_counit_app (k G : Type u) [CommRing k] [Monoid G] (X : ModuleCat k) : (coinvariantsAdjunction k G).counit.app X = desc (CategoryTheory.CategoryStruct.id ((trivialFunctor k G).obj X))

@[simp]

theorem Rep.coinvariantsAdjunction_unit_app_hom (k G : Type u) [CommRing k] [Monoid G] (X : Rep k G) : ((coinvariantsAdjunction k G).unit.app X).hom = (coinvariantsMk k G).app X

@[simp]

theorem Rep.coinvariantsAdjunction_homEquiv_apply_hom (k G : Type u) [CommRing k] [Monoid G] {X : Rep k G} {Y : ModuleCat k} (f : (coinvariantsFunctor k G).obj X ⟶ Y) : (((coinvariantsAdjunction k G).homEquiv X Y) f).hom = CategoryTheory.CategoryStruct.comp ((coinvariantsMk k G).app X) f

@[simp]

theorem Rep.coinvariantsAdjunction_homEquiv_symm_apply_hom (k G : Type u) [CommRing k] [Monoid G] {X : Rep k G} {Y : ModuleCat k} (f : X ⟶ (trivialFunctor k G).obj Y) : ((coinvariantsAdjunction k G).homEquiv X Y).symm f = desc f

instance Rep.instPreservesZeroMorphismsModuleCatCoinvariantsFunctor (k G : Type u) [CommRing k] [Monoid G] : (coinvariantsFunctor k G).PreservesZeroMorphisms

instance Rep.instIsLeftAdjointModuleCatCoinvariantsFunctor (k G : Type u) [CommRing k] [Monoid G] : (coinvariantsFunctor k G).IsLeftAdjoint

@[reducible, inline]

noncomputable abbrev Rep.coinvariantsTensor (k G : Type u) [CommRing k] [Monoid G] : CategoryTheory.Functor (Rep k G) (CategoryTheory.Functor (Rep k G) (ModuleCat k))

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.

@[reducible, inline]

noncomputable abbrev Rep.coinvariantsTensorMk {k G : Type u} [CommRing k] [Monoid G] (A B : Rep k G) : ↑A.V →ₗ[k] ↑B.V →ₗ[k] ↑(((coinvariantsTensor k G).obj A).obj B)

The bilinear map sending a : A, b : B to ⟦a ⊗ₜ b⟧ in (A ⊗[k] B)_G.

theorem Rep.coinvariantsTensorMk_apply {k G : Type u} [CommRing k] [Monoid G] {A B : Rep k G} (a : ↑A.V) (b : ↑B.V) : ((A.coinvariantsTensorMk B) a) b = (Representation.Coinvariants.mk (((CategoryTheory.MonoidalCategory.curriedTensor (Rep k G)).obj A).obj B).ρ) (a ⊗ₜ[k] b)

theorem Rep.coinvariantsTensor_hom_ext {k G : Type u} [CommRing k] [Monoid G] {A B : Rep k G} {M : ModuleCat k} {f g : ((coinvariantsTensor k G).obj A).obj B ⟶ M} (hfg : (A.coinvariantsTensorMk B).compr₂ (ModuleCat.Hom.hom f) = (A.coinvariantsTensorMk B).compr₂ (ModuleCat.Hom.hom g)) : f = g

theorem Rep.coinvariantsTensor_hom_ext_iff {k G : Type u} [CommRing k] [Monoid G] {A B : Rep k G} {M : ModuleCat k} {f g : ((coinvariantsTensor k G).obj A).obj B ⟶ M} : f = g ↔ (A.coinvariantsTensorMk B).compr₂ (ModuleCat.Hom.hom f) = (A.coinvariantsTensorMk B).compr₂ (ModuleCat.Hom.hom g)

instance Rep.instAdditiveModuleCatObjFunctorCoinvariantsTensor {k G : Type u} [CommRing k] [Monoid G] (A : Rep k G) : ((coinvariantsTensor k G).obj A).Additive

instance Rep.instLinearModuleCatObjFunctorCoinvariantsTensor {k G : Type u} [CommRing k] [Monoid G] (A : Rep k G) : CategoryTheory.Functor.Linear k ((coinvariantsTensor k G).obj A)

noncomputable def Rep.quotientToCoinvariantsFunctor (k : Type u) {G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.Normal] : CategoryTheory.Functor (Rep k G) (Rep k (G ⧸ S))

Given a normal subgroup S ≤ G, this is the functor sending a G-representation A to the G ⧸ S-representation it induces on A_S.

@[simp]

theorem Rep.quotientToCoinvariantsFunctor_obj_V (k : Type u) {G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.Normal] (X : Rep k G) : ((quotientToCoinvariantsFunctor k S).obj X).V = ModuleCat.of k ↑(X.toCoinvariants S).V

@[simp]

theorem Rep.quotientToCoinvariantsFunctor_map_hom (k : Type u) {G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.Normal] {X Y : Rep k G} (f : X ⟶ Y) : ((quotientToCoinvariantsFunctor k S).map f).hom = (coinvariantsFunctor k ↥S).map ((Action.res (ModuleCat k) S.subtype).map f)

noncomputable def Rep.coinvariantsTensorFreeToFinsupp {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (α : Type u) [DecidableEq α] : (CategoryTheory.MonoidalCategoryStruct.tensorObj A (free k G α)).ρ.Coinvariants →ₗ[k] α →₀ ↑A.V

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)).

@[simp]

theorem Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {α : Type u} [DecidableEq α] (x : ↑A.V) (i : α) (g : G) (r : k) : (A.coinvariantsTensorFreeToFinsupp α) ((Representation.Coinvariants.mk (A.ρ.tprod (Representation.free k G α))) (x ⊗ₜ[k] fun₀ | i => fun₀ | g => r)) = fun₀ | i => r • (A.ρ g⁻¹) x

noncomputable def Rep.finsuppToCoinvariantsTensorFree {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (α : Type u) [DecidableEq α] : (α →₀ ↑A.V) →ₗ[k] (CategoryTheory.MonoidalCategoryStruct.tensorObj A (free k G α)).ρ.Coinvariants

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⟧.

@[simp]

theorem Rep.finsuppToCoinvariantsTensorFree_single {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {α : Type u} [DecidableEq α] (i : α) (x : ↑A.V) : ((A.finsuppToCoinvariantsTensorFree α) fun₀ | i => x) = (Representation.Coinvariants.mk (A.ρ.tprod (Representation.free k G α))) (x ⊗ₜ[k] fun₀ | i => fun₀ | 1 => 1)

@[reducible, inline]

noncomputable abbrev Rep.coinvariantsTensorFreeLEquiv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (α : Type u) [DecidableEq α] : (CategoryTheory.MonoidalCategoryStruct.tensorObj A (free k G α)).ρ.Coinvariants ≃ₗ[k] α →₀ ↑A.V

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)).

@[simp]

theorem Rep.coinvariantsTensorFreeLEquiv_symm_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (α : Type u) [DecidableEq α] (a : α →₀ ↑A.V) : (A.coinvariantsTensorFreeLEquiv α).symm a = (A.finsuppToCoinvariantsTensorFree α) a

@[simp]

theorem Rep.coinvariantsTensorFreeLEquiv_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (α : Type u) [DecidableEq α] (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj A (free k G α)).ρ.Coinvariants) : (A.coinvariantsTensorFreeToFinsupp α) x = (A.coinvariantsTensorFreeToFinsupp α) x