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.

Additionally, we show that the functor Rep k H ⥤ ModuleCat k sending B : Rep k H to (Ind(φ)(A) ⊗ B))_H is naturally isomorphic to the one sending B to (A ⊗ Res(φ)(B))_G. This is used to prove Shapiro's lemma in Mathlib/RepresentationTheory/Homological/GroupHomology/Shapiro.lean.

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 φ.
• Rep.coinvariantsTensorIndNatIso φ A : given a group homomorphism φ : G →* H and A : Rep k G, this is a natural isomorphism between the functor sending B : Rep k H to (Ind(φ)(A) ⊗ B))_H and the one sending B to (A ⊗ Res(φ)(B))_G. Used to prove Shapiro's lemma.

@[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_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

@[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

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) φ) (MonoidHom.comp Y.ρ φ)) (TensorProduct.lift ((Finsupp.lift (↑Y.V →ₗ[k] ↑Y.1) k H) fun (h : H) => Y.ρ h⁻¹)) ⋯

instance Rep.instIsLeftAdjointIndFunctor {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) : (indFunctor k φ).IsLeftAdjoint

instance Rep.instIsRightAdjointActionModuleCatRes {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) : (Action.res (ModuleCat k) φ).IsRightAdjoint

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

Given a group hom φ : G →* H, A : Rep k G and B : Rep k H, this is the k-linear map (Ind(φ)(A) ⊗ B))_H ⟶ (A ⊗ Res(φ)(B))_G sending ⟦h ⊗ₜ a⟧ ⊗ₜ b to ⟦a ⊗ ρ(h)(b)⟧ for all h : H, a : A, and b : B.

Equations

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

theorem Rep.coinvariantsTensorIndHom_mk_tmul_indVMk {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Rep k G} {B : Rep k H} (h : H) (x : ↑A.V) (y : ↑B.V) : (CategoryTheory.ConcreteCategory.hom (coinvariantsTensorIndHom φ A B)) ((((ind φ A).coinvariantsTensorMk B) ((Representation.IndV.mk φ A.ρ h) x)) y) = ((A.coinvariantsTensorMk ((Action.res (ModuleCat k) φ).obj B)) x) ((B.ρ h) y)

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

Given a group hom φ : G →* H, A : Rep k G and B : Rep k H, this is the k-linear map (A ⊗ Res(φ)(B))_G ⟶ (Ind(φ)(A) ⊗ B))_H sending ⟦a ⊗ₜ b⟧ to ⟦1 ⊗ₜ a⟧ ⊗ₜ b for all a : A, and b : B.

Equations

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

theorem Rep.coinvariantsTensorIndInv_mk_tmul_indMk {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Rep k G} {B : Rep k H} (x : ↑A.V) (y : ↑B.V) : (CategoryTheory.ConcreteCategory.hom (coinvariantsTensorIndInv φ A B)) ((Representation.Coinvariants.mk (A.ρ.tprod (ρ ((Action.res (ModuleCat k) φ).obj B)))) (x ⊗ₜ[k] y)) = (((ind φ A).coinvariantsTensorMk B) ((Representation.IndV.mk φ A.ρ 1) x)) y

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

Given a group hom φ : G →* H, A : Rep k G and B : Rep k H, this is the k-linear isomorphism (Ind(φ)(A) ⊗ B))_H ⟶ (A ⊗ Res(φ)(B))_G sending ⟦h ⊗ₜ a⟧ ⊗ₜ b to ⟦a ⊗ ρ(h)(b)⟧ for all h : H, a : A, and b : B.

Equations

• Rep.coinvariantsTensorIndIso φ A B = { hom := Rep.coinvariantsTensorIndHom φ A B, inv := Rep.coinvariantsTensorIndInv φ A B, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem Rep.coinvariantsTensorIndIso_inv {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) (B : Rep k H) : (coinvariantsTensorIndIso φ A B).inv = coinvariantsTensorIndInv φ A B

@[simp]

theorem Rep.coinvariantsTensorIndIso_hom {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) (B : Rep k H) : (coinvariantsTensorIndIso φ A B).hom = coinvariantsTensorIndHom φ A B

noncomputable def Rep.coinvariantsTensorIndNatIso {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) : (coinvariantsTensor k H).obj (ind φ A) ≅ (Action.res (ModuleCat k) φ).comp ((coinvariantsTensor k G).obj A)

Given a group hom φ : G →* H and A : Rep k G, the functor Rep k H ⥤ ModuleCat k sending B ↦ (Ind(φ)(A) ⊗ B))_H is naturally isomorphic to the one sending B ↦ (A ⊗ Res(φ)(B))_G.

Equations

• Rep.coinvariantsTensorIndNatIso φ A = CategoryTheory.NatIso.ofComponents (fun (B : Rep k H) => Rep.coinvariantsTensorIndIso φ A B) ⋯

@[simp]

theorem Rep.coinvariantsTensorIndNatIso_inv_app {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) (X : Rep k H) : (coinvariantsTensorIndNatIso φ A).inv.app X = coinvariantsTensorIndInv φ A X

@[simp]

theorem Rep.coinvariantsTensorIndNatIso_hom_app {k G H : Type u} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep k G) (X : Rep k H) : (coinvariantsTensorIndNatIso φ A).hom.app X = coinvariantsTensorIndHom φ A X