Induced representations

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

By ind φ A we mean the (k[H] ⊗[k] A)_G with the G-representation on k[H] defined by φ. We define a representation of H on this submodule by sending h : H and ⟦h₁ ⊗ₜ a⟧ to ⟦h₁h⁻¹ ⊗ₜ a⟧.

We also prove that the restriction functor Rep k H ⥤ Rep k G along φ is right adjoint to the induction functor and hence that the induction functor preserves colimits.

Main definitions

• Representation.ind φ ρ : given a group homomorphism φ : G →* H, this is the induction of a G-representation (A, ρ) along φ, defined as (k[H] ⊗[k] A)_G and with H-action given by h • ⟦h₁ ⊗ₜ a⟧ := ⟦h₁h⁻¹ ⊗ₜ a⟧ for h, h₁ : H, a : A.
• Rep.indResAdjunction k φ: given a group homomorphism φ : G →* H, this is the adjunction between the induction functor along φ and the restriction functor Rep k H ⥤ Rep k G along φ.

@[reducible, inline]

abbrev Representation.IndV {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} [AddCommGroup A] [Module k A] (ρ : Representation k G A) : Type (max u_4 u_1 u_3)

Given a group homomorphism φ : G →* H and a G-representation (A, ρ), this is the k-module (k[H] ⊗[k] A)_G with the G-representation on k[H] defined by φ. See Representation.ind for the induced H-representation on IndV φ ρ.

Equations

• Representation.IndV φ ρ = (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) ρ).Coinvariants

@[reducible, inline]

noncomputable abbrev Representation.IndV.mk {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} [AddCommGroup A] [Module k A] (ρ : Representation k G A) (h : H) : A →ₗ[k] IndV φ ρ

Given a group homomorphism φ : G →* H and a G-representation (A, ρ), this is the H → A →ₗ[k] (k[H] ⊗[k] A)_G sending h, a to ⟦h ⊗ₜ a⟧.

Equations

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

theorem Representation.IndV.hom_ext {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} {B : Type u_5} [AddCommGroup A] [Module k A] (ρ : Representation k G A) [AddCommGroup B] [Module k B] {f g : IndV φ ρ →ₗ[k] B} (hfg : ∀ (h : H), f ∘ₗ mk φ ρ h = g ∘ₗ mk φ ρ h) : f = g

theorem Representation.IndV.hom_ext_iff {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] {φ : G →* H} {A : Type u_4} {B : Type u_5} [AddCommGroup A] [Module k A] {ρ : Representation k G A} [AddCommGroup B] [Module k B] {f g : IndV φ ρ →ₗ[k] B} : f = g ↔ ∀ (h : H), f ∘ₗ mk φ ρ h = g ∘ₗ mk φ ρ h

noncomputable def Representation.ind {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} [AddCommGroup A] [Module k A] (ρ : Representation k G A) : Representation k H (IndV φ ρ)

Given a group homomorphism φ : G →* H and a G-representation A, this is (k[H] ⊗[k] A)_G equipped with the H-representation defined by sending h : H and ⟦h₁ ⊗ₜ a⟧ to ⟦h₁h⁻¹ ⊗ₜ a⟧.

Equations

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

@[simp]

theorem Representation.ind_apply {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} [AddCommGroup A] [Module k A] (ρ : Representation k G A) (h : H) : (ind φ ρ) h = Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) (LinearMap.rTensor A (Finsupp.lmapDomain k k fun (x : H) => x * h⁻¹)) ⋯

theorem Representation.ind_mk {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} [AddCommGroup A] [Module k A] (ρ : Representation k G A) (h₁ h₂ : H) (a : A) : ((ind φ ρ) h₁) ((IndV.mk φ ρ h₂) a) = (IndV.mk φ ρ (h₂ * h₁⁻¹)) a

@[reducible, inline]

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

Given a group homomorphism φ : G →* H and a G-representation A, this is (k[H] ⊗[k] A)_G equipped with the H-representation defined by sending h : H and ⟦h₁ ⊗ₜ a⟧ to ⟦h₁h⁻¹ ⊗ₜ a⟧.

Equations

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

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

Given a group homomorphism φ : G →* H, a morphism of G-representations f : A ⟶ B induces a morphism of H-representations (k[H] ⊗[k] A)_G ⟶ (k[H] ⊗[k] B)_G.

Equations

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

@[simp]

theorem Rep.indMap_hom {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) {A B : Rep k G} (f : A ⟶ B) : (indMap φ f).hom = ModuleCat.ofHom (Representation.Coinvariants.map (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ) (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) B.ρ) (LinearMap.lTensor (H →₀ k) (ModuleCat.Hom.hom f.hom)) ⋯)

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

Given a group homomorphism φ : G →* H, this is the functor sending a G-representation A to the induced H-representation ind φ A, with action on maps induced by left tensoring.

Equations

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

@[simp]

theorem Rep.indFunctor_map (k : Type u) {G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) {X✝ Y✝ : Rep k G} (f : X✝ ⟶ Y✝) : (indFunctor k φ).map f = indMap φ f

@[simp]

theorem Rep.indFunctor_obj (k : Type u) {G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) : (indFunctor k φ).obj A = ind φ A

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

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

Equations

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

@[simp]

theorem Rep.indResHomEquiv_symm_apply_hom {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) (B : Rep k H) (f : A ⟶ (Action.res (ModuleCat k) φ).obj B) : ((indResHomEquiv φ A B).symm f).hom = ModuleCat.ofHom (Representation.Coinvariants.lift (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ) (TensorProduct.lift ((Finsupp.lift (↑A.V →ₗ[k] ↑B.1) k H) fun (h : H) => B.ρ h⁻¹ ∘ₗ ModuleCat.Hom.hom f.hom)) ⋯)

@[simp]

theorem Rep.indResHomEquiv_apply_hom {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) (B : Rep k H) (f : ind φ A ⟶ B) : ((indResHomEquiv φ A B) f).hom = ModuleCat.ofHom (ModuleCat.Hom.hom f.hom ∘ₗ Representation.IndV.mk φ A.ρ 1)

noncomputable def Rep.indResAdjunction (k : Type u) {G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) : indFunctor k φ ⊣ Action.res (ModuleCat k) φ

Given a group homomorphism φ : G →* H, the induction functor Rep k G ⥤ Rep k H is left adjoint to the restriction functor along φ.

Equations

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

@[simp]

theorem Rep.indResAdjunction_unit_app_hom_hom (k : Type u) {G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (X : Rep k G) : ModuleCat.Hom.hom ((indResAdjunction k φ).unit.app X).hom = Representation.IndV.mk φ X.ρ 1

@[simp]

theorem Rep.indResAdjunction_counit_app_hom_hom (k : Type u) {G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (Y : Rep k H) : ModuleCat.Hom.hom ((indResAdjunction k φ).counit.app Y).hom = Representation.Coinvariants.lift (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) ((Action.res (ModuleCat k) φ).obj Y).ρ) (TensorProduct.lift ((Finsupp.lift (↑Y.V →ₗ[k] ↑Y.1) k H) fun (h : H) => Y.ρ h⁻¹)) ⋯

instance Rep.instPreservesColimitsIndFunctor {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) : CategoryTheory.Limits.PreservesColimits (indFunctor k φ)

instance Rep.instPreservesLimitsActionModuleCatRes {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) : CategoryTheory.Limits.PreservesLimits (Action.res (ModuleCat k) φ)