Equivalence between Rep k G and ModuleCat k[G]

In this file we show that the category of k-linear representations of a monoid G is equivalent to the category of modules over the monoid algebra k[G].

@[reducible, inline]

noncomputable abbrev Rep.diagonalSuccIsoTensorTrivial (k G : Type u) [Group G] [CommRing k] (n : ℕ) : diagonal k G (n + 1) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (leftRegular k G) (trivial k G ((Fin n → G) →₀ k))

An isomorphism of k-linear representations of G from k[Gⁿ⁺¹] to k[G] ⊗ₖ k[Gⁿ] (on which G acts by ρ(g₁)(g₂ ⊗ x) = (g₁ * g₂) ⊗ x) sending (g₀, ..., gₙ) to g₀ ⊗ (g₀⁻¹g₁, g₁⁻¹g₂, ..., gₙ₋₁⁻¹gₙ). The inverse sends g₀ ⊗ (g₁, ..., gₙ) to (g₀, g₀g₁, ..., g₀g₁...gₙ).

Equations

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

@[reducible, inline]

noncomputable abbrev Rep.diagonalSuccIsoFree (k G : Type u) [Group G] [CommRing k] (n : ℕ) : diagonal k G (n + 1) ≅ free k G (Fin n → G)

Representation isomorphism k[Gⁿ⁺¹] ≅ (Gⁿ →₀ k[G]), where the right-hand representation is defined pointwise by the left regular representation on k[G]. The map sends single (g₀, ..., gₙ) a ↦ single (g₀⁻¹g₁, ..., gₙ₋₁⁻¹gₙ) (single g₀ a).

Equations

• Rep.diagonalSuccIsoFree k G n = Rep.diagonalSuccIsoTensorTrivial k G n ≪≫ Rep.leftRegularTensorTrivialIsoFree k G (Fin n → G)

@[reducible, inline]

noncomputable abbrev Rep.diagonalHomEquiv (k G : Type u) [Group G] [CommRing k] (n : ℕ) (A : Rep k G) : (diagonal k G (n + 1) ⟶ A) ≃ₗ[k] (Fin n → G) → ↑A

Given a k-linear G-representation A, the set of representation morphisms Hom(k[Gⁿ⁺¹], A) is k-linearly isomorphic to the set of functions Gⁿ → A.

Equations

• Rep.diagonalHomEquiv k G n A = (CategoryTheory.Linear.homCongr k (Rep.diagonalSuccIsoFree k G n) (CategoryTheory.Iso.refl A)).trans (Rep.freeLiftLEquiv k G (Fin n → G) A)

The categorical equivalence Rep k G ≌ Module.{u} k[G].

theorem Rep.to_Module_monoidAlgebra_map_aux {k : Type u_1} {G : Type u_2} [CommRing k] [Monoid G] (V : Type u_3) (W : Type u_4) [AddCommGroup V] [AddCommGroup W] [Module k V] [Module k W] (ρ : G →* V →ₗ[k] V) (σ : G →* W →ₗ[k] W) (f : V →ₗ[k] W) (w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f) (r : MonoidAlgebra k G) (x : V) : f ((((MonoidAlgebra.lift k (V →ₗ[k] V) G) ρ) r) x) = (((MonoidAlgebra.lift k (W →ₗ[k] W) G) σ) r) (f x)

Auxiliary lemma for toModuleMonoidAlgebra.

noncomputable def Rep.toModuleMonoidAlgebraMap {k : Type u} {G : Type v} [CommRing k] [Monoid G] {V W : Rep k G} (f : V ⟶ W) : ModuleCat.of (MonoidAlgebra k G) V.ρ.asModule ⟶ ModuleCat.of (MonoidAlgebra k G) W.ρ.asModule

Auxiliary definition for toModuleMonoidAlgebra.

Equations

• Rep.toModuleMonoidAlgebraMap f = ModuleCat.ofHom (let __src := (Rep.Hom.hom f).toLinearMap; { toAddHom := __src.toAddHom, map_smul' := ⋯ })

noncomputable def Rep.toModuleMonoidAlgebra {k : Type u} {G : Type v} [CommRing k] [Monoid G] : CategoryTheory.Functor (Rep k G) (ModuleCat (MonoidAlgebra k G))

Functorially convert a representation of G into a module over k[G].

Equations

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

noncomputable def Rep.ofModuleMonoidAlgebra {k : Type u} {G : Type v} [CommRing k] [Monoid G] : CategoryTheory.Functor (ModuleCat (MonoidAlgebra k G)) (Rep k G)

Functorially convert a module over k[G] into a representation of G.

Equations

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

theorem Rep.ofModuleMonoidAlgebra_obj_coe {k : Type u} {G : Type v} [CommRing k] [Monoid G] (M : ModuleCat (MonoidAlgebra k G)) : ↑(ofModuleMonoidAlgebra.obj M) = RestrictScalars k (MonoidAlgebra k G) ↑M

theorem Rep.ofModuleMonoidAlgebra_obj_ρ {k : Type u} {G : Type v} [CommRing k] [Monoid G] (M : ModuleCat (MonoidAlgebra k G)) : (ofModuleMonoidAlgebra.obj M).ρ = Representation.ofModule ↑M

noncomputable def Rep.counitIsoAddEquiv {k : Type u} {G : Type v} [CommRing k] [Monoid G] {M : ModuleCat (MonoidAlgebra k G)} : ↑((ofModuleMonoidAlgebra.comp toModuleMonoidAlgebra).obj M) ≃+ ↑M

Auxiliary definition for equivalenceModuleMonoidAlgebra.

Equations

• Rep.counitIsoAddEquiv = id ((Representation.ofModule ↑M).asModuleEquiv.toAddEquiv.trans (RestrictScalars.addEquiv k (MonoidAlgebra k G) ↑M))

noncomputable def Rep.unitIsoAddEquiv {k : Type u} {G : Type v} [CommRing k] [Monoid G] {V : Rep k G} : ↑V ≃+ ↑((toModuleMonoidAlgebra.comp ofModuleMonoidAlgebra).obj V)

Auxiliary definition for equivalenceModuleMonoidAlgebra.

Equations

• Rep.unitIsoAddEquiv = id (V.ρ.asModuleEquiv.symm.toAddEquiv.trans (RestrictScalars.addEquiv k (MonoidAlgebra k G) V.ρ.asModule).symm)

noncomputable def Rep.counitIso {k : Type u} {G : Type v} [CommRing k] [Monoid G] (M : ModuleCat (MonoidAlgebra k G)) : (ofModuleMonoidAlgebra.comp toModuleMonoidAlgebra).obj M ≅ M

Auxiliary definition for equivalenceModuleMonoidAlgebra.

Equations

• Rep.counitIso M = (let __src := Rep.counitIsoAddEquiv; { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }).toModuleIso

theorem Rep.unit_iso_comm {k : Type u} {G : Type v} [CommRing k] [Monoid G] (V : Rep k G) (g : G) (x : ↑V) : unitIsoAddEquiv ((V.ρ g).toFun x) = ((ofModuleMonoidAlgebra.obj (toModuleMonoidAlgebra.obj V)).ρ g).toFun (unitIsoAddEquiv x)

noncomputable def Rep.unitIso {k : Type u} {G : Type v} [CommRing k] [Monoid G] (V : Rep k G) : V ≅ (toModuleMonoidAlgebra.comp ofModuleMonoidAlgebra).obj V

Auxiliary definition for equivalenceModuleMonoidAlgebra.

Equations

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

noncomputable def Rep.equivalenceModuleMonoidAlgebra {k : Type u} {G : Type v} [CommRing k] [Monoid G] : Rep k G ≌ ModuleCat (MonoidAlgebra k G)

The categorical equivalence Rep k G ≌ ModuleCat k[G].

Equations

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

instance Rep.instIsEquivalenceModuleCatMonoidAlgebraToModuleMonoidAlgebra {k : Type u} {G : Type v} [CommRing k] [Monoid G] : toModuleMonoidAlgebra.IsEquivalence

instance Rep.instIsEquivalenceModuleCatMonoidAlgebraOfModuleMonoidAlgebra {k : Type u} {G : Type v} [CommRing k] [Monoid G] : ofModuleMonoidAlgebra.IsEquivalence

instance Rep.instHasBinaryBiproducts {k : Type u} {G : Type v} [CommRing k] [Monoid G] : CategoryTheory.Limits.HasBinaryBiproducts (Rep k G)

instance Rep.instHasZeroObject {k : Type u} {G : Type v} [CommRing k] [Monoid G] : CategoryTheory.Limits.HasZeroObject (Rep k G)

instance Rep.instHasFiniteProducts {k : Type u} {G : Type v} [CommRing k] [Monoid G] : CategoryTheory.Limits.HasFiniteProducts (Rep k G)

@[implicit_reducible]

noncomputable instance Rep.instAbelian {k : Type u} {G : Type v} [CommRing k] [Monoid G] : CategoryTheory.Abelian (Rep k G)

Equations

• Rep.instAbelian = CategoryTheory.abelianOfEquivalence Rep.toModuleMonoidAlgebra

instance Rep.instEnoughProjectives {k G : Type u} [CommRing k] [Monoid G] : CategoryTheory.EnoughProjectives (Rep k G)

instance Rep.free_projective {k : Type u} {G : Type v} [CommRing k] [Monoid G] {α : Type (max w u)} : CategoryTheory.Projective (free k G α)

instance Rep.diagonal_succ_projective {k : Type u} [CommRing k] {G : Type u} [Group G] {n : ℕ} : CategoryTheory.Projective (diagonal k G (n + 1))

instance Rep.leftRegular_projective {k : Type u} [CommRing k] {G : Type u} [Group G] : CategoryTheory.Projective (leftRegular k G)

instance Rep.trivial_projective_of_subsingleton {k : Type u} [CommRing k] {G : Type u} [Group G] [Subsingleton G] : CategoryTheory.Projective (trivial k G k)