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

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.

Equations

• Representation.Coinvariants.ker ρ = Submodule.span k (Set.range fun (gv : G × V) => (ρ gv.1) gv.2 - gv.2)

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}⟩.

Equations

• ρ.Coinvariants = (V ⧸ Representation.Coinvariants.ker ρ)

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

Equations

• Representation.Coinvariants.instAddCommGroup ρ = inferInstanceAs (AddCommGroup (V ⧸ Representation.Coinvariants.ker ρ))

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

Equations

• Representation.Coinvariants.instModule ρ = inferInstanceAs (Module k (V ⧸ Representation.Coinvariants.ker ρ))

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.

Equations

• Representation.Coinvariants.mk ρ = (Representation.Coinvariants.ker ρ).mkQ

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.

Equations

• Representation.Coinvariants.lift ρ f h = (Representation.Coinvariants.ker ρ).liftQ f ⋯

@[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.

Equations

• Representation.Coinvariants.map ρ τ f hf = Representation.Coinvariants.lift ρ (Representation.Coinvariants.mk τ ∘ₗ f) ⋯

@[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 ρ υ (ψ ∘ₗ φ) ⋯

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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• Rep.coinvariantsMk k G = { app := fun (X : Rep k G) => ModuleCat.ofHom (Representation.Coinvariants.mk X.ρ), naturality := ⋯ }

@[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.

Equations

• Rep.desc f = ModuleCat.ofHom (Representation.Coinvariants.lift A.ρ (ModuleCat.Hom.hom f.hom) ⋯)

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.

Equations

• One or more equations did not get rendered due to their size.

@[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