Induction and coinduction from the trivial subgroup

For a group G and a k-module X, the representation coinduced from the trivial subgroup, coindBot k G X = Coind_⊥^G X, is the module of functions G → X with G acting by right translation, (g • f) h = f (h * g), and the representation induced from the trivial subgroup, indBot k G X = Ind_⊥^G X, is k[G] ⊗ X, which is the module of finitely supported functions G →₀ X with the same right-translation action (Rep.indBotEquivFinsupp). Every representation A embeds into coindBot k G A.V (by a ↦ (g ↦ g • a)) and is a quotient of indBot k G A.V; these are the two maps used for dimension shifting. For a finite group the two constructions agree (Rep.indBotIsoCoindBot), and for any group k[G] is induced from the trivial subgroup (Rep.indBotIsoLeftRegular).

Both constructions are stable under restriction to a subgroup S: writing G as S × G ⧸ S through (s, y) ↦ y.out * s (Mathlib's Subgroup.groupEquivQuotientProdSubgroup), the restriction of Coind_⊥^G X to S is Coind_⊥^S (G ⧸ S → X) (Rep.resCoindBotIso), and the restriction of Ind_⊥^G X to S is Ind_⊥^S (G ⧸ S →₀ X) (Rep.resIndBotIso).

The constructions follow ClassFieldTheory/Cohomology/IndCoind/Finite.lean and IndCoind/TrivialCohomology.lean in kbuzzard/ClassFieldTheory, commit ccc3323c6750abca25b49b35106f54eb3a398509, adapted to Mathlib's Rep.coind and Rep.ind.

Main definitions

• Rep.resBotIsoTrivial: the restriction of a representation to the trivial subgroup is the trivial representation on its underlying module.
• Rep.coindBot, Rep.coindBotFunctor: coinduction from the trivial subgroup.
• Rep.coindBotRepFunctor, Rep.indBotRepFunctor: coinduction and induction on the underlying module, as endofunctors of representations.
• Rep.coindBotUnitNatTrans, Rep.indBotCounitNatTrans: the canonical embedding into coinduction and projection from induction, as natural transformations.
• Rep.coindBotMap, Rep.indBotMap: maps induced by morphisms of representations.
• Rep.coindBotUnit: the monomorphism A ⟶ coindBot k G A.V.
• Rep.toCoindBot: the morphism B ⟶ coindBot k G X, b ↦ (g ↦ r (g • b)), attached to a k-linear map r : B → X.
• Rep.indBot, Rep.indBotFunctor: induction from the trivial subgroup.
• Rep.indBotCounit: the epimorphism indBot k G A.V ⟶ A.
• Rep.fromIndBot: the morphism indBot k G X ⟶ B, ⟦g ⊗ₜ x⟧ ↦ g⁻¹ • s x, attached to a k-linear map s : X → B.
• Rep.coindBotEquivPi, Rep.indBotEquivFinsupp: the underlying modules as functions G → X and finitely supported functions G →₀ X.
• Rep.indBotIsoCoindBot: for a finite group, indBot k G X ≅ coindBot k G X.
• Rep.indBotIsoLeftRegular: indBot k G k ≅ k[G].
• Rep.leftRegularIsoCoindBot: for a finite group, k[G] ≅ coindBot k G k.
• Rep.resCoindBotIso, Rep.resIndBotIso: restrictions to a subgroup, again coinduced, respectively induced, from the trivial subgroup.
• Rep.quotientToInvariantsCoindBotIso: the invariants under a normal subgroup S of a representation coinduced from the trivial subgroup, coinduced from the trivial subgroup of G ⧸ S.

References

• J. S. Milne, Class Field Theory, Chapter II, §1.
• K. S. Brown, Cohomology of Groups, Chapter III, §5.

def Rep.resBotIsoTrivial {k G : Type u} [Group G] [Semiring k] (A : Rep.{u_1, u, u} k G) : res ⊥.subtype A ≅ trivial k ↥⊥ ↑A

The restriction of a representation to the trivial subgroup is the trivial representation on its underlying module.

Equations

• A.resBotIsoTrivial = Rep.mkIso (Representation.Equiv.mk (LinearEquiv.refl k ↑A) ⋯)

@[simp]

theorem Rep.resBotIsoTrivial_hom_hom_apply {k G : Type u} [Group G] [Semiring k] (A : Rep.{u_1, u, u} k G) (x : ↑A) : (Hom.hom A.resBotIsoTrivial.hom) x = x

The identification of the restriction to the trivial subgroup with the trivial representation does not move elements.

@[simp]

theorem Rep.resBotIsoTrivial_inv_hom_apply {k G : Type u} [Group G] [Semiring k] (A : Rep.{u_1, u, u} k G) (x : ↑A) : (Hom.hom A.resBotIsoTrivial.inv) x = x

The inverse identification of the trivial representation with the restriction to the trivial subgroup does not move elements.

@[reducible, inline]

noncomputable abbrev Rep.coindBot (k G : Type u) [Group G] [CommRing k] (X : Type u) [AddCommGroup X] [Module k X] : Rep.{u, u, u} k G

The representation of G coinduced from the trivial subgroup on a k-module X: the functions G → X, with G acting by right translation, (g • f) h = f (h * g).

Equations

• Rep.coindBot k G X = Rep.coind.{?u.1, ?u.1, ?u.1, ?u.1} ⊥.subtype (Rep.trivial k (↥⊥) X)

noncomputable def Rep.coindBotFunctor (k G : Type u) [Group G] [CommRing k] : CategoryTheory.Functor (ModuleCat k) (Rep.{u, u, u} k G)

Coinduction from the trivial subgroup, as a functor ModuleCat k ⥤ Rep k G.

Equations

• Rep.coindBotFunctor k G = (Rep.trivialFunctor k ↥⊥).comp (Rep.coindFunctor k ⊥.subtype)

@[simp]

theorem Rep.coindBotFunctor_obj {k G : Type u} [Group G] [CommRing k] (X : ModuleCat k) : (coindBotFunctor k G).obj X = coindBot k G ↑X

Evaluating the coinduction functor from the trivial subgroup gives coindBot.

@[simp]

theorem Rep.coindBotFunctor_map_hom_apply_coe {k G : Type u} [Group G] [CommRing k] {X Y : ModuleCat k} (f : X ⟶ Y) (x : ↑(coindBot k G ↑X)) (g : G) : ↑((Hom.hom ((coindBotFunctor k G).map f)) x) g = (ModuleCat.Hom.hom f) (↑x g)

The coinduction functor from the trivial subgroup acts on a morphism by postcomposition.

def Rep.coindBotUnit {k G : Type u} [Group G] [CommRing k] (A : Rep.{u, u, u} k G) : A ⟶ coindBot k G ↑A

The canonical embedding of a representation A into the representation coinduced from the trivial subgroup on its underlying module, a ↦ (g ↦ A.ρ g a).

Equations

• A.coindBotUnit = Rep.resCoindToHom ⊥.subtype A (Rep.trivial k ↥⊥ ↑A) A.resBotIsoTrivial.hom

@[simp]

theorem Rep.coindBotUnit_hom_apply_coe {k G : Type u} [Group G] [CommRing k] (A : Rep.{u, u, u} k G) (a : ↑A) (g : G) : ↑((Hom.hom A.coindBotUnit) a) g = (A.ρ g) a

The embedding into the coinduced representation sends a to the function g ↦ A.ρ g a.

instance Rep.coindBotUnit_mono {k G : Type u} [Group G] [CommRing k] (A : Rep.{u, u, u} k G) : CategoryTheory.Mono A.coindBotUnit

The embedding into the coinduced representation is a monomorphism.

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

Coinduction on the underlying module, viewed as an endofunctor of representations.

Equations

• Rep.coindBotRepFunctor = (CategoryTheory.forget₂ (Rep.{?u.1, ?u.1, ?u.1} k G) (ModuleCat k)).comp (Rep.coindBotFunctor k G)

noncomputable def Rep.coindBotMap {k G : Type u} [Group G] [CommRing k] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : coindBot k G ↑A ⟶ coindBot k G ↑B

The map of coinduced representations associated to a morphism of representations.

Equations

• Rep.coindBotMap f = (Rep.coindBotFunctor k G).map ((CategoryTheory.forget₂ (Rep.{?u.1, ?u.1, ?u.1} k G) (ModuleCat k)).map f)

@[simp]

theorem Rep.coindBotRepFunctor_obj {k G : Type u} [Group G] [CommRing k] (A : Rep.{u, u, u} k G) : coindBotRepFunctor.obj A = coindBot k G ↑A

The coinduction endofunctor acts on objects by coinduction of underlying modules.

@[simp]

theorem Rep.coindBotRepFunctor_map {k G : Type u} [Group G] [CommRing k] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : coindBotRepFunctor.map f = coindBotMap f

The coinduction endofunctor acts on morphisms by coindBotMap.

@[simp]

theorem Rep.coindBotMap_id {k G : Type u} [Group G] [CommRing k] (A : Rep.{u, u, u} k G) : coindBotMap (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id (coindBot k G ↑A)

The map induced by an identity morphism is the identity.

@[simp]

theorem Rep.coindBotMap_comp {k G : Type u} [Group G] [CommRing k] {A B C : Rep.{u, u, u} k G} (f : A ⟶ B) (g : B ⟶ C) : coindBotMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (coindBotMap f) (coindBotMap g)

The map induced by a composite is the composite of the induced maps.

@[simp]

theorem Rep.coindBotMap_hom_apply_coe {k G : Type u} [Group G] [CommRing k] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) (x : ↑(coindBot k G ↑A)) (g : G) : ↑((Hom.hom (coindBotMap f)) x) g = (Hom.hom f) (↑x g)

The coinduced map acts pointwise by the underlying map.

theorem Rep.coindBotUnit_naturality {k G : Type u} [Group G] [CommRing k] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp f B.coindBotUnit = CategoryTheory.CategoryStruct.comp A.coindBotUnit (coindBotMap f)

The embedding into a coinduced representation is natural in the representation.

theorem Rep.coindBotUnit_naturality_assoc {k G : Type u} [Group G] [CommRing k] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) {Z : Rep.{u, u, u} k G} (h : coindBot k G ↑B ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp B.coindBotUnit h) = CategoryTheory.CategoryStruct.comp A.coindBotUnit (CategoryTheory.CategoryStruct.comp (coindBotMap f) h)

The embedding into a coinduced representation is natural in the representation.

def Rep.coindBotUnitNatTrans {k G : Type u} [Group G] [CommRing k] : CategoryTheory.Functor.id (Rep.{u, u, u} k G) ⟶ coindBotRepFunctor

The canonical embedding into coinduction, as a natural transformation.

Equations

• Rep.coindBotUnitNatTrans = { app := fun (A : Rep.{?u.1, ?u.1, ?u.1} k G) => A.coindBotUnit, naturality := ⋯ }

@[simp]

theorem Rep.coindBotUnitNatTrans_app {k G : Type u} [Group G] [CommRing k] (A : Rep.{u, u, u} k G) : coindBotUnitNatTrans.app A = A.coindBotUnit

The component of the coinduction unit at A is its canonical embedding.

def Rep.coindBotEquivPi (k G : Type u) [Group G] [CommRing k] (X : Type u) [AddCommGroup X] [Module k X] : ↑(coindBot k G X) ≃ₗ[k] G → X

The underlying module of the representation coinduced from the trivial subgroup is the module of all functions G → X.

Equations

• Rep.coindBotEquivPi k G X = LinearEquiv.ofTop (Representation.coindV ⊥.subtype (Rep.trivial k (↥⊥) X).ρ) ⋯

@[simp]

theorem Rep.coindBotEquivPi_apply {k G : Type u} [Group G] [CommRing k] (X : Type u) [AddCommGroup X] [Module k X] (f : ↑(coindBot k G X)) : (coindBotEquivPi k G X) f = ↑f

The identification of the coinduced module with functions is the underlying function.

@[simp]

theorem Rep.coindBotEquivPi_symm_apply_coe {k G : Type u} [Group G] [CommRing k] (X : Type u) [AddCommGroup X] [Module k X] (f : G → X) : ↑((coindBotEquivPi k G X).symm f) = f

The inverse identification of functions with the coinduced module is the underlying function.

theorem Rep.leftInverse_coindBotUnit {k G : Type u} [Group G] [CommRing k] (A : Rep.{u, u, u} k G) : Function.LeftInverse ⇑(LinearMap.proj 1 ∘ₗ ↑(coindBotEquivPi k G ↑A)) ⇑(Hom.hom A.coindBotUnit)

Evaluation at 1 is a k-linear retraction of the embedding of a representation into the representation coinduced from the trivial subgroup.

noncomputable def Rep.toCoindBot {k G : Type u} [Group G] [CommRing k] (A : Rep.{u, u, u} k G) {X : Type u} [AddCommGroup X] [Module k X] (r : ↑A →ₗ[k] X) : A ⟶ coindBot k G X

The morphism n ↦ (g ↦ r (g • n)) from a representation to the representation coinduced from the trivial subgroup, attached to a k-linear map r.

Equations

• A.toCoindBot r = CategoryTheory.CategoryStruct.comp A.coindBotUnit ((Rep.coindBotFunctor k G).map (ModuleCat.ofHom r))

@[simp]

theorem Rep.toCoindBot_hom_apply_coe {k G : Type u} [Group G] [CommRing k] (A : Rep.{u, u, u} k G) {X : Type u} [AddCommGroup X] [Module k X] (r : ↑A →ₗ[k] X) (a : ↑A) (g : G) : ↑((Hom.hom (A.toCoindBot r)) a) g = r ((A.ρ g) a)

The morphism attached to r sends a to the function g ↦ r (g • a).

theorem Rep.comp_toCoindBot_of_leftInverse {k G : Type u} [Group G] [CommRing k] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) {r : ↑B →ₗ[k] ↑A} (hr : Function.LeftInverse ⇑r ⇑(Hom.hom f)) : CategoryTheory.CategoryStruct.comp f (B.toCoindBot r) = A.coindBotUnit

If r is a retraction of f : A ⟶ B, then f followed by n ↦ (g ↦ r (g • n)) is the embedding of A into its coinduced representation.

theorem Rep.comp_toCoindBot_of_leftInverse_assoc {k G : Type u} [Group G] [CommRing k] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) {r : ↑B →ₗ[k] ↑A} (hr : Function.LeftInverse ⇑r ⇑(Hom.hom f)) {Z : Rep.{u, u, u} k G} (h : coindBot k G ↑A ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (B.toCoindBot r) h) = CategoryTheory.CategoryStruct.comp A.coindBotUnit h

If r is a retraction of f : A ⟶ B, then f followed by n ↦ (g ↦ r (g • n)) is the embedding of A into its coinduced representation.

@[reducible, inline]

noncomputable abbrev Rep.indBot (k G : Type u) [Group G] [CommRing k] (X : Type u) [AddCommGroup X] [Module k X] : Rep.{u, u, u} k G

The representation of G induced from the trivial subgroup on a k-module X, namely k[G] ⊗[k] X; Rep.indBotEquivFinsupp identifies it with the finitely supported functions G →₀ X with G acting by right translation, (g • f) h = f (h * g).

Equations

• Rep.indBot k G X = Rep.ind ⊥.subtype (Rep.trivial k (↥⊥) X)

noncomputable def Rep.indBotFunctor (k G : Type u) [Group G] [CommRing k] : CategoryTheory.Functor (ModuleCat k) (Rep.{u, u, u} k G)

Induction from the trivial subgroup, as a functor ModuleCat k ⥤ Rep k G.

Equations

• Rep.indBotFunctor k G = (Rep.trivialFunctor k ↥⊥).comp (Rep.indFunctor k ⊥.subtype)

@[simp]

theorem Rep.indBotFunctor_obj {k G : Type u} [Group G] [CommRing k] (X : ModuleCat k) : (indBotFunctor k G).obj X = indBot k G ↑X

Evaluating the induction functor from the trivial subgroup gives indBot.

theorem Rep.indBotFunctor_map_hom_mk {k G : Type u} [Group G] [CommRing k] {X Y : ModuleCat k} (f : X ⟶ Y) (g : G) (x : ↑X) : (Hom.hom ((indBotFunctor k G).map f)) ((Representation.IndV.mk ⊥.subtype (Representation.trivial k ↥⊥ ↑X) g) x) = (Representation.IndV.mk ⊥.subtype (Representation.trivial k ↥⊥ ↑Y) g) ((ModuleCat.Hom.hom f) x)

The induction functor from the trivial subgroup acts on generators through the morphism: ⟦g ⊗ₜ x⟧ ↦ ⟦g ⊗ₜ f x⟧.

theorem Rep.indBot_hom_ext {k G : Type u} [Group G] [CommRing k] {X : Type u} [AddCommGroup X] [Module k X] {B : Rep.{u, u, u} k G} {f f' : indBot k G X ⟶ B} (h : ∀ (x : X), (Hom.hom f) ((Representation.IndV.mk ⊥.subtype (Representation.trivial k (↥⊥) X) 1) x) = (Hom.hom f') ((Representation.IndV.mk ⊥.subtype (Representation.trivial k (↥⊥) X) 1) x)) : f = f'

Two morphisms out of the representation induced from the trivial subgroup agree once they agree on the generators ⟦1 ⊗ₜ x⟧: by equivariance, these determine the values on every ⟦g ⊗ₜ x⟧.

noncomputable def Rep.indBotCounit {k G : Type u} [Group G] [CommRing k] (A : Rep.{u, u, u} k G) : indBot k G ↑A ⟶ A

The canonical projection from the representation induced from the trivial subgroup on the underlying module of A onto A, ⟦g ⊗ₜ a⟧ ↦ A.ρ g⁻¹ a.

Equations

• A.indBotCounit = (Rep.indResHomEquiv ⊥.subtype (Rep.trivial k ↥⊥ ↑A) A).symm A.resBotIsoTrivial.inv

@[simp]

theorem Rep.indBotCounit_hom_mk {k G : Type u} [Group G] [CommRing k] (A : Rep.{u, u, u} k G) (g : G) (a : ↑A) : (Hom.hom A.indBotCounit) ((Representation.IndV.mk ⊥.subtype (Representation.trivial k ↥⊥ ↑A) g) a) = (A.ρ g⁻¹) a

The projection from the induced representation on generators: ⟦g ⊗ₜ a⟧ ↦ A.ρ g⁻¹ a.

theorem Rep.rightInverse_indBotCounit {k G : Type u} [Group G] [CommRing k] (A : Rep.{u, u, u} k G) : Function.RightInverse ⇑(Representation.IndV.mk ⊥.subtype (Representation.trivial k ↥⊥ ↑A) 1) ⇑(Hom.hom A.indBotCounit)

The generator map a ↦ ⟦1 ⊗ₜ a⟧ is a k-linear section of the projection from the representation induced from the trivial subgroup onto a representation.

instance Rep.indBotCounit_epi {k G : Type u} [Group G] [CommRing k] (A : Rep.{u, u, u} k G) : CategoryTheory.Epi A.indBotCounit

The projection from the induced representation is an epimorphism.

noncomputable def Rep.indBotMap {k G : Type u} [Group G] [CommRing k] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : indBot k G ↑A ⟶ indBot k G ↑B

The map of induced representations associated to a morphism of representations.

Equations

• Rep.indBotMap f = Rep.indMap ⊥.subtype ((Rep.trivialFunctor k ↥⊥).map (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap))

@[simp]

theorem Rep.indBotMap_id {k G : Type u} [Group G] [CommRing k] (A : Rep.{u, u, u} k G) : indBotMap (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id (indBot k G ↑A)

The map induced by an identity morphism is the identity.

@[simp]

theorem Rep.indBotMap_comp {k G : Type u} [Group G] [CommRing k] {A B C : Rep.{u, u, u} k G} (f : A ⟶ B) (g : B ⟶ C) : indBotMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (indBotMap f) (indBotMap g)

The map induced by a composite is the composite of the induced maps.

theorem Rep.indBotMap_hom_mk {k G : Type u} [Group G] [CommRing k] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) (g : G) (a : ↑A) : (Hom.hom (indBotMap f)) ((Representation.IndV.mk ⊥.subtype (Representation.trivial k ↥⊥ ↑A) g) a) = (Representation.IndV.mk ⊥.subtype (Representation.trivial k ↥⊥ ↑B) g) ((Hom.hom f) a)

The induced map applies the underlying map to every generator.

theorem Rep.indBotCounit_naturality {k G : Type u} [Group G] [CommRing k] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (indBotMap f) B.indBotCounit = CategoryTheory.CategoryStruct.comp A.indBotCounit f

The projection from an induced representation is natural in the representation.

theorem Rep.indBotCounit_naturality_assoc {k G : Type u} [Group G] [CommRing k] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) {Z : Rep.{u, u, u} k G} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (indBotMap f) (CategoryTheory.CategoryStruct.comp B.indBotCounit h) = CategoryTheory.CategoryStruct.comp A.indBotCounit (CategoryTheory.CategoryStruct.comp f h)

The projection from an induced representation is natural in the representation.

noncomputable def Rep.fromIndBot {k G : Type u} [Group G] [CommRing k] (B : Rep.{u, u, u} k G) {X : Type u} [AddCommGroup X] [Module k X] (s : X →ₗ[k] ↑B) : indBot k G X ⟶ B

The morphism ⟦g ⊗ₜ x⟧ ↦ g⁻¹ • s x to a representation from the representation induced from the trivial subgroup, attached to a k-linear map s.

Equations

• B.fromIndBot s = CategoryTheory.CategoryStruct.comp (Rep.indMap ⊥.subtype ((Rep.trivialFunctor k ↥⊥).map (ModuleCat.ofHom s))) B.indBotCounit

theorem Rep.fromIndBot_hom_mk {k G : Type u} [Group G] [CommRing k] (B : Rep.{u, u, u} k G) {X : Type u} [AddCommGroup X] [Module k X] (s : X →ₗ[k] ↑B) (g : G) (x : X) : (Hom.hom (B.fromIndBot s)) ((Representation.IndV.mk ⊥.subtype (Representation.trivial k (↥⊥) X) g) x) = (B.ρ g⁻¹) (s x)

The morphism attached to s on generators: ⟦g ⊗ₜ x⟧ ↦ g⁻¹ • s x.

theorem Rep.fromIndBot_comp_of_rightInverse {k G : Type u} [Group G] [CommRing k] {A B : Rep.{u, u, u} k G} (f : B ⟶ A) {s : ↑A →ₗ[k] ↑B} (hs : Function.RightInverse ⇑s ⇑(Hom.hom f)) : CategoryTheory.CategoryStruct.comp (B.fromIndBot s) f = A.indBotCounit

If s is a section of f : B ⟶ A, then ⟦g ⊗ₜ a⟧ ↦ g⁻¹ • s a followed by f is the projection of the representation induced from the trivial subgroup onto A.

theorem Rep.fromIndBot_comp_of_rightInverse_assoc {k G : Type u} [Group G] [CommRing k] {A B : Rep.{u, u, u} k G} (f : B ⟶ A) {s : ↑A →ₗ[k] ↑B} (hs : Function.RightInverse ⇑s ⇑(Hom.hom f)) {Z : Rep.{u, u, u} k G} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (B.fromIndBot s) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp A.indBotCounit h

If s is a section of f : B ⟶ A, then ⟦g ⊗ₜ a⟧ ↦ g⁻¹ • s a followed by f is the projection of the representation induced from the trivial subgroup onto A.

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

Induction on the underlying module, viewed as an endofunctor of representations.

Equations

• Rep.indBotRepFunctor = (CategoryTheory.forget₂ (Rep.{?u.1, ?u.1, ?u.1} k G) (ModuleCat k)).comp (Rep.indBotFunctor k G)

@[simp]

theorem Rep.indBotRepFunctor_obj {k G : Type u} [Group G] [CommRing k] (A : Rep.{u, u, u} k G) : indBotRepFunctor.obj A = indBot k G ↑A

The induction endofunctor acts on objects by induction of underlying modules.

@[simp]

theorem Rep.indBotRepFunctor_map {k G : Type u} [Group G] [CommRing k] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) : indBotRepFunctor.map f = indBotMap f

The induction endofunctor acts on morphisms by indBotMap.

noncomputable def Rep.indBotCounitNatTrans {k G : Type u} [Group G] [CommRing k] : indBotRepFunctor ⟶ CategoryTheory.Functor.id (Rep.{u, u, u} k G)

The canonical projection from induction, as a natural transformation.

Equations

• Rep.indBotCounitNatTrans = { app := fun (A : Rep.{?u.1, ?u.1, ?u.1} k G) => A.indBotCounit, naturality := ⋯ }

@[simp]

theorem Rep.indBotCounitNatTrans_app {k G : Type u} [Group G] [CommRing k] (A : Rep.{u, u, u} k G) : indBotCounitNatTrans.app A = A.indBotCounit

The component of the induction counit at A is its canonical projection.

noncomputable def Rep.indBotEquivFinsupp (k G : Type u) [Group G] [CommRing k] (X : Type u) [AddCommGroup X] [Module k X] : ↑(indBot k G X) ≃ₗ[k] G →₀ X

The underlying module of the representation induced from the trivial subgroup is the module of finitely supported functions G →₀ X, ⟦g ⊗ₜ x⟧ ↦ single g x: the coinvariants of the trivial group are the whole module k[G] ⊗ X.

Equations

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

theorem Rep.indBotEquivFinsupp_mk {k G : Type u} [Group G] [CommRing k] (X : Type u) [AddCommGroup X] [Module k X] (g : G) (x : X) : (indBotEquivFinsupp k G X) ((Representation.IndV.mk ⊥.subtype (Representation.trivial k (↥⊥) X) g) x) = Finsupp.single g x

The underlying module of the induced representation on generators: ⟦g ⊗ₜ x⟧ ↦ single g x.

theorem Rep.indBotEquivFinsupp_ρ_apply {k G : Type u} [Group G] [CommRing k] (X : Type u) [AddCommGroup X] [Module k X] (g : G) (v : ↑(indBot k G X)) (h : G) : ((indBotEquivFinsupp k G X) (((indBot k G X).ρ g) v)) h = ((indBotEquivFinsupp k G X) v) (h * g)

G acts on the finitely supported functions underlying the representation induced from the trivial subgroup by right translation: (g • v) h = v (h * g).

noncomputable def Rep.indBotIsoLeftRegular {k G : Type u} [Group G] [CommRing k] : indBot k G k ≅ leftRegular k G

For any group, k[G] is induced from the trivial subgroup: Ind_⊥^G k ≅ k[G ⧸ ⊥] ≅ k[G].

Equations

• Rep.indBotIsoLeftRegular = TauCeti.indTrivialIso k ⊥ ≪≫ TauCeti.quotientBotIsoLeftRegular k

@[simp]

theorem Rep.indBotIsoLeftRegular_hom_hom_apply_coeff {k G : Type u} [Group G] [CommRing k] (v : ↑(indBot k G k)) (g : G) : ((Hom.hom indBotIsoLeftRegular.hom) v).coeff g = ((indBotEquivFinsupp k G k) v) g⁻¹

The isomorphism from induction out of the trivial subgroup to the left regular representation reads the underlying finitely supported function with inverted indices.

@[simp]

theorem Rep.indBotEquivFinsupp_indBotIsoLeftRegular_inv_hom_apply {k G : Type u} [Group G] [CommRing k] (v : ↑(leftRegular k G)) (g : G) : ((indBotEquivFinsupp k G k) ((Hom.hom indBotIsoLeftRegular.inv) v)) g = v.coeff g⁻¹

The inverse isomorphism, from the left regular representation back to induction out of the trivial subgroup, likewise reads the underlying finitely supported function with inverted indices.

noncomputable def Rep.indBotIsoCoindBot {k G : Type u} [Group G] [CommRing k] [Finite G] (X : Type u) [AddCommGroup X] [Module k X] : indBot k G X ≅ coindBot k G X

For a finite group, induction and coinduction from the trivial subgroup agree.

Equations

• Rep.indBotIsoCoindBot X = (Rep.trivial k (↥⊥) X).indCoindIso

noncomputable def Rep.leftRegularIsoCoindBot {k G : Type u} [Group G] [CommRing k] [Finite G] : leftRegular k G ≅ coindBot k G k

For a finite group, the left regular representation k[G] is coinduced from the trivial subgroup.

Equations

• Rep.leftRegularIsoCoindBot = Rep.indBotIsoLeftRegular.symm ≪≫ Rep.indBotIsoCoindBot k

noncomputable def Rep.resCoindBotIso {k G : Type u} [Group G] [CommRing k] (S : Subgroup G) (X : Type u) [AddCommGroup X] [Module k X] : res S.subtype (coindBot k G X) ≅ coindBot k (↥S) (G ⧸ S → X)

The restriction to a subgroup S of a representation coinduced from the trivial subgroup of G is coinduced from the trivial subgroup of S, on [G : S] copies of the coefficients: f ↦ (s ↦ (y ↦ f (y.out * s))) (resCoindBotIso_hom_hom_apply_coe).

Equations

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

@[simp]

theorem Rep.resCoindBotIso_hom_hom_apply_coe {k G : Type u} [Group G] [CommRing k] (S : Subgroup G) (X : Type u) [AddCommGroup X] [Module k X] (f : ↑(coindBot k G X)) (s : ↥S) (y : G ⧸ S) : ↑((Hom.hom (resCoindBotIso S X).hom) f) s y = ↑f (Quotient.out y * ↑s)

The restriction of a coinduced representation to S: f ↦ (s ↦ (y ↦ f (y.out * s))).

@[simp]

theorem Rep.resCoindBotIso_inv_hom_apply_coe {k G : Type u} [Group G] [CommRing k] (S : Subgroup G) (X : Type u) [AddCommGroup X] [Module k X] (F : ↑(coindBot k (↥S) (G ⧸ S → X))) (g : G) : ↑((Hom.hom (resCoindBotIso S X).inv) F) g = ↑F (Subgroup.groupEquivQuotientProdSubgroup g).2 ↑g

The inverse of the restriction of a coinduced representation to S: a function F : S → (G ⧸ S → X) goes to g ↦ F (⟦g⟧.out⁻¹ * g) ⟦g⟧, read through Mathlib's decomposition Subgroup.groupEquivQuotientProdSubgroup of g.

noncomputable def Rep.resIndBotIso {k G : Type u} [Group G] [CommRing k] (S : Subgroup G) (X : Type u) [AddCommGroup X] [Module k X] : res S.subtype (indBot k G X) ≅ indBot k (↥S) (G ⧸ S →₀ X)

The restriction to a subgroup S of a representation induced from the trivial subgroup of G is induced from the trivial subgroup of S, on the finitely supported functions G ⧸ S →₀ X: a finitely supported function on G = S × G ⧸ S is a finitely supported function on S with values finitely supported on G ⧸ S (indBotEquivFinsupp_resIndBotIso_hom_hom_apply).

Equations

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

@[simp]

theorem Rep.indBotEquivFinsupp_resIndBotIso_hom_hom_apply {k G : Type u} [Group G] [CommRing k] (S : Subgroup G) (X : Type u) [AddCommGroup X] [Module k X] (v : ↑(indBot k G X)) (s : ↥S) (y : G ⧸ S) : (((indBotEquivFinsupp k (↥S) (G ⧸ S →₀ X)) ((Hom.hom (resIndBotIso S X).hom) v)) s) y = ((indBotEquivFinsupp k G X) v) (Quotient.out y * ↑s)

The restriction of an induced representation to S: the finitely supported function attached to v sends s to the finitely supported function y ↦ v (y.out * s).

@[simp]

theorem Rep.indBotEquivFinsupp_resIndBotIso_inv_hom_apply {k G : Type u} [Group G] [CommRing k] (S : Subgroup G) (X : Type u) [AddCommGroup X] [Module k X] (W : ↑(indBot k (↥S) (G ⧸ S →₀ X))) (g : G) : ((indBotEquivFinsupp k G X) ((Hom.hom (resIndBotIso S X).inv) W)) g = (((indBotEquivFinsupp k (↥S) (G ⧸ S →₀ X)) W) (Subgroup.groupEquivQuotientProdSubgroup g).2) ↑g

The inverse of the restriction of an induced representation to S: the finitely supported function on G attached to W evaluates W at the decomposition g = ⟦g⟧.out * (⟦g⟧.out⁻¹ * g) of g into a coset and an element of S.

noncomputable def Rep.quotientToInvariantsCoindBotIso {k G : Type u} [Group G] [CommRing k] (S : Subgroup G) (X : Type u) [AddCommGroup X] [Module k X] [S.Normal] : (coindBot k G X).quotientToInvariants S ≅ coindBot k (G ⧸ S) X

For a normal subgroup S, the S-invariants of the representation coinduced from the trivial subgroup of G are coinduced from the trivial subgroup of G ⧸ S: an S-invariant function on G is a function on G ⧸ S, f ↦ (y ↦ f y.out) (quotientToInvariantsCoindBotIso_hom_hom_apply_coe).

Equations

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

@[simp]

theorem Rep.quotientToInvariantsCoindBotIso_hom_hom_apply_coe {k G : Type u} [Group G] [CommRing k] (S : Subgroup G) (X : Type u) [AddCommGroup X] [Module k X] [S.Normal] (f : ↑((coindBot k G X).quotientToInvariants S)) (y : G ⧸ S) : ↑((Hom.hom (quotientToInvariantsCoindBotIso S X).hom) f) y = ↑↑f (Quotient.out y)

The S-invariants of a coinduced representation, as a function on G ⧸ S: f ↦ (y ↦ f y.out).

@[simp]

theorem Rep.quotientToInvariants_coindBot_apply_out_mk {k G : Type u} [Group G] [CommRing k] (S : Subgroup G) (X : Type u) [AddCommGroup X] [Module k X] [S.Normal] (f : ↑((coindBot k G X).quotientToInvariants S)) (g : G) : ↑↑f (Quotient.out ↑g) = ↑↑f g

An invariant function has the same value at a representative and at the chosen representative of its coset. Together with quotientToInvariantsCoindBotIso_hom_hom_apply_coe, this evaluates the forward isomorphism on cosets of representatives.

@[simp]

theorem Rep.quotientToInvariantsCoindBotIso_inv_hom_apply_coe_coe {k G : Type u} [Group G] [CommRing k] (S : Subgroup G) (X : Type u) [AddCommGroup X] [Module k X] [S.Normal] (F : ↑(coindBot k (G ⧸ S) X)) (g : G) : ↑↑((Hom.hom (quotientToInvariantsCoindBotIso S X).inv) F) g = ↑F ↑g

A function on G ⧸ S, as an S-invariant function on G: F ↦ (g ↦ F ⟦g⟧).