Coinduced representations

Given a commutative ring k, a monoid homomorphism φ : G →* H, and a k-linear G-representation A, this file introduces the coinduced representation $Coind_G^H(A)$ of A as an H-representation.

By coind φ A we mean the submodule of functions H → A such that for all g : G, h : H, f (φ g * h) = ρ g (f h). We define a representation of H on this submodule by sending h : H and f : coind φ A to the function H → A sending h₁ to f (h₁ * h).

Alternatively, we could define $Coind_G^H(A)$ as the morphisms $Hom(k[H], A)$ in the category Rep k G, which we equip with the H-representation sending h : H and f : k[H] ⟶ A to the representation morphism sending r · h₁ to r • f (h₁ * h). We include this definition as coind' φ A and prove the two representations are isomorphic.

We also prove that the restriction functor Rep k H ⥤ Rep k G along φ is left adjoint to the coinduction functor and hence that the coinduction functor preserves limits.

Main definitions

• Representation.coind φ ρ : the coinduction of ρ along φ defined as the k-submodule of G-equivariant functions H → A, with H-action given by (h • f) h₁ := f (h₁ * h) for f : H → A, h, h₁ : H.
• Representation.coind' φ A : the coinduction of A along φ defined as the set of G-representation morphisms k[H] ⟶ A, with H-action given by (h • f) (r • h₁) := r • f(h₁ * h) for f : k[H] ⟶ A, h, h₁ : H, r : k.
• Rep.resCoindAdjunction k φ: given a monoid homomorphism φ : G →* H, this is the adjunction between the restriction functor Rep k H ⥤ Rep k G along φ and the coinduction functor along φ.

def Representation.coindV {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommSemiring k] [Monoid G] [Monoid H] (φ : G →* H) {A : Type u_4} [AddCommMonoid A] [Module k A] (ρ : Representation k G A) : Submodule k (H → A)

If ρ : Representation k G A and φ : G →* H then coindV φ ρ is the sub-k-module of functions H → A underlying the coinduction of ρ along φ, i.e., the functions f : H → A such that f (φ g * h) = (ρ g) (f h) for all g : G and h : H.

Equations

• Representation.coindV φ ρ = { carrier := {f : H → A | ∀ (g : G) (h : H), f (φ g * h) = (ρ g) (f h)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Representation.coe_coindV {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommSemiring k] [Monoid G] [Monoid H] (φ : G →* H) {A : Type u_4} [AddCommMonoid A] [Module k A] (ρ : Representation k G A) : ↑(coindV φ ρ) = {f : H → A | ∀ (g : G) (h : H), f (φ g * h) = (ρ g) (f h)}

def Representation.coind {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommSemiring k] [Monoid G] [Monoid H] (φ : G →* H) {A : Type u_4} [AddCommMonoid A] [Module k A] (ρ : Representation k G A) : Representation k H ↥(coindV φ ρ)

If ρ : Representation k G A and φ : G →* H then coind φ ρ is the representation coinduced by ρ along φ, defined as the following action of H on the submodule coindV φ ρ of G-equivariant functions from H to A: we let h : H send the function f : H → A to the function sending h₁ to f (h₁ * h).

See also Rep.coind and Representation.coind' for variants involving the category Rep k G.

Equations

• Representation.coind φ ρ = { toFun := fun (h : H) => (LinearMap.funLeft k A fun (x : H) => x * h).restrict ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Representation.coind_apply {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommSemiring k] [Monoid G] [Monoid H] (φ : G →* H) {A : Type u_4} [AddCommMonoid A] [Module k A] (ρ : Representation k G A) (h : H) : (coind φ ρ) h = (LinearMap.funLeft k A fun (x : H) => x * h).restrict ⋯

@[reducible, inline]

noncomputable abbrev Rep.coind {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (A : Rep k G) : Rep k H

If φ : G →* H and A : Rep k G then coind φ A is the coinduction of A along φ, defined by letting H act on the G-equivariant functions H → A by (h • f) h₁ := f (h₁ * h).

Equations

• Rep.coind φ A = Rep.of (Representation.coind φ A.ρ)

noncomputable def Rep.coindMap {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) {A B : Rep k G} (f : A ⟶ B) : coind φ A ⟶ coind φ B

Given a monoid morphism φ : G →* H and a morphism of G-representations f : A ⟶ B, there is a natural H-representation morphism coind φ A ⟶ coind φ B, given by postcomposition by f.

Equations

• Rep.coindMap φ f = { hom := ModuleCat.ofHom (((ModuleCat.Hom.hom f.hom).compLeft H).restrict ⋯), comm := ⋯ }

@[simp]

theorem Rep.coindMap_hom {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) {A B : Rep k G} (f : A ⟶ B) : (coindMap φ f).hom = ModuleCat.ofHom (((ModuleCat.Hom.hom f.hom).compLeft H).restrict ⋯)

noncomputable def Rep.coindFunctor (k : Type u) {G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) : CategoryTheory.Functor (Rep k G) (Rep k H)

Given a monoid homomorphism φ : G →* H, this is the functor sending a G-representation A to the coinduced H-representation coind φ A, with action on maps given by postcomposition.

Equations

• Rep.coindFunctor k φ = { obj := fun (A : Rep k G) => Rep.coind φ A, map := fun {X Y : Rep k G} (f : X ⟶ Y) => Rep.coindMap φ f, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem Rep.coindFunctor_map (k : Type u) {G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) {X✝ Y✝ : Rep k G} (f : X✝ ⟶ Y✝) : (coindFunctor k φ).map f = coindMap φ f

@[simp]

theorem Rep.coindFunctor_obj (k : Type u) {G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (A : Rep k G) : (coindFunctor k φ).obj A = coind φ A

noncomputable def Representation.coind' {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (A : Rep k G) : Representation k H ((Action.res (ModuleCat k) φ).obj (Rep.leftRegular k H) ⟶ A)

If φ : G →* H and A : Rep k G then coind' φ A, the coinduction of A along φ, is defined as an H-action on Hom_{k[G]}(k[H], A). If f : k[H] → A is G-equivariant then (h • f) (r • h₁) := r • f (h₁ * h), where r : k.

Equations

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

@[simp]

theorem Representation.coind'_apply_apply {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (A : Rep k G) (h : H) (f : (Action.res (ModuleCat k) φ).obj (Rep.leftRegular k H) ⟶ A) : ((coind' φ A) h) f = CategoryTheory.CategoryStruct.comp ((Action.res (ModuleCat k) φ).map ((Rep.leftRegular k H).leftRegularHomEquiv.symm (Finsupp.single h 1))) f

@[reducible, inline]

noncomputable abbrev Rep.coind' {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (A : Rep k G) : Rep k H

If φ : G →* H and A : Rep k G then coind' φ A, the coinduction of A along φ, is defined as an H-action on Hom_{k[G]}(k[H], A). If f : k[H] → A is G-equivariant then (h • f) (r • h₁) := r • f (h₁ * h), where r : k.

Equations

• Rep.coind' φ A = Rep.of (Representation.coind' φ A)

theorem Rep.coind'_ext {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) {A : Rep k G} {f g : ↑(coind' φ A).V} (hfg : ∀ (h : H), (CategoryTheory.ConcreteCategory.hom f.hom) (Finsupp.single h 1) = (CategoryTheory.ConcreteCategory.hom g.hom) (Finsupp.single h 1)) : f = g

theorem Rep.coind'_ext_iff {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] {φ : G →* H} {A : Rep k G} {f g : ↑(coind' φ A).V} : f = g ↔ ∀ (h : H), (CategoryTheory.ConcreteCategory.hom f.hom) (Finsupp.single h 1) = (CategoryTheory.ConcreteCategory.hom g.hom) (Finsupp.single h 1)

noncomputable def Rep.coindMap' {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) {A B : Rep k G} (f : A ⟶ B) : coind' φ A ⟶ coind' φ B

Given a monoid morphism φ : G →* H and a morphism of G-representations f : A ⟶ B, there is a natural H-representation morphism coind' φ A ⟶ coind' φ B, given by postcomposition by f.

Equations

• Rep.coindMap' φ f = { hom := ModuleCat.ofHom (CategoryTheory.Linear.rightComp k ((Action.res (ModuleCat k) φ).obj (Rep.leftRegular k H)) f), comm := ⋯ }

@[simp]

theorem Rep.coindMap'_hom {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) {A B : Rep k G} (f : A ⟶ B) : (coindMap' φ f).hom = ModuleCat.ofHom (CategoryTheory.Linear.rightComp k ((Action.res (ModuleCat k) φ).obj (leftRegular k H)) f)

noncomputable def Rep.coindFunctor' (k : Type u) {G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) : CategoryTheory.Functor (Rep k G) (Rep k H)

Given a monoid homomorphism φ : G →* H, this is the functor sending a G-representation A to the coinduced H-representation coind' φ A, with action on maps given by postcomposition.

Equations

• Rep.coindFunctor' k φ = { obj := fun (A : Rep k G) => Rep.coind' φ A, map := fun {X Y : Rep k G} (f : X ⟶ Y) => Rep.coindMap' φ f, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem Rep.coindFunctor'_map (k : Type u) {G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) {X✝ Y✝ : Rep k G} (f : X✝ ⟶ Y✝) : (coindFunctor' k φ).map f = coindMap' φ f

@[simp]

theorem Rep.coindFunctor'_obj (k : Type u) {G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (A : Rep k G) : (coindFunctor' k φ).obj A = coind' φ A

noncomputable def Rep.coindVEquiv {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (A : Rep k G) : ↥(Representation.coindV φ A.ρ) ≃ₗ[k] (Action.res (ModuleCat k) φ).obj (leftRegular k H) ⟶ A

If φ : G →* H and A : Rep k G then the k-submodule of functions f : H → A such that for all g : G, h : H, f (φ g * h) = A.ρ g (f h), is k-linearly equivalent to the G-representation morphisms k[H] ⟶ A.

Equations

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

@[simp]

theorem Rep.coindVEquiv_apply_hom {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (A : Rep k G) (f : ↥(Representation.coindV φ A.ρ)) : ((coindVEquiv φ A) f).hom = ModuleCat.ofHom (Finsupp.linearCombination k ↑f)

@[simp]

theorem Rep.coindVEquiv_symm_apply_coe {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (A : Rep k G) (f : (Action.res (ModuleCat k) φ).obj (leftRegular k H) ⟶ A) (h : H) : ↑((coindVEquiv φ A).symm f) h = (CategoryTheory.ConcreteCategory.hom f.hom) (Finsupp.single h 1)

noncomputable def Rep.coindIso {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (A : Rep k G) : coind φ A ≅ coind' φ A

coind φ A and coind' φ A are isomorphic representations, with the underlying k-linear equivalence given by coindVEquiv.

Equations

• Rep.coindIso φ A = Action.mkIso (Rep.coindVEquiv φ A).toModuleIso ⋯

@[simp]

theorem Rep.coindIso_hom_hom_hom {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (A : Rep k G) : ModuleCat.Hom.hom (coindIso φ A).hom.hom = ↑(coindVEquiv φ A)

@[simp]

theorem Rep.coindIso_inv_hom_hom {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (A : Rep k G) : ModuleCat.Hom.hom (coindIso φ A).inv.hom = ↑(coindVEquiv φ A).symm

noncomputable def Rep.coindFunctorIso {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) : coindFunctor k φ ≅ coindFunctor' k φ

Given a monoid homomorphism φ : G →* H, the coinduction functors Rep k G ⥤ Rep k H given by coindFunctor k φ and coindFunctor' k φ are naturally isomorphic, with isomorphism on objects given by coindIso φ.

Equations

• Rep.coindFunctorIso φ = CategoryTheory.NatIso.ofComponents (Rep.coindIso φ) ⋯

@[simp]

theorem Rep.coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (X : Rep k G) (f : ↥(Representation.coindV φ X.ρ)) (d : H →₀ k) : (ModuleCat.Hom.hom ((ModuleCat.Hom.hom ((coindFunctorIso φ).hom.app X).hom) f).hom) d = d.sum fun (i : H) (c : k) => c • ↑f i

@[simp]

theorem Rep.coindFunctorIso_inv_app_hom_hom_apply_coe {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (X : Rep k G) (a : (Action.res (ModuleCat k) φ).obj (leftRegular k H) ⟶ X) (h : H) : ↑((ModuleCat.Hom.hom ((coindFunctorIso φ).inv.app X).hom) a) h = (CategoryTheory.ConcreteCategory.hom a.hom) (Finsupp.single h 1)

noncomputable def Rep.resCoindHomEquiv {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (B : Rep k H) (A : Rep k G) : ((Action.res (ModuleCat k) φ).obj B ⟶ A) ≃ₗ[k] B ⟶ coind φ A

Given a monoid homomorphism φ : G →* H, an H-representation B, and a G-representation A, there is a k-linear equivalence between the G-representation morphisms B ⟶ A and the H-representation morphisms B ⟶ coind φ A.

Equations

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

@[simp]

theorem Rep.resCoindHomEquiv_apply_hom {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (B : Rep k H) (A : Rep k G) (f : (Action.res (ModuleCat k) φ).obj B ⟶ A) : ((resCoindHomEquiv φ B A) f).hom = ModuleCat.ofHom (LinearMap.codRestrict (Representation.coindV φ A.ρ) (LinearMap.pi fun (h : H) => ModuleCat.Hom.hom f.hom ∘ₗ B.ρ h) ⋯)

@[simp]

theorem Rep.resCoindHomEquiv_symm_apply_hom {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (B : Rep k H) (A : Rep k G) (f : B ⟶ coind φ A) : ((resCoindHomEquiv φ B A).symm f).hom = ModuleCat.ofHom (LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ ModuleCat.Hom.hom f.hom)

@[reducible, inline]

noncomputable abbrev Rep.resCoindAdjunction (k : Type u) {G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) : Action.res (ModuleCat k) φ ⊣ coindFunctor k φ

Given a monoid homomorphism φ : G →* H, the coinduction functor Rep k G ⥤ Rep k H is right adjoint to the restriction functor along φ.

Equations

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

@[simp]

theorem Rep.resCoindAdjunction_counit_app_hom_hom (k : Type u) {G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (Y : Action (ModuleCat k) G) : ModuleCat.Hom.hom ((resCoindAdjunction k φ).counit.app Y).hom = LinearMap.proj 1 ∘ₗ (Representation.coindV φ (ρ Y)).subtype

@[simp]

theorem Rep.resCoindAdjunction_unit_app_hom_hom (k : Type u) {G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (X : Action (ModuleCat k) H) : ModuleCat.Hom.hom ((resCoindAdjunction k φ).unit.app X).hom = LinearMap.codRestrict (Representation.coindV φ (ρ ((Action.res (ModuleCat k) φ).obj X))) (LinearMap.pi fun (h : H) => (ρ X) h) ⋯

instance Rep.instPreservesLimitsCoindFunctor {k G H : Type u} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) : CategoryTheory.Limits.PreservesLimits (coindFunctor k φ)