(Co)induced representations of a finite index subgroup

Given a commutative ring k, a finite index subgroup S ≤ G, and a k-linear S-representation A, this file defines an isomorphism $Ind_S^G(A) ≅ Coind_S^G(A)$. Given g : G and a : A, the forward map sends ⟦g ⊗ₜ[k] a⟧ to the function G → Asupported at sg by ρ(s)(a) for s : S and which is 0 elsewhere. Meanwhile, the inverse sends f : G → A to ∑ᵢ ⟦gᵢ ⊗ₜ[k] f(gᵢ)⟧ for 1 ≤ i ≤ n, where g₁, ..., gₙ is a set of right coset representatives of S.

Main definitions

• Rep.indCoindIso A: An isomorphism Ind_S^G(A) ≅ Coind_S^G(A) for a finite index subgroup S ≤ G and a k-linear S-representation A.
• Rep.indCoindNatIso k S: A natural isomorphism between the functors Ind_S^G and Coind_S^G.

TODO

• Add Shapiro's lemma, using this isomorphism.

noncomputable def Rep.indToCoindAux {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep k ↥S) (g : G) : ↑A.V →ₗ[k] G → ↑A.V

Let S ≤ G be a subgroup and (A, ρ) a k-linear S-representation. Then given g : G and a : A, this is the function G → A sending sg to ρ(s)(a) for all s : S and everything else to 0.

Equations

• A.indToCoindAux g = LinearMap.pi fun (g₁ : G) => if h : (QuotientGroup.rightRel S) g₁ g then A.ρ ⟨g₁ * g⁻¹, ⋯⟩ else 0

@[simp]

theorem Rep.indToCoindAux_self {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] {A : Rep k ↥S} (g : G) (a : ↑A.V) : (A.indToCoindAux g) a g = a

theorem Rep.indToCoindAux_of_not_rel {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] {A : Rep k ↥S} (g g₁ : G) (a : ↑A.V) (h : ¬(QuotientGroup.rightRel S) g₁ g) : (A.indToCoindAux g) a g₁ = 0

@[simp]

theorem Rep.indToCoindAux_mul_snd {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] {A : Rep k ↥S} (g g₁ : G) (a : ↑A.V) (s : ↥S) : (A.indToCoindAux g) a (↑s * g₁) = (A.ρ s) ((A.indToCoindAux g) a g₁)

@[simp]

theorem Rep.indToCoindAux_mul_fst {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] {A : Rep k ↥S} (g₁ g₂ : G) (a : ↑A.V) (s : ↥S) : (A.indToCoindAux (↑s * g₁)) ((A.ρ s) a) g₂ = (A.indToCoindAux g₁) a g₂

@[simp]

theorem Rep.indToCoindAux_snd_mul_inv {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] {A : Rep k ↥S} (g₁ g₂ g₃ : G) (a : ↑A.V) : (A.indToCoindAux g₁) a (g₂ * g₃⁻¹) = (A.indToCoindAux (g₁ * g₃)) a g₂

@[simp]

theorem Rep.indToCoindAux_fst_mul_inv {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] {A : Rep k ↥S} (g₁ g₂ g₃ : G) (a : ↑A.V) : (A.indToCoindAux (g₁ * g₂⁻¹)) a g₃ = (A.indToCoindAux g₁) a (g₃ * g₂)

theorem Rep.indToCoindAux_comm {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] {A B : Rep k ↥S} (f : A ⟶ B) (g₁ g₂ : G) (a : ↑A.V) : (B.indToCoindAux g₁) ((CategoryTheory.ConcreteCategory.hom f.hom) a) g₂ = (CategoryTheory.ConcreteCategory.hom f.hom) ((A.indToCoindAux g₁) a g₂)

@[reducible, inline]

noncomputable abbrev Rep.indToCoind {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep k ↥S) : ↑(ind S.subtype A).V →ₗ[k] ↑(coind S.subtype A).V

Let S ≤ G be a subgroup and A a k-linear S-representation. This is the k-linear map Ind_S^G(A) →ₗ[k] Coind_S^G(A) sending (⟦g ⊗ₜ[k] a⟧, sg) ↦ ρ(s)(a).

Equations

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

noncomputable def Rep.coindToInd {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} (A : Rep k ↥S) [Fintype (G ⧸ S)] : ↑(coind S.subtype A).V →ₗ[k] ↑(ind S.subtype A).V

Let S ≤ G be a finite index subgroup, g₁, ..., gₙ a set of right coset representatives of S, and A a k-linear S-representation. This is the k-linear map Coind_S^G(A) →ₗ[k] Ind_S^G(A) sending f : G → A to ∑ᵢ ⟦gᵢ ⊗ₜ[k] f(gᵢ)⟧ for 1 ≤ i ≤ n.

Equations

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

@[simp]

theorem Rep.coindToInd_apply {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} (A : Rep k ↥S) [Fintype (G ⧸ S)] (f : ↑(coind S.subtype A).V) : A.coindToInd f = ∑ g : Quotient (QuotientGroup.rightRel S), g.liftOn (fun (g : G) => (Representation.IndV.mk S.subtype A.ρ g) (↑f g)) ⋯

theorem Rep.coindToInd_of_support_subset_orbit {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} {A : Rep k ↥S} [Fintype (G ⧸ S)] (g : G) (f : ↑(coind S.subtype A).V) (hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g) : A.coindToInd f = (Representation.IndV.mk S.subtype A.ρ g) (↑f g)

noncomputable def Rep.indCoindIso {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep k ↥S) [Fintype (G ⧸ S)] : ind S.subtype A ≅ coind S.subtype A

Let S ≤ G be a finite index subgroup, g₁, ..., gₙ a set of right coset representatives of S, and A a k-linear S-representation. This is an isomorphism Ind_S^G(A) ≅ Coind_S^G(A). The forward map sends (⟦g ⊗ₜ[k] a⟧, sg) ↦ ρ(s)(a), and the inverse sends f : G → A to ∑ᵢ ⟦gᵢ ⊗ₜ[k] f(gᵢ)⟧ for 1 ≤ i ≤ n.

Equations

• A.indCoindIso = Action.mkIso { hom := ModuleCat.ofHom A.indToCoind, inv := ModuleCat.ofHom A.coindToInd, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯

@[simp]

theorem Rep.indCoindIso_hom_hom_hom {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep k ↥S) [Fintype (G ⧸ S)] : ModuleCat.Hom.hom A.indCoindIso.hom.hom = A.indToCoind

@[simp]

theorem Rep.indCoindIso_inv_hom_hom {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep k ↥S) [Fintype (G ⧸ S)] : ModuleCat.Hom.hom A.indCoindIso.inv.hom = A.coindToInd

noncomputable def Rep.indCoindNatIso (k : Type u) {G : Type u} [CommRing k] [Group G] (S : Subgroup G) [DecidableRel ⇑(QuotientGroup.rightRel S)] [Fintype (G ⧸ S)] : indFunctor k S.subtype ≅ coindFunctor k S.subtype

Given a finite index subgroup S ≤ G, this is a natural isomorphism between the Ind_S^G and Coind_G^S functors Rep k S ⥤ Rep k G.

Equations

• Rep.indCoindNatIso k S = CategoryTheory.NatIso.ofComponents (fun (x : Rep k ↥S) => x.indCoindIso) ⋯

@[simp]

theorem Rep.indCoindNatIso_inv_app (k : Type u) {G : Type u} [CommRing k] [Group G] (S : Subgroup G) [DecidableRel ⇑(QuotientGroup.rightRel S)] [Fintype (G ⧸ S)] (X : Rep k ↥S) : (indCoindNatIso k S).inv.app X = X.indCoindIso.inv

@[simp]

theorem Rep.indCoindNatIso_hom_app (k : Type u) {G : Type u} [CommRing k] [Group G] (S : Subgroup G) [DecidableRel ⇑(QuotientGroup.rightRel S)] [Fintype (G ⧸ S)] (X : Rep k ↥S) : (indCoindNatIso k S).hom.app X = X.indCoindIso.hom

noncomputable def Rep.resIndAdjunction (k : Type u) {G : Type u} [CommRing k] [Group G] (S : Subgroup G) [DecidableRel ⇑(QuotientGroup.rightRel S)] [Fintype (G ⧸ S)] : Action.res (ModuleCat k) S.subtype ⊣ indFunctor k S.subtype

Given a finite index subgroup S ≤ G, Ind_S^G is right adjoint to the restriction functor Res k G ⥤ Res k S, since it is naturally isomorphic to Coind_S^G.

Equations

• Rep.resIndAdjunction k S = (Rep.resCoindAdjunction k S.subtype).ofNatIsoRight (Rep.indCoindNatIso k S).symm

instance Rep.instIsRightAdjointSubtypeMemSubgroupIndFunctorSubtype (k : Type u) {G : Type u} [CommRing k] [Group G] (S : Subgroup G) [DecidableRel ⇑(QuotientGroup.rightRel S)] [Fintype (G ⧸ S)] : (indFunctor k S.subtype).IsRightAdjoint

@[simp]

theorem Rep.resIndAdjunction_counit_app {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep k ↥S) [Fintype (G ⧸ S)] : (resIndAdjunction k S).counit.app A = CategoryTheory.CategoryStruct.comp ((Action.res (ModuleCat k) S.subtype).map A.indCoindIso.hom) ((resCoindAdjunction k S.subtype).counit.app A)

@[simp]

theorem Rep.resIndAdjunction_unit_app {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] [Fintype (G ⧸ S)] (B : Rep k G) : (resIndAdjunction k S).unit.app B = CategoryTheory.CategoryStruct.comp ((resCoindAdjunction k S.subtype).unit.app B) (indCoindIso ((Action.res (ModuleCat k) S.subtype).obj B)).inv

theorem Rep.resIndAdjunction_homEquiv_apply {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep k ↥S) [Fintype (G ⧸ S)] {B : Rep k G} (f : (Action.res (ModuleCat k) S.subtype).obj B ⟶ A) : ((resIndAdjunction k S).homEquiv B A) f = CategoryTheory.CategoryStruct.comp ((resCoindHomEquiv S.subtype B A) f) A.indCoindIso.inv

theorem Rep.resIndAdjunction_homEquiv_symm_apply {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep k ↥S) [Fintype (G ⧸ S)] {B : Rep k G} (f : B ⟶ (indFunctor k S.subtype).obj A) : ((resIndAdjunction k S).homEquiv B A).symm f = (resCoindHomEquiv S.subtype B A).symm (CategoryTheory.CategoryStruct.comp f A.indCoindIso.hom)

noncomputable def Rep.coindResAdjunction (k : Type u) {G : Type u} [CommRing k] [Group G] (S : Subgroup G) [DecidableRel ⇑(QuotientGroup.rightRel S)] [Fintype (G ⧸ S)] : coindFunctor k S.subtype ⊣ Action.res (ModuleCat k) S.subtype

Given a finite index subgroup S ≤ G, Coind_S^G is left adjoint to the restriction functor Res k G ⥤ Res k S, since it is naturally isomorphic to Ind_S^G.

Equations

• Rep.coindResAdjunction k S = (Rep.indResAdjunction k S.subtype).ofNatIsoLeft (Rep.indCoindNatIso k S)

instance Rep.instIsLeftAdjointSubtypeMemSubgroupCoindFunctorSubtype {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] [Fintype (G ⧸ S)] : (coindFunctor k S.subtype).IsLeftAdjoint

@[simp]

theorem Rep.coindResAdjunction_counit_app {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] [Fintype (G ⧸ S)] (B : Rep k G) : (coindResAdjunction k S).counit.app B = CategoryTheory.CategoryStruct.comp (indCoindIso ((Action.res (ModuleCat k) S.subtype).obj B)).inv ((indResAdjunction k S.subtype).counit.app B)

@[simp]

theorem Rep.coindResAdjunction_unit_app {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep k ↥S) [Fintype (G ⧸ S)] : (coindResAdjunction k S).unit.app A = CategoryTheory.CategoryStruct.comp ((indResAdjunction k S.subtype).unit.app A) ((Action.res (ModuleCat k) S.subtype).map A.indCoindIso.hom)

theorem Rep.coindResAdjunction_homEquiv_apply {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep k ↥S) [Fintype (G ⧸ S)] {B : Rep k G} (f : coind S.subtype A ⟶ B) : ((coindResAdjunction k S).homEquiv A B) f = (indResHomEquiv S.subtype A B) (CategoryTheory.CategoryStruct.comp A.indCoindIso.hom f)

theorem Rep.coindResAdjunction_homEquiv_symm_apply {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep k ↥S) [Fintype (G ⧸ S)] {B : Rep k G} (f : A ⟶ (Action.res (ModuleCat k) S.subtype).obj B) : ((coindResAdjunction k S).homEquiv A B).symm f = CategoryTheory.CategoryStruct.comp A.indCoindIso.inv ((indResHomEquiv S.subtype A B).symm f)