Rep k G is the category of k-linear representations of G.

If V : Rep k G, there is a coercion that allows you to treat V as a type, and this type comes equipped with a Module k V instance. Also V.ρ gives the homomorphism G →* (V →ₗ[k] V).

Conversely, given a homomorphism ρ : G →* (V →ₗ[k] V), you can construct the bundled representation as Rep.of ρ.

We construct the categorical equivalence Rep k G ≌ ModuleCat (MonoidAlgebra k G). We verify that Rep k G is a k-linear abelian symmetric monoidal category with all (co)limits.

@[reducible, inline]

noncomputable abbrev Rep (k G : Type u) [Ring k] [Monoid G] : Type (u + 1)

The category of k-linear representations of a monoid G.

Equations

• Rep k G = Action (ModuleCat k) G

noncomputable instance instLinearRep (k G : Type u) [CommRing k] [Monoid G] : CategoryTheory.Linear k (Rep k G)

Equations

• instLinearRep k G = inferInstance

noncomputable instance Rep.instCoeSortType {k G : Type u} [CommRing k] [Monoid G] : CoeSort (Rep k G) (Type u)

Equations

• Rep.instCoeSortType = { coe := fun (V : Rep k G) => ↑V.V }

noncomputable instance Rep.instAddCommGroupCarrierVModuleCat {k G : Type u} [CommRing k] [Monoid G] (V : Rep k G) : AddCommGroup ↑V.V

Equations

• V.instAddCommGroupCarrierVModuleCat = id inferInstance

noncomputable instance Rep.instModuleCarrierVModuleCat {k G : Type u} [CommRing k] [Monoid G] (V : Rep k G) : Module k ↑V.V

Equations

• V.instModuleCarrierVModuleCat = id inferInstance

noncomputable def Rep.ρ {k G : Type u} [CommRing k] [Monoid G] (V : Rep k G) : Representation k G ↑V.V

Specialize the existing Action.ρ, changing the type to Representation k G V.

Equations

• V.ρ = V.V.endRingEquiv.toMonoidHom.comp V.ρ

@[reducible, inline]

noncomputable abbrev Rep.of {k G : Type u} [CommRing k] [Monoid G] {V : Type u} [AddCommGroup V] [Module k V] (ρ : G →* V →ₗ[k] V) : Rep k G

Lift an unbundled representation to Rep.

Equations

• Rep.of ρ = { V := ModuleCat.of k V, ρ := (ModuleCat.of k V).endRingEquiv.symm.toMonoidHom.comp ρ }

theorem Rep.coe_of {k G : Type u} [CommRing k] [Monoid G] {V : Type u} [AddCommGroup V] [Module k V] (ρ : G →* V →ₗ[k] V) : ↑(of ρ).V = V

@[simp]

theorem Rep.of_ρ {k G : Type u} [CommRing k] [Monoid G] {V : Type u} [AddCommGroup V] [Module k V] (ρ : G →* V →ₗ[k] V) : (of ρ).ρ = ρ

theorem Rep.Action_ρ_eq_ρ {k G : Type u} [CommRing k] [Monoid G] {A : Rep k G} : A.ρ = A.V.endRingEquiv.symm.toMonoidHom.comp A.ρ

@[simp]

theorem Rep.ρ_hom {k G : Type u} [CommRing k] [Monoid G] {X : Rep k G} (g : G) : ModuleCat.Hom.hom (X.ρ g) = X.ρ g

@[simp]

theorem Rep.ofHom_ρ {k G : Type u} [CommRing k] [Monoid G] {X : Rep k G} (g : G) : ModuleCat.ofHom (X.ρ g) = X.ρ g

@[deprecated Representation.inv_self_apply (since := "2025-05-09")]

theorem Rep.ρ_inv_self_apply {k : Type u} [CommRing k] {G : Type u} [Group G] (A : Rep k G) (g : G) (x : ↑A.V) : (A.ρ g⁻¹) ((A.ρ g) x) = x

@[deprecated Representation.self_inv_apply (since := "2025-05-09")]

theorem Rep.ρ_self_inv_apply {k : Type u} [CommRing k] {G : Type u} [Group G] {A : Rep k G} (g : G) (x : ↑A.V) : (A.ρ g) ((A.ρ g⁻¹) x) = x

theorem Rep.hom_comm_apply {k G : Type u} [CommRing k] [Monoid G] {A B : Rep k G} (f : A ⟶ B) (g : G) (x : ↑A.V) : (CategoryTheory.ConcreteCategory.hom f.hom) ((A.ρ g) x) = (B.ρ g) ((CategoryTheory.ConcreteCategory.hom f.hom) x)

@[reducible, inline]

noncomputable abbrev Rep.trivial (k G : Type u) [CommRing k] [Monoid G] (V : Type u) [AddCommGroup V] [Module k V] : Rep k G

The trivial k-linear G-representation on a k-module V.

Equations

• Rep.trivial k G V = Rep.of (Representation.trivial k G V)

theorem Rep.trivial_def {k G : Type u} [CommRing k] [Monoid G] {V : Type u} [AddCommGroup V] [Module k V] (g : G) : (trivial k G V).ρ g = LinearMap.id

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

The functor equipping a module with the trivial representation.

Equations

• Rep.trivialFunctor k G = { obj := fun (V : ModuleCat k) => Rep.trivial k G ↑V, map := fun {X Y : ModuleCat k} (f : X ⟶ Y) => { hom := f, comm := ⋯ }, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem Rep.trivialFunctor_map_hom (k G : Type u) [CommRing k] [Monoid G] {X✝ Y✝ : ModuleCat k} (f : X✝ ⟶ Y✝) : ((trivialFunctor k G).map f).hom = f

@[simp]

theorem Rep.trivialFunctor_obj_V (k G : Type u) [CommRing k] [Monoid G] (V : ModuleCat k) : ((trivialFunctor k G).obj V).V = V

@[reducible, inline]

noncomputable abbrev Rep.IsTrivial {k G : Type u} [CommRing k] [Monoid G] (A : Rep k G) : Prop

A predicate for representations that fix every element.

Equations

• A.IsTrivial = A.ρ.IsTrivial

instance Rep.instIsTrivialObjModuleCatTrivialFunctor {k G : Type u} [CommRing k] [Monoid G] (X : ModuleCat k) : ((trivialFunctor k G).obj X).IsTrivial

instance Rep.instIsTrivialTrivial {k G : Type u} [CommRing k] [Monoid G] {V : Type u} [AddCommGroup V] [Module k V] : (trivial k G V).IsTrivial

instance Rep.instIsTrivialOfOfIsTrivial {k G : Type u} [CommRing k] [Monoid G] {V : Type u} [AddCommGroup V] [Module k V] (ρ : Representation k G V) [ρ.IsTrivial] : (of ρ).IsTrivial

instance Rep.instIsTrivialCarrierVModuleCatOfCompLinearMapIdρ {k G : Type u} [CommRing k] [Monoid G] {H V : Type u} [Group H] [AddCommGroup V] [Module k V] (ρ : Representation k H V) (f : G →* H) [Representation.IsTrivial (MonoidHom.comp ρ f)] : Representation.IsTrivial (MonoidHom.comp (of ρ).ρ f)

@[reducible, inline]

noncomputable abbrev Rep.ofQuotient {k : Type u} [CommRing k] {G : Type u} [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : Rep k (G ⧸ S)

Given a normal subgroup S ≤ G, a G-representation ρ which is trivial on S factors through G ⧸ S.

Equations

• A.ofQuotient S = Rep.of (A.ρ.ofQuotient S)

@[reducible, inline]

noncomputable abbrev Rep.resOfQuotientIso {k : Type u} [CommRing k] {G : Type u} [Group G] (A : Rep k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : (Action.res (ModuleCat k) (QuotientGroup.mk' S)).obj (A.ofQuotient S) ≅ A

A G-representation A on which a normal subgroup S ≤ G acts trivially induces a G ⧸ S-representation on A, and composing this with the quotient map G → G ⧸ S gives the original representation by definition. Useful for typechecking.

Equations

• A.resOfQuotientIso S = CategoryTheory.Iso.refl ((Action.res (ModuleCat k) (QuotientGroup.mk' S)).obj (A.ofQuotient S))

@[reducible, inline]

noncomputable abbrev Rep.subrepresentation {k G : Type u} [CommRing k] [Monoid G] (A : Rep k G) (W : Submodule k ↑A.V) (le_comap : ∀ (g : G), W ≤ Submodule.comap (A.ρ g) W) : Rep k G

Given a k-linear G-representation (V, ρ), this is the representation defined by restricting ρ to a G-invariant k-submodule of V.

Equations

• A.subrepresentation W le_comap = Rep.of (A.ρ.subrepresentation W le_comap)

noncomputable def Rep.subtype {k G : Type u} [CommRing k] [Monoid G] (A : Rep k G) (W : Submodule k ↑A.V) (le_comap : ∀ (g : G), W ≤ Submodule.comap (A.ρ g) W) : A.subrepresentation W le_comap ⟶ A

The natural inclusion of a subrepresentation into the ambient representation.

Equations

• A.subtype W le_comap = { hom := ModuleCat.ofHom W.subtype, comm := ⋯ }

@[simp]

theorem Rep.subtype_hom {k G : Type u} [CommRing k] [Monoid G] (A : Rep k G) (W : Submodule k ↑A.V) (le_comap : ∀ (g : G), W ≤ Submodule.comap (A.ρ g) W) : (A.subtype W le_comap).hom = ModuleCat.ofHom W.subtype

@[reducible, inline]

noncomputable abbrev Rep.quotient {k G : Type u} [CommRing k] [Monoid G] (A : Rep k G) (W : Submodule k ↑A.V) (le_comap : ∀ (g : G), W ≤ Submodule.comap (A.ρ g) W) : Rep k G

Given a k-linear G-representation (V, ρ) and a G-invariant k-submodule W ≤ V, this is the representation induced on V ⧸ W by ρ.

Equations

• A.quotient W le_comap = Rep.of (A.ρ.quotient W le_comap)

noncomputable def Rep.mkQ {k G : Type u} [CommRing k] [Monoid G] (A : Rep k G) (W : Submodule k ↑A.V) (le_comap : ∀ (g : G), W ≤ Submodule.comap (A.ρ g) W) : A ⟶ A.quotient W le_comap

The natural projection from a representation to its quotient by a subrepresentation.

Equations

• A.mkQ W le_comap = { hom := ModuleCat.ofHom W.mkQ, comm := ⋯ }

@[simp]

theorem Rep.mkQ_hom {k G : Type u} [CommRing k] [Monoid G] (A : Rep k G) (W : Submodule k ↑A.V) (le_comap : ∀ (g : G), W ≤ Submodule.comap (A.ρ g) W) : (A.mkQ W le_comap).hom = ModuleCat.ofHom W.mkQ

instance Rep.instPreservesLimitsModuleCatForget₂ {k G : Type u} [CommRing k] [Monoid G] : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ (Rep k G) (ModuleCat k))

instance Rep.instPreservesColimitsModuleCatForget₂ {k G : Type u} [CommRing k] [Monoid G] : CategoryTheory.Limits.PreservesColimits (CategoryTheory.forget₂ (Rep k G) (ModuleCat k))

theorem Rep.epi_iff_surjective {k G : Type u} [CommRing k] [Monoid G] {A B : Rep k G} (f : A ⟶ B) : CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f.hom)

theorem Rep.mono_iff_injective {k G : Type u} [CommRing k] [Monoid G] {A B : Rep k G} (f : A ⟶ B) : CategoryTheory.Mono f ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f.hom)

@[simp]

theorem Rep.tensor_ρ {k G : Type u} [CommRing k] [Monoid G] {A B : Rep k G} : (CategoryTheory.MonoidalCategoryStruct.tensorObj A B).ρ = A.ρ.tprod B.ρ

@[simp]

theorem Rep.res_obj_ρ {k G : Type u} [CommRing k] [Monoid G] {H : Type u} [Monoid H] (f : G →* H) (A : Rep k H) (g : G) : (ρ ((Action.res (ModuleCat k) f).obj A)) g = A.ρ (f g)

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

The monoidal functor sending a type H with a G-action to the induced k-linear G-representation on k[H].

Equations

• Rep.linearization k G = (ModuleCat.free k).mapAction G

noncomputable instance Rep.instMonoidalActionTypeLinearization (k G : Type u) [CommRing k] [Monoid G] : (linearization k G).Monoidal

Equations

• Rep.instMonoidalActionTypeLinearization k G = id inferInstance

@[simp]

theorem Rep.coe_linearization_obj {k G : Type u} [CommRing k] [Monoid G] (X : Action (Type u) G) : ↑((linearization k G).obj X).V = (X.V →₀ k)

theorem Rep.linearization_obj_ρ {k G : Type u} [CommRing k] [Monoid G] (X : Action (Type u) G) (g : G) : ((linearization k G).obj X).ρ g = Finsupp.lmapDomain k k (X.ρ g)

@[simp]

theorem Rep.coe_linearization_obj_ρ {k G : Type u} [CommRing k] [Monoid G] (X : Action (Type u) G) (g : G) : ((linearization k G).obj X).ρ g = Finsupp.lmapDomain k k (X.ρ g)

theorem Rep.linearization_single {k G : Type u} [CommRing k] [Monoid G] (X : Action (Type u) G) (g : G) (x : X.V) (r : k) : (((linearization k G).obj X).ρ g) (Finsupp.single x r) = Finsupp.single (X.ρ g x) r

@[deprecated "Use `Rep.linearization_single` instead" (since := "2025-06-02")]

theorem Rep.linearization_of {k G : Type u} [CommRing k] [Monoid G] (X : Action (Type u) G) (g : G) (x : X.V) : (((linearization k G).obj X).ρ g) (Finsupp.single x 1) = Finsupp.single (X.ρ g x) 1

@[simp]

theorem Rep.linearization_map_hom {k G : Type u} [CommRing k] [Monoid G] {X Y : Action (Type u) G} (f : X ⟶ Y) : ((linearization k G).map f).hom = ModuleCat.ofHom (Finsupp.lmapDomain k k f.hom)

theorem Rep.linearization_map_hom_single {k G : Type u} [CommRing k] [Monoid G] {X Y : Action (Type u) G} (f : X ⟶ Y) (x : X.V) (r : k) : (CategoryTheory.ConcreteCategory.hom ((linearization k G).map f).hom) (Finsupp.single x r) = Finsupp.single (f.hom x) r

@[simp]

theorem Rep.linearization_μ_hom {k G : Type u} [CommRing k] [Monoid G] (X Y : Action (Type u) G) : (CategoryTheory.Functor.LaxMonoidal.μ (linearization k G) X Y).hom = ModuleCat.ofHom ↑(finsuppTensorFinsupp' k X.V Y.V)

@[simp]

theorem Rep.linearization_δ_hom {k G : Type u} [CommRing k] [Monoid G] (X Y : Action (Type u) G) : (CategoryTheory.Functor.OplaxMonoidal.δ (linearization k G) X Y).hom = ModuleCat.ofHom ↑(finsuppTensorFinsupp' k X.V Y.V).symm

@[simp]

theorem Rep.linearization_ε_hom {k G : Type u} [CommRing k] [Monoid G] : (CategoryTheory.Functor.LaxMonoidal.ε (linearization k G)).hom = ModuleCat.ofHom (Finsupp.lsingle PUnit.unit)

theorem Rep.linearization_η_hom_apply {k G : Type u} [CommRing k] [Monoid G] (r : k) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.OplaxMonoidal.η (linearization k G)).hom) (Finsupp.single PUnit.unit r) = r

noncomputable def Rep.linearizationTrivialIso (k G : Type u) [CommRing k] [Monoid G] (X : Type u) : (linearization k G).obj { V := X, ρ := 1 } ≅ trivial k G (X →₀ k)

The linearization of a type X on which G acts trivially is the trivial G-representation on k[X].

Equations

• Rep.linearizationTrivialIso k G X = Action.mkIso (CategoryTheory.Iso.refl ((Rep.linearization k G).obj { V := X, ρ := 1 }).V) ⋯

@[simp]

theorem Rep.linearizationTrivialIso_inv_hom (k G : Type u) [CommRing k] [Monoid G] (X : Type u) : (linearizationTrivialIso k G X).inv.hom = CategoryTheory.CategoryStruct.id ((linearization k G).obj { V := X, ρ := 1 }).V

@[simp]

theorem Rep.linearizationTrivialIso_hom_hom (k G : Type u) [CommRing k] [Monoid G] (X : Type u) : (linearizationTrivialIso k G X).hom.hom = CategoryTheory.CategoryStruct.id ((linearization k G).obj { V := X, ρ := 1 }).V

@[reducible, inline]

noncomputable abbrev Rep.ofMulAction (k G : Type u) [CommRing k] [Monoid G] (H : Type u) [MulAction G H] : Rep k G

Given a G-action on H, this is k[H] bundled with the natural representation G →* End(k[H]) as a term of type Rep k G.

Equations

• Rep.ofMulAction k G H = Rep.of (Representation.ofMulAction k G H)

@[reducible, inline]

noncomputable abbrev Rep.leftRegular (k G : Type u) [CommRing k] [Monoid G] : Rep k G

The k-linear G-representation on k[G], induced by left multiplication.

Equations

• Rep.leftRegular k G = Rep.ofMulAction k G G

@[reducible, inline]

noncomputable abbrev Rep.diagonal (k G : Type u) [CommRing k] [Monoid G] (n : ℕ) : Rep k G

The k-linear G-representation on k[Gⁿ], induced by left multiplication.

Equations

• Rep.diagonal k G n = Rep.ofMulAction k G (Fin n → G)

noncomputable def Rep.diagonalOneIsoLeftRegular (k G : Type u) [CommRing k] [Monoid G] : diagonal k G 1 ≅ leftRegular k G

The natural isomorphism between the representations on k[G¹] and k[G] induced by left multiplication in G.

Equations

• Rep.diagonalOneIsoLeftRegular k G = Action.mkIso (Finsupp.domLCongr (Equiv.funUnique (Fin 1) G)).toModuleIso ⋯

@[simp]

theorem Rep.diagonalOneIsoLeftRegular_inv_hom (k G : Type u) [CommRing k] [Monoid G] : (diagonalOneIsoLeftRegular k G).inv.hom = ModuleCat.ofHom ↑(Finsupp.domLCongr (Equiv.funUnique (Fin 1) G).symm)

@[simp]

theorem Rep.diagonalOneIsoLeftRegular_hom_hom (k G : Type u) [CommRing k] [Monoid G] : (diagonalOneIsoLeftRegular k G).hom.hom = ModuleCat.ofHom ↑(Finsupp.domLCongr (Equiv.funUnique (Fin 1) G))

noncomputable def Rep.ofMulActionSubsingletonIsoTrivial (k G : Type u) [CommRing k] [Monoid G] (H : Type u) [Subsingleton H] [MulOneClass H] [MulAction G H] : ofMulAction k G H ≅ trivial k G k

When H = {1}, the G-representation on k[H] induced by an action of G on H is isomorphic to the trivial representation on k.

Equations

• Rep.ofMulActionSubsingletonIsoTrivial k G H = Action.mkIso (Finsupp.LinearEquiv.finsuppUnique k k H).toModuleIso ⋯

@[simp]

theorem Rep.ofMulActionSubsingletonIsoTrivial_inv_hom (k G : Type u) [CommRing k] [Monoid G] (H : Type u) [Subsingleton H] [MulOneClass H] [MulAction G H] : (ofMulActionSubsingletonIsoTrivial k G H).inv.hom = ModuleCat.ofHom ↑(Finsupp.LinearEquiv.finsuppUnique k k H).symm

@[simp]

theorem Rep.ofMulActionSubsingletonIsoTrivial_hom_hom (k G : Type u) [CommRing k] [Monoid G] (H : Type u) [Subsingleton H] [MulOneClass H] [MulAction G H] : (ofMulActionSubsingletonIsoTrivial k G H).hom.hom = ModuleCat.ofHom ↑(Finsupp.LinearEquiv.finsuppUnique k k H)

noncomputable def Rep.linearizationOfMulActionIso (k G : Type u) [CommRing k] [Monoid G] (H : Type u) [MulAction G H] : (linearization k G).obj (Action.ofMulAction G H) ≅ ofMulAction k G H

The linearization of a type H with a G-action is definitionally isomorphic to the k-linear G-representation on k[H] induced by the G-action on H.

Equations

• Rep.linearizationOfMulActionIso k G H = CategoryTheory.Iso.refl ((Rep.linearization k G).obj (Action.ofMulAction G H))

noncomputable def Rep.ofDistribMulAction (k G A : Type u) [CommRing k] [Monoid G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] : Rep k G

Turns a k-module A with a compatible DistribMulAction of a monoid G into a k-linear G-representation on A.

Equations

• Rep.ofDistribMulAction k G A = Rep.of (Representation.ofDistribMulAction k G A)

@[simp]

theorem Rep.ofDistribMulAction_ρ_apply_apply (k G A : Type u) [CommRing k] [Monoid G] [AddCommGroup A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (g : G) (a : A) : ((ofDistribMulAction k G A).ρ g) a = g • a

noncomputable def Rep.ofAlgebraAut (R S : Type) [CommRing R] [CommRing S] [Algebra R S] : Rep ℤ (S ≃ₐ[R] S)

Given an R-algebra S, the ℤ-linear representation associated to the natural action of S ≃ₐ[R] S on S.

Equations

• Rep.ofAlgebraAut R S = Rep.ofDistribMulAction ℤ (S ≃ₐ[R] S) S

noncomputable def Rep.ofMulDistribMulAction (M G : Type) [Monoid M] [CommGroup G] [MulDistribMulAction M G] : Rep ℤ M

Turns a CommGroup G with a MulDistribMulAction of a monoid M into a ℤ-linear M-representation on Additive G.

Equations

• Rep.ofMulDistribMulAction M G = Rep.of (Representation.ofMulDistribMulAction M G)

@[simp]

theorem Rep.ofMulDistribMulAction_ρ_apply_apply (M G : Type) [Monoid M] [CommGroup G] [MulDistribMulAction M G] (g : M) (a : Additive G) : ((ofMulDistribMulAction M G).ρ g) a = Additive.ofMul (g • Additive.toMul a)

noncomputable def Rep.ofAlgebraAutOnUnits (R S : Type) [CommRing R] [CommRing S] [Algebra R S] : Rep ℤ (S ≃ₐ[R] S)

Given an R-algebra S, the ℤ-linear representation associated to the natural action of S ≃ₐ[R] S on Sˣ.

Equations

• Rep.ofAlgebraAutOnUnits R S = Rep.ofMulDistribMulAction (S ≃ₐ[R] S) Sˣ

noncomputable def Rep.leftRegularHom {k G : Type u} [CommRing k] [Monoid G] (A : Rep k G) (x : ↑A.V) : leftRegular k G ⟶ A

Given an element x : A, there is a natural morphism of representations k[G] ⟶ A sending g ↦ A.ρ(g)(x).

Equations

• A.leftRegularHom x = { hom := ModuleCat.ofHom ((Finsupp.lift (↑A.V) k G) fun (g : G) => (A.ρ g) x), comm := ⋯ }

@[simp]

theorem Rep.leftRegularHom_hom {k G : Type u} [CommRing k] [Monoid G] (A : Rep k G) (x : ↑A.V) : (A.leftRegularHom x).hom = ModuleCat.ofHom ((Finsupp.lift (↑A.V) k G) fun (g : G) => (A.ρ g) x)

theorem Rep.leftRegularHom_hom_single {k G : Type u} [CommRing k] [Monoid G] {A : Rep k G} (g : G) (x : ↑A.V) (r : k) : (CategoryTheory.ConcreteCategory.hom (A.leftRegularHom x).hom) (Finsupp.single g r) = r • (A.ρ g) x

noncomputable def Rep.leftRegularHomEquiv {k G : Type u} [CommRing k] [Monoid G] (A : Rep k G) : (leftRegular k G ⟶ A) ≃ₗ[k] ↑A.V

Given a k-linear G-representation A, there is a k-linear isomorphism between representation morphisms Hom(k[G], A) and A.

Equations

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

@[simp]

theorem Rep.leftRegularHomEquiv_apply {k G : Type u} [CommRing k] [Monoid G] (A : Rep k G) (f : leftRegular k G ⟶ A) : A.leftRegularHomEquiv f = (CategoryTheory.ConcreteCategory.hom f.hom) (Finsupp.single 1 1)

@[simp]

theorem Rep.leftRegularHomEquiv_symm_apply {k G : Type u} [CommRing k] [Monoid G] (A : Rep k G) (x : ↑A.V) : A.leftRegularHomEquiv.symm x = A.leftRegularHom x

theorem Rep.leftRegularHomEquiv_symm_single {k G : Type u} [CommRing k] [Monoid G] {A : Rep k G} (x : ↑A.V) (g : G) : (CategoryTheory.ConcreteCategory.hom (A.leftRegularHomEquiv.symm x).hom) (Finsupp.single g 1) = (A.ρ g) x

@[reducible, inline]

noncomputable abbrev Rep.finsupp {k G : Type u} [CommRing k] [Monoid G] (α : Type u) (A : Rep k G) : Rep k G

The representation on α →₀ A defined pointwise by a representation on A.

Equations

• Rep.finsupp α A = Rep.of (A.ρ.finsupp α)

@[reducible, inline]

noncomputable abbrev Rep.free (k G : Type u) [CommRing k] [Monoid G] (α : Type u) : Rep k G

The representation on α →₀ k[G] defined pointwise by the left regular representation on k[G].

Equations

• Rep.free k G α = Rep.of (Representation.free k G α)

noncomputable def Rep.freeLift {k G : Type u} [CommRing k] [Monoid G] {α : Type u} (A : Rep k G) [DecidableEq α] (f : α → ↑A.V) : free k G α ⟶ A

Given f : α → A, the natural representation morphism (α →₀ k[G]) ⟶ A sending single a (single g r) ↦ r • A.ρ g (f a).

Equations

• A.freeLift f = { hom := ModuleCat.ofHom ((Finsupp.linearCombination k fun (x : α × G) => (A.ρ x.2) (f x.1)) ∘ₗ ↑(Finsupp.finsuppProdLEquiv k).symm), comm := ⋯ }

@[simp]

theorem Rep.freeLift_hom {k G : Type u} [CommRing k] [Monoid G] {α : Type u} (A : Rep k G) [DecidableEq α] (f : α → ↑A.V) : (A.freeLift f).hom = ModuleCat.ofHom ((Finsupp.linearCombination k fun (x : α × G) => (A.ρ x.2) (f x.1)) ∘ₗ ↑(Finsupp.finsuppProdLEquiv k).symm)

theorem Rep.freeLift_hom_single_single {k G : Type u} [CommRing k] [Monoid G] {α : Type u} {A : Rep k G} [DecidableEq α] (f : α → ↑A.V) (i : α) (g : G) (r : k) : (CategoryTheory.ConcreteCategory.hom (A.freeLift f).hom) (Finsupp.single i (Finsupp.single g r)) = r • (A.ρ g) (f i)

noncomputable def Rep.freeLiftLEquiv {k G : Type u} [CommRing k] [Monoid G] (α : Type u) (A : Rep k G) [DecidableEq α] : (free k G α ⟶ A) ≃ₗ[k] α → ↑A.V

The natural linear equivalence between functions α → A and representation morphisms (α →₀ k[G]) ⟶ A.

Equations

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

@[simp]

theorem Rep.freeLiftLEquiv_apply {k G : Type u} [CommRing k] [Monoid G] (α : Type u) (A : Rep k G) [DecidableEq α] (f : free k G α ⟶ A) (i : α) : (freeLiftLEquiv α A) f i = (CategoryTheory.ConcreteCategory.hom f.hom) (Finsupp.single i (Finsupp.single 1 1))

@[simp]

theorem Rep.freeLiftLEquiv_symm_apply {k G : Type u} [CommRing k] [Monoid G] (α : Type u) (A : Rep k G) [DecidableEq α] (f : α → ↑A.V) : (freeLiftLEquiv α A).symm f = A.freeLift f

theorem Rep.free_ext {k G : Type u} [CommRing k] [Monoid G] {α : Type u} {A : Rep k G} [DecidableEq α] (f g : free k G α ⟶ A) (h : ∀ (i : α), (CategoryTheory.ConcreteCategory.hom f.hom) (Finsupp.single i (Finsupp.single 1 1)) = (CategoryTheory.ConcreteCategory.hom g.hom) (Finsupp.single i (Finsupp.single 1 1))) : f = g

theorem Rep.free_ext_iff {k G : Type u} [CommRing k] [Monoid G] {α : Type u} {A : Rep k G} [DecidableEq α] {f g : free k G α ⟶ A} : f = g ↔ ∀ (i : α), (CategoryTheory.ConcreteCategory.hom f.hom) (Finsupp.single i (Finsupp.single 1 1)) = (CategoryTheory.ConcreteCategory.hom g.hom) (Finsupp.single i (Finsupp.single 1 1))

noncomputable def Rep.finsuppTensorLeft {k G : Type u} [CommRing k] [Monoid G] (A B : Rep k G) (α : Type u) [DecidableEq α] : CategoryTheory.MonoidalCategoryStruct.tensorObj (finsupp α A) B ≅ finsupp α (CategoryTheory.MonoidalCategoryStruct.tensorObj A B)

Given representations A, B and a type α, this is the natural representation isomorphism (α →₀ A) ⊗ B ≅ (A ⊗ B) →₀ α sending single x a ⊗ₜ b ↦ single x (a ⊗ₜ b).

Equations

• A.finsuppTensorLeft B α = Action.mkIso (TensorProduct.finsuppLeft k (↑A.V) (↑B.V) α).toModuleIso ⋯

@[simp]

theorem Rep.finsuppTensorLeft_hom_hom {k G : Type u} [CommRing k] [Monoid G] (A B : Rep k G) (α : Type u) [DecidableEq α] : (A.finsuppTensorLeft B α).hom.hom = ModuleCat.ofHom ↑(TensorProduct.finsuppLeft k (↑A.V) (↑B.V) α)

@[simp]

theorem Rep.finsuppTensorLeft_inv_hom {k G : Type u} [CommRing k] [Monoid G] (A B : Rep k G) (α : Type u) [DecidableEq α] : (A.finsuppTensorLeft B α).inv.hom = ModuleCat.ofHom ↑(TensorProduct.finsuppLeft k (↑A.V) (↑B.V) α).symm

noncomputable def Rep.finsuppTensorRight {k G : Type u} [CommRing k] [Monoid G] (A B : Rep k G) (α : Type u) [DecidableEq α] : CategoryTheory.MonoidalCategoryStruct.tensorObj A (finsupp α B) ≅ finsupp α (CategoryTheory.MonoidalCategoryStruct.tensorObj A B)

Given representations A, B and a type α, this is the natural representation isomorphism A ⊗ (α →₀ B) ≅ (A ⊗ B) →₀ α sending a ⊗ₜ single x b ↦ single x (a ⊗ₜ b).

Equations

• A.finsuppTensorRight B α = Action.mkIso (TensorProduct.finsuppRight k (↑A.V) (↑B.V) α).toModuleIso ⋯

@[simp]

theorem Rep.finsuppTensorRight_hom_hom {k G : Type u} [CommRing k] [Monoid G] (A B : Rep k G) (α : Type u) [DecidableEq α] : (A.finsuppTensorRight B α).hom.hom = ModuleCat.ofHom ↑(TensorProduct.finsuppRight k (↑A.V) (↑B.V) α)

@[simp]

theorem Rep.finsuppTensorRight_inv_hom {k G : Type u} [CommRing k] [Monoid G] (A B : Rep k G) (α : Type u) [DecidableEq α] : (A.finsuppTensorRight B α).inv.hom = ModuleCat.ofHom ↑(TensorProduct.finsuppRight k (↑A.V) (↑B.V) α).symm

noncomputable def Rep.leftRegularTensorTrivialIsoFree (k G : Type u) [CommRing k] [Monoid G] (α : Type u) [DecidableEq α] : CategoryTheory.MonoidalCategoryStruct.tensorObj (leftRegular k G) (trivial k G (α →₀ k)) ≅ free k G α

The natural isomorphism sending single g r₁ ⊗ single a r₂ ↦ single a (single g r₁r₂).

Equations

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

theorem Rep.leftRegularTensorTrivialIsoFree_hom_hom (k G : Type u) [CommRing k] [Monoid G] (α : Type u) [DecidableEq α] : (leftRegularTensorTrivialIsoFree k G α).hom.hom = ModuleCat.ofHom ↑(((finsuppTensorFinsupp' k G α).trans (Finsupp.domLCongr (Equiv.prodComm G α))).trans (Finsupp.finsuppProdLEquiv k))

theorem Rep.leftRegularTensorTrivialIsoFree_inv_hom (k G : Type u) [CommRing k] [Monoid G] (α : Type u) [DecidableEq α] : (leftRegularTensorTrivialIsoFree k G α).inv.hom = ModuleCat.ofHom ↑((Finsupp.finsuppProdLEquiv k).symm.trans ((Finsupp.domLCongr (Equiv.prodComm α G)).trans (finsuppTensorFinsupp' k G α).symm))

@[simp]

theorem Rep.leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single {k G : Type u} [CommRing k] [Monoid G] {α : Type u} [DecidableEq α] (i : α) (g : G) (r s : k) : (ModuleCat.Hom.hom (leftRegularTensorTrivialIsoFree k G α).hom.hom) (Finsupp.single g r ⊗ₜ[k] Finsupp.single i s) = Finsupp.single i (Finsupp.single g (r * s))

@[simp]

theorem Rep.leftRegularTensorTrivialIsoFree_inv_hom_single_single {k G : Type u} [CommRing k] [Monoid G] {α : Type u} [DecidableEq α] (i : α) (g : G) (r : k) : (ModuleCat.Hom.hom (leftRegularTensorTrivialIsoFree k G α).inv.hom) (Finsupp.single i (Finsupp.single g r)) = Finsupp.single g r ⊗ₜ[k] Finsupp.single i 1

noncomputable def Rep.diagonalSuccIsoTensorTrivial (k G : Type u) [CommRing k] [Group G] (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.

@[simp]

theorem Rep.diagonalSuccIsoTensorTrivial_hom_hom_single {k G : Type u} [CommRing k] [Group G] {n : ℕ} (f : Fin (n + 1) → G) (a : k) : (ModuleCat.Hom.hom (diagonalSuccIsoTensorTrivial k G n).hom.hom) (Finsupp.single f a) = Finsupp.single (f 0) 1 ⊗ₜ[k] Finsupp.single (fun (i : Fin n) => (f i.castSucc)⁻¹ * f i.succ) a

theorem Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_single {k G : Type u} [CommRing k] [Group G] {n : ℕ} (g : G) (f : Fin n → G) (a b : k) : (CategoryTheory.ConcreteCategory.hom (diagonalSuccIsoTensorTrivial k G n).inv.hom) (Finsupp.single g a ⊗ₜ[k] Finsupp.single f b) = Finsupp.single (g • Fin.partialProd f) (a * b)

theorem Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left {k G : Type u} [CommRing k] [Group G] {n : ℕ} (g : G) (f : (Fin n → G) →₀ k) (r : k) : (CategoryTheory.ConcreteCategory.hom (diagonalSuccIsoTensorTrivial k G n).inv.hom) (Finsupp.single g r ⊗ₜ[k] f) = ((Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G)) fun (f : Fin n → G) => Finsupp.single (g • Fin.partialProd f) r) f

theorem Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right {k G : Type u} [CommRing k] [Group G] {n : ℕ} (g : G →₀ k) (f : Fin n → G) (r : k) : (CategoryTheory.ConcreteCategory.hom (diagonalSuccIsoTensorTrivial k G n).inv.hom) (g ⊗ₜ[k] Finsupp.single f r) = ((Finsupp.lift ((Fin (n + 1) → G) →₀ k) k G) fun (a : G) => Finsupp.single (a • Fin.partialProd f) r) g

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

Representation isomorphism k[Gⁿ⁺¹] ≅ (Gⁿ →₀ k[G]), where the righthand 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)

@[simp]

theorem Rep.diagonalSuccIsoFree_hom_hom_single {k G : Type u} [CommRing k] [Group G] {n : ℕ} [DecidableEq (Fin n → G)] (f : Fin (n + 1) → G) (a : k) : (CategoryTheory.ConcreteCategory.hom (diagonalSuccIsoFree k G n).hom.hom) (Finsupp.single f a) = Finsupp.single (fun (i : Fin n) => (f i.castSucc)⁻¹ * f i.succ) (Finsupp.single (f 0) a)

@[simp]

theorem Rep.diagonalSuccIsoFree_inv_hom_single_single {k G : Type u} [CommRing k] [Group G] {n : ℕ} [DecidableEq (Fin n → G)] (g : G) (f : Fin n → G) (a : k) : (CategoryTheory.ConcreteCategory.hom (diagonalSuccIsoFree k G n).inv.hom) (Finsupp.single f (Finsupp.single g a)) = Finsupp.single (g • Fin.partialProd f) a

theorem Rep.diagonalSuccIsoFree_inv_hom_single {k G : Type u} [CommRing k] [Group G] {n : ℕ} [DecidableEq (Fin n → G)] (g : G →₀ k) (f : Fin n → G) : (CategoryTheory.ConcreteCategory.hom (diagonalSuccIsoFree k G n).inv.hom) (Finsupp.single f g) = ((Finsupp.lift ((Fin (n + 1) → G) →₀ k) k G) fun (a : G) => Finsupp.single (a • Fin.partialProd f) 1) g

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

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 n A = (CategoryTheory.Linear.homCongr k (Rep.diagonalSuccIsoFree k G n) (CategoryTheory.Iso.refl A)).trans (Rep.freeLiftLEquiv (Fin n → G) A)

theorem Rep.diagonalHomEquiv_apply {k G : Type u} [CommRing k] [Group G] {n : ℕ} [DecidableEq (Fin n → G)] {A : Rep k G} (f : diagonal k G (n + 1) ⟶ A) (x : Fin n → G) : (diagonalHomEquiv n A) f x = (CategoryTheory.ConcreteCategory.hom f.hom) (Finsupp.single (Fin.partialProd x) 1)

Given a k-linear G-representation A, diagonalHomEquiv is a k-linear isomorphism of the set of representation morphisms Hom(k[Gⁿ⁺¹], A) with Fun(Gⁿ, A). This lemma says that this sends a morphism of representations f : k[Gⁿ⁺¹] ⟶ A to the function (g₁, ..., gₙ) ↦ f(1, g₁, g₁g₂, ..., g₁g₂...gₙ).

theorem Rep.diagonalHomEquiv_symm_apply {k G : Type u} [CommRing k] [Group G] {n : ℕ} [DecidableEq (Fin n → G)] {A : Rep k G} (f : (Fin n → G) → ↑A.V) (x : Fin (n + 1) → G) : (CategoryTheory.ConcreteCategory.hom ((diagonalHomEquiv n A).symm f).hom) (Finsupp.single x 1) = (A.ρ (x 0)) (f fun (i : Fin n) => (x i.castSucc)⁻¹ * x i.succ)

Given a k-linear G-representation A, diagonalHomEquiv is a k-linear isomorphism of the set of representation morphisms Hom(k[Gⁿ⁺¹], A) with Fun(Gⁿ, A). This lemma says that the inverse map sends a function f : Gⁿ → A to the representation morphism sending (g₀, ... gₙ) ↦ ρ(g₀)(f(g₀⁻¹g₁, g₁⁻¹g₂, ..., gₙ₋₁⁻¹gₙ)), where ρ is the representation attached to A.

@[deprecated "We no longer use `diagonalHomEquiv` to define group cohomology" (since := "2025-06-08")]

theorem Rep.diagonalHomEquiv_symm_partialProd_succ {k G : Type u} [CommRing k] [Group G] {n : ℕ} [DecidableEq (Fin n → G)] {A : Rep k G} (f : (Fin n → G) → ↑A.V) (g : Fin (n + 1) → G) (a : Fin (n + 1)) : (CategoryTheory.ConcreteCategory.hom ((diagonalHomEquiv n A).symm f).hom) (Finsupp.single (Fin.partialProd g ∘ a.succ.succAbove) 1) = f (a.contractNth (fun (x1 x2 : G) => x1 * x2) g)

Auxiliary lemma for defining group cohomology, used to show that the isomorphism diagonalHomEquiv commutes with the differentials in two complexes which compute group cohomology.

noncomputable def Rep.ihom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) : CategoryTheory.Functor (Rep k G) (Rep k G)

Given a k-linear G-representation (A, ρ₁), this is the 'internal Hom' functor sending (B, ρ₂) to the representation Homₖ(A, B) that maps g : G and f : A →ₗ[k] B to (ρ₂ g) ∘ₗ f ∘ₗ (ρ₁ g⁻¹).

Equations

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

@[simp]

theorem Rep.ihom_map_hom {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {X Y : Rep k G} (f : X ⟶ Y) : (A.ihom.map f).hom = ModuleCat.ofHom ((LinearMap.llcomp k ↑A.V ↑X.V ↑Y.V) (ModuleCat.Hom.hom f.hom))

@[simp]

theorem Rep.ihom_obj_ρ {k G : Type u} [CommRing k] [Group G] (A B : Rep k G) : (A.ihom.obj B).ρ = (ModuleCat.of k (↑A.V →ₗ[k] ↑B.V)).endRingEquiv.symm.toMonoidHom.comp (A.ρ.linHom B.ρ)

@[simp]

theorem Rep.ihom_obj_V_carrier {k G : Type u} [CommRing k] [Group G] (A B : Rep k G) : ↑(A.ihom.obj B).V = (↑A.V →ₗ[k] ↑B.V)

@[simp]

theorem Rep.ihom_obj_V_isAddCommGroup {k G : Type u} [CommRing k] [Group G] (A B : Rep k G) : (A.ihom.obj B).V.isAddCommGroup = LinearMap.addCommGroup

@[simp]

theorem Rep.ihom_obj_V_isModule {k G : Type u} [CommRing k] [Group G] (A B : Rep k G) : (A.ihom.obj B).V.isModule = LinearMap.module

@[simp]

theorem Rep.ihom_obj_ρ_apply {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} (g : G) (x : ↑A.V →ₗ[k] ↑B.V) : ((A.ihom.obj B).ρ g) x = B.ρ g ∘ₗ x ∘ₗ A.ρ g⁻¹

noncomputable def Rep.homEquiv {k G : Type u} [CommRing k] [Group G] (A B C : Rep k G) : (CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C) ≃ (B ⟶ A.ihom.obj C)

Given a k-linear G-representation A, this is the Hom-set bijection in the adjunction A ⊗ - ⊣ ihom(A, -). It sends f : A ⊗ B ⟶ C to a Rep k G morphism defined by currying the k-linear map underlying f, giving a map A →ₗ[k] B →ₗ[k] C, then flipping the arguments.

Equations

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

theorem Rep.homEquiv_apply_hom {k G : Type u} [CommRing k] [Group G] {A B C : Rep k G} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C) : ((A.homEquiv B C) f).hom = ModuleCat.ofHom (TensorProduct.curry (ModuleCat.Hom.hom f.hom)).flip

Porting note: if we generate this with @[simps] the linter complains some types in the LHS simplify.

theorem Rep.homEquiv_symm_apply_hom {k G : Type u} [CommRing k] [Group G] {A B C : Rep k G} (f : B ⟶ A.ihom.obj C) : ((A.homEquiv B C).symm f).hom = ModuleCat.ofHom ((TensorProduct.uncurry k ↑A.V ↑B.V ↑C.V) (ModuleCat.Hom.hom f.hom).flip)

Porting note: if we generate this with @[simps] the linter complains some types in the LHS simplify.

noncomputable instance Rep.instMonoidalClosed {k G : Type u} [CommRing k] [Group G] : CategoryTheory.MonoidalClosed (Rep k G)

Equations

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

@[simp]

theorem Rep.ihom_obj_ρ_def {k G : Type u} [CommRing k] [Group G] (A B : Rep k G) : ((CategoryTheory.ihom A).obj B).ρ = (A.ihom.obj B).ρ

@[simp]

theorem Rep.homEquiv_def {k G : Type u} [CommRing k] [Group G] (A B C : Rep k G) : (CategoryTheory.ihom.adjunction A).homEquiv B C = A.homEquiv B C

@[simp]

theorem Rep.ihom_ev_app_hom {k G : Type u} [CommRing k] [Group G] (A B : Rep k G) : ((CategoryTheory.ihom.ev A).app B).hom = ModuleCat.ofHom ((TensorProduct.uncurry k (↑A.V) (↑A.V →ₗ[k] ↑B.V) ↑B.V) LinearMap.id.flip)

@[simp]

theorem Rep.ihom_coev_app_hom {k G : Type u} [CommRing k] [Group G] (A B : Rep k G) : ((CategoryTheory.ihom.coev A).app B).hom = ModuleCat.ofHom (TensorProduct.mk k ↑A.V ↑((CategoryTheory.Functor.id (Rep k G)).obj B).1).flip

noncomputable def Rep.MonoidalClosed.linearHomEquiv {k G : Type u} [CommRing k] [Group G] (A B C : Rep k G) : (CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C) ≃ₗ[k] B ⟶ (CategoryTheory.ihom A).obj C

There is a k-linear isomorphism between the sets of representation morphismsHom(A ⊗ B, C) and Hom(B, Homₖ(A, C)).

Equations

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

noncomputable def Rep.MonoidalClosed.linearHomEquivComm {k G : Type u} [CommRing k] [Group G] (A B C : Rep k G) : (CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C) ≃ₗ[k] A ⟶ (CategoryTheory.ihom B).obj C

There is a k-linear isomorphism between the sets of representation morphismsHom(A ⊗ B, C) and Hom(A, Homₖ(B, C)).

Equations

• Rep.MonoidalClosed.linearHomEquivComm A B C = (CategoryTheory.Linear.homCongr k (β_ A B) (CategoryTheory.Iso.refl C)).trans (Rep.MonoidalClosed.linearHomEquiv B A C)

@[simp]

theorem Rep.MonoidalClosed.linearHomEquiv_hom {k G : Type u} [CommRing k] [Group G] {A B C : Rep k G} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C) : ((linearHomEquiv A B C) f).hom = ModuleCat.ofHom (TensorProduct.curry (ModuleCat.Hom.hom f.hom)).flip

@[simp]

theorem Rep.MonoidalClosed.linearHomEquivComm_hom {k G : Type u} [CommRing k] [Group G] {A B C : Rep k G} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C) : ((linearHomEquivComm A B C) f).hom = ModuleCat.ofHom (TensorProduct.curry (ModuleCat.Hom.hom f.hom))

theorem Rep.MonoidalClosed.linearHomEquiv_symm_hom {k G : Type u} [CommRing k] [Group G] {A B C : Rep k G} (f : B ⟶ (CategoryTheory.ihom A).obj C) : ((linearHomEquiv A B C).symm f).hom = ModuleCat.ofHom ((TensorProduct.uncurry k ↑A.V ↑B.V ↑C.V) (ModuleCat.Hom.hom f.hom).flip)

theorem Rep.MonoidalClosed.linearHomEquivComm_symm_hom {k G : Type u} [CommRing k] [Group G] {A B C : Rep k G} (f : A ⟶ (CategoryTheory.ihom B).obj C) : ((linearHomEquivComm A B C).symm f).hom = ModuleCat.ofHom ((TensorProduct.uncurry k ↑A.V ↑B.V ↑C.V) (ModuleCat.Hom.hom f.hom))

noncomputable def Representation.repOfTprodIso {k G : Type u} [CommRing k] [Monoid G] {V W : Type u} [AddCommGroup V] [AddCommGroup W] [Module k V] [Module k W] (ρ : Representation k G V) (τ : Representation k G W) : Rep.of (ρ.tprod τ) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (Rep.of ρ) (Rep.of τ)

Tautological isomorphism to help Lean in typechecking.

Equations

• ρ.repOfTprodIso τ = CategoryTheory.Iso.refl (Rep.of (ρ.tprod τ))

theorem Representation.repOfTprodIso_apply {k G : Type u} [CommRing k] [Monoid G] {V W : Type u} [AddCommGroup V] [AddCommGroup W] [Module k V] [Module k W] (ρ : Representation k G V) (τ : Representation k G W) (x : TensorProduct k V W) : (CategoryTheory.ConcreteCategory.hom (ρ.repOfTprodIso τ).hom.hom) x = x

theorem Representation.repOfTprodIso_inv_apply {k G : Type u} [CommRing k] [Monoid G] {V W : Type u} [AddCommGroup V] [AddCommGroup W] [Module k V] [Module k W] (ρ : Representation k G V) (τ : Representation k G W) (x : TensorProduct k V W) : (CategoryTheory.ConcreteCategory.hom (ρ.repOfTprodIso τ).inv.hom) x = x

The categorical equivalence Rep k G ≌ Module.{u} (MonoidAlgebra 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 G (V →ₗ[k] V)) ρ) r) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) r) (f x)

Auxiliary lemma for toModuleMonoidAlgebra.

noncomputable def Rep.toModuleMonoidAlgebraMap {k G : Type u} [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 := ModuleCat.Hom.hom f.hom; { toAddHom := __src.toAddHom, map_smul' := ⋯ })

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

Functorially convert a representation of G into a module over MonoidAlgebra k G.

Equations

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

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

Functorially convert a module over MonoidAlgebra 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 G : Type u} [CommRing k] [Monoid G] (M : ModuleCat (MonoidAlgebra k G)) : ↑(ofModuleMonoidAlgebra.obj M).V = RestrictScalars k (MonoidAlgebra k G) ↑M

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

noncomputable def Rep.counitIsoAddEquiv {k G : Type u} [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 G : Type u} [CommRing k] [Monoid G] {V : Rep k G} : ↑V.V ≃+ ↑((toModuleMonoidAlgebra.comp ofModuleMonoidAlgebra).obj V).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 G : Type u} [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 G : Type u} [CommRing k] [Monoid G] (V : Rep k G) (g : G) (x : ↑V.V) : unitIsoAddEquiv ((V.ρ g).toFun x) = ((ofModuleMonoidAlgebra.obj (toModuleMonoidAlgebra.obj V)).ρ g).toFun (unitIsoAddEquiv x)

noncomputable def Rep.unitIso {k G : Type u} [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 G : Type u} [CommRing k] [Monoid G] : Rep k G ≌ ModuleCat (MonoidAlgebra k G)

The categorical equivalence Rep k G ≌ ModuleCat (MonoidAlgebra k G).

Equations

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

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

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

instance Rep.diagonal_succ_projective {k : Type u} [CommRing k] {G : Type u} [Group G] {n : ℕ} [DecidableEq (Fin n → G)] : 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)