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} [Semiring 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} [Semiring 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)}

@[simp]

theorem Representation.mem_coindV {k : Type u_1} {G : Type u_2} {H : Type u_3} [Semiring k] [Monoid G] [Monoid H] (φ : G →* H) {A : Type u_4} [AddCommMonoid A] [Module k A] (σ : Representation k G A) (f : H → A) : f ∈ coindV φ σ ↔ ∀ (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} [Semiring k] [Monoid G] [Monoid H] (φ : G →* H) {B : Type u_5} [AddCommMonoid B] [Module k B] (ρ : Representation k G B) : 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 B 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} [Semiring k] [Monoid G] [Monoid H] (φ : G →* H) {B : Type u_5} [AddCommMonoid B] [Module k B] (ρ : Representation k G B) (h : H) : (coind φ ρ) h = (LinearMap.funLeft k B fun (x : H) => x * h).restrict ⋯

def Representation.coindMap {k : Type u_1} {G : Type u_2} {H : Type u_3} [Semiring k] [Monoid G] [Monoid H] (φ : G →* H) {A : Type u_4} {B : Type u_5} [AddCommMonoid A] [Module k A] [AddCommMonoid B] [Module k B] {σ : Representation k G A} {ρ : Representation k G B} (f : σ.IntertwiningMap ρ) : (coind φ σ).IntertwiningMap (coind φ ρ)

Given a monoid homomorphism φ : G →* H and an intertwining map f : σ ⟶ ρ, there is a natural intertwining map coind φ σ ⟶ coind φ ρ given by postcomposition by f.

Equations

• Representation.coindMap φ f = { toLinearMap := (f.compLeft H).restrict ⋯, isIntertwining' := ⋯ }

theorem Representation.coindMap_coe_apply {k : Type u_1} {G : Type u_2} {H : Type u_3} [Semiring k] [Monoid G] [Monoid H] (φ : G →* H) {A : Type u_4} {B : Type u_5} [AddCommMonoid A] [Module k A] [AddCommMonoid B] [Module k B] (σ : Representation k G A) (ρ : Representation k G B) (f : σ.IntertwiningMap ρ) (x : ↥(coindV φ σ)) : ↑((coindMap φ f) x) = (f.compLeft H) ↑x

@[simp]

theorem Representation.coindMap_coe_apply_apply {k : Type u_1} {G : Type u_2} {H : Type u_3} [Semiring k] [Monoid G] [Monoid H] (φ : G →* H) {A : Type u_4} {B : Type u_5} [AddCommMonoid A] [Module k A] [AddCommMonoid B] [Module k B] (σ : Representation k G A) (ρ : Representation k G B) (f : σ.IntertwiningMap ρ) (x : ↥(coindV φ σ)) (h : H) : ↑((coindMap φ f) x) h = f (↑x h)

@[reducible, inline]

noncomputable abbrev Rep.coind {k : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (A : Rep.{u_1, u, v} k G) : Rep.{max w u_1, u, w} 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.{?u.44, ?u.43, ?u.42, ?u.41} φ A = Rep.of (Representation.coind φ A.ρ)

@[reducible, inline]

noncomputable abbrev Rep.coindMap {k : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) {A B : Rep.{u_1, u, v} k G} (f : A ⟶ B) : coind.{u, v, w, u_1} φ A ⟶ coind.{u, v, w, u_1} φ 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 = Rep.ofHom (Representation.coindMap φ (Rep.Hom.hom f))

noncomputable def Rep.coindFunctor (k : Type u) {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) : CategoryTheory.Functor (Rep.{t, u, v} k G) (Rep.{max w t, u, w} 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

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

@[simp]

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

@[simp]

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

instance Rep.instPreservesEpimorphismsSubtypeMemSubgroupCoindFunctorSubtype {k : Type u} [CommRing k] {G : Type v'} [Group G] (S : Subgroup G) : (coindFunctor k S.subtype).PreservesEpimorphisms

noncomputable def Representation.coind' {k : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (A : Rep.{max u w, u, v} k G) : Representation k H (Rep.res φ (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 : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (A : Rep.{max u w, u, v} k G) (h : H) (f : Rep.res φ (Rep.leftRegular k H) ⟶ A) : ((coind' φ A) h) f = CategoryTheory.CategoryStruct.comp ((Rep.resFunctor φ).map (↑(Rep.leftRegular k H).leftRegularHomEquiv.symm (Finsupp.single h 1))) f

@[reducible, inline]

noncomputable abbrev Rep.coind' {k : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (A : Rep.{max u w, u, v} k G) : Rep.{max u w, u, w} 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 : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) {A : Rep.{max u w, u, v} k G} {f g : ↑(coind' φ A)} (hfg : ∀ (h : H), (Hom.hom f).toLinearMap (Finsupp.single h 1) = (Hom.hom g).toLinearMap (Finsupp.single h 1)) : f = g

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

noncomputable def Rep.coindMap' {k : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) {A B : Rep.{max u w, u, v} 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 = Rep.ofHom (let __spread.0 := CategoryTheory.Linear.rightComp k (Rep.res φ (Rep.leftRegular k H)) f; { toLinearMap := __spread.0, isIntertwining' := ⋯ })

noncomputable def Rep.coindFunctor' (k : Type u) {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) : CategoryTheory.Functor (Rep.{max u w, u, v} k G) (Rep.{max u w, u, w} 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

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

@[simp]

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

@[simp]

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

noncomputable def Rep.coindVEquiv {k : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (A : Rep.{max u w, u, v} k G) : ↥(Representation.coindV φ A.ρ) ≃ₗ[k] res φ (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_symm_apply_coe {k : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (A : Rep.{max u w, u, v} k G) (f : res φ (leftRegular k H) ⟶ A) (h : H) : ↑((coindVEquiv φ A).symm f) h = (Hom.hom f).toLinearMap (Finsupp.single h 1)

@[simp]

theorem Rep.coindVEquiv_apply {k : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (A : Rep.{max u w, u, v} k G) (f : ↥(Representation.coindV φ A.ρ)) : (coindVEquiv φ A) f = ofHom { toLinearMap := Finsupp.linearCombination k ↑f, isIntertwining' := ⋯ }

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

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

Equations

• Rep.coindIso φ A = Rep.mkIso (Representation.Equiv.mk (Rep.coindVEquiv φ A) ⋯)

noncomputable def Rep.coindFunctorIso {k : Type u} {G : Type v} {H : Type w} [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_inv_app_hom_toFun_coe {k : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (X : Rep.{max u w, u, v} k G) (a : res φ (leftRegular k H) ⟶ X) (h : H) : ↑((Hom.hom ((coindFunctorIso φ).inv.app X)) a) h = (Hom.hom a) (Finsupp.single h 1)

@[simp]

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

def Rep.resCoindToHom {k : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (B : Rep.{max u_1 w, u, w} k H) (A : Rep.{max u_1 w, u, v} k G) (f : res φ B ⟶ A) : B ⟶ coind.{u, v, w, max u_1 w} φ A

The morphism induced by the adjunction between res φ and coind φ sending a morphism f : res φ B ⟶ A to the morphism B ⟶ coind φ A given by the underlying linear map sending b : B.V to the function sending h : H to f ((B.ρ h) b).

Equations

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

@[simp]

theorem Rep.resCoindToHom_hom_apply_coe {k : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (B : Rep.{max w u_1, u, w} k H) (A : Rep.{max w u_1, u, v} k G) (f : res φ B ⟶ A) (c : ↑B) (i : H) : ↑((Hom.hom (resCoindToHom φ B A f)) c) i = (Hom.hom f) ((B.ρ i) c)

def Rep.resCoindHomEquiv {k : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (B : Rep.{max w t, u, w} k H) (A : Rep.{max w t, u, v} k G) : (res φ B ⟶ A) ≃ₗ[k] B ⟶ coind.{u, v, w, max t w} φ 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 res φ B ⟶ A and the H-representation morphisms B ⟶ coind φ A.

Note Rep.resCoindHomEquiv.{t, u, v, w} has the property that even with all inputs explicitly given, the first universe cannot be synthesized.

Equations

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

@[simp]

theorem Rep.resCoindHomEquiv_symm_apply {k : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (B : Rep.{max w t, u, w} k H) (A : Rep.{max w t, u, v} k G) (f : B ⟶ coind.{u, v, w, max t w} φ A) : (resCoindHomEquiv.{t, u, v, w} φ B A).symm f = ofHom { toLinearMap := LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap, isIntertwining' := ⋯ }

@[simp]

theorem Rep.resCoindHomEquiv_apply {k : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) (B : Rep.{max w t, u, w} k H) (A : Rep.{max w t, u, v} k G) (f : res φ B ⟶ A) : (resCoindHomEquiv.{t, u, v, w} φ B A) f = resCoindToHom φ B A f

@[reducible, inline]

noncomputable abbrev Rep.resCoindAdjunction (k : Type u) {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) : resFunctor φ ⊣ 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.

instance Rep.instIsRightAdjointCoindFunctor {k : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) : (coindFunctor k φ).IsRightAdjoint

instance Rep.instIsLeftAdjointResFunctor {k : Type u} {G : Type v} {H : Type w} [CommRing k] [Monoid G] [Monoid H] (φ : G →* H) : (resFunctor φ).IsLeftAdjoint

instance Rep.instPreservesProjectiveObjectsSubtypeMemSubgroupResFunctorSubtype {k : Type u} [CommRing k] {G : Type w} [Group G] (S : Subgroup G) : (resFunctor S.subtype).PreservesProjectiveObjects