Restricting to a finite-index subgroup and coming back

Let S be a subgroup of finite index in a group G. Coinduction from S to G is right adjoint to restriction (Rep.resCoindAdjunction), and, because the index is finite, also left adjoint to it (Rep.coindResAdjunction). For a G-representation A this gives two maps

A ⟶ Coind_S^G(Res_S A) ⟶ A,

the unit of the first adjunction, a ↦ (g ↦ g • a), and the counit of the second, the trace f ↦ ∑ g⁻¹ • f g over representatives g of the right cosets of S. Their composite is multiplication by the index [G : S]. This is the identity behind the normalization cor ∘ res = [G : S] of group-cohomological corestriction.

Because the index is finite, induction Ind_S^G is identified with coinduction (Rep.indCoindIso), and the same identity holds for the unit A ⟶ Ind_S^G(Res_S A) of restriction–induction followed by the counit Ind_S^G(Res_S A) ⟶ A of induction–restriction. That form is behind the normalization of the transfer in group homology.

Main results

• Subgroup.coindResAdjunction_counit_app_hom_apply: the trace sums g⁻¹ • f g over the chosen representatives g of the right cosets of S.
• TauCeti.Rep.resCoindAdjunction_unit_app_comp_coindResAdjunction_counit_app: the composite of the unit and the trace is [G : S] • 𝟙 A.
• TauCeti.Rep.resIndAdjunction_unit_app_comp_indResAdjunction_counit_app: the same identity with coinduction replaced by induction, through Mathlib's identification Rep.indCoindIso.
• Rep.coinvariantsMk_coindToInd_unit: in the G-coinvariants of Ind_S^G(Res_S A), the unit A ⟶ Ind_S^G(Res_S A) sends a to the class of 1 ⊗ ∑_{q ∈ G ⧸ S} q⁻¹ • a, the relative transfer Representation.relTransfer.

References

• K. S. Brown, Cohomology of Groups, Graduate Texts in Mathematics 87, Springer (1982), Chapter III, §9.

theorem Subgroup.coindResAdjunction_counit_app_hom_apply {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.FiniteIndex] (A : Rep.{u, u, u} k G) (f : ↑(Rep.coind.{u, u, u, u} S.subtype (Rep.res S.subtype A))) : (Rep.Hom.hom ((Rep.coindResAdjunction k S).counit.app A)) f = ∑ q : Quotient (QuotientGroup.rightRel S), (A.ρ q.out⁻¹) (↑f q.out)

The trace as a sum over right cosets. For a finite-index subgroup S ≤ G, the counit Coind_S^G(Res_S A) ⟶ A of coinduction–restriction sends f to ∑ g⁻¹ • f g, the sum over the representatives g = q.out of the right cosets q = S g.

theorem TauCeti.indToCoind_mk {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] {A : Rep.{w, u, v} k ↥S} (g : G) (a : ↑A) : ↑(A.indToCoind ((Representation.IndV.mk S.subtype A.ρ g) a)) = (A.indToCoindAux g) a

Mathlib's induction-to-coinduction map sends a tensor generator to the function supported on its right coset, with value a at g.

theorem TauCeti.Rep.resCoindAdjunction_unit_app_comp_coindResAdjunction_counit_app {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.FiniteIndex] (A : Rep.{u, u, u} k G) : CategoryTheory.CategoryStruct.comp ((Rep.resCoindAdjunction k S.subtype).unit.app A) ((Rep.coindResAdjunction k S).counit.app A) = S.index • CategoryTheory.CategoryStruct.id A

Unit followed by trace is the index. For a finite-index subgroup S ≤ G, the unit A ⟶ Coind_S^G(Res_S A) of restriction–coinduction followed by the counit Coind_S^G(Res_S A) ⟶ A of coinduction–restriction is multiplication by [G : S].

theorem TauCeti.Rep.resIndAdjunction_unit_app_comp_indResAdjunction_counit_app {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.FiniteIndex] (A : Rep.{u, u, u} k G) : CategoryTheory.CategoryStruct.comp ((Rep.resIndAdjunction k S).unit.app A) ((Rep.indResAdjunction k S.subtype).counit.app A) = S.index • CategoryTheory.CategoryStruct.id A

Unit followed by counit is the index, for induction. For a finite-index subgroup S ≤ G, the unit A ⟶ Ind_S^G(Res_S A) of restriction–induction followed by the counit Ind_S^G(Res_S A) ⟶ A of induction–restriction is multiplication by [G : S].

theorem TauCeti.Rep.resIndAdjunction_unit_app_comp_indResAdjunction_counit_app_assoc {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.FiniteIndex] (A : Rep.{u, u, u} k G) {Z : Rep.{u, u, u} k G} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp ((Rep.resIndAdjunction k S).unit.app A) (CategoryTheory.CategoryStruct.comp ((Rep.indResAdjunction k S.subtype).counit.app A) h) = CategoryTheory.CategoryStruct.comp (S.index • CategoryTheory.CategoryStruct.id A) h

Unit followed by counit is the index, for induction. For a finite-index subgroup S ≤ G, the unit A ⟶ Ind_S^G(Res_S A) of restriction–induction followed by the counit Ind_S^G(Res_S A) ⟶ A of induction–restriction is multiplication by [G : S].

The unit of restriction–induction in coinvariants

theorem Rep.coinvariantsMk_coindToInd_unit {k G : Type u} [CommRing k] [Group G] (M : Rep.{max u u_1, u, u} k G) (S : Subgroup G) [S.FiniteIndex] (m : ↑M) : (Representation.Coinvariants.mk (Representation.ind S.subtype (res S.subtype M).ρ)) ((res S.subtype M).coindToInd ((Hom.hom ((resCoindAdjunction k S.subtype).unit.app M)) m)) = (Representation.Coinvariants.mk (Representation.ind S.subtype (res S.subtype M).ρ)) ((Representation.IndV.mk S.subtype (res S.subtype M).ρ 1) ((M.ρ.relTransfer S) m))

The unit of Res ⊣ Ind, read in coinvariants, is the relative transfer. For a finite-index subgroup S ≤ G, the unit M ⟶ Ind_S^G Res_S M sends m to ∑ᵢ ⟦gᵢ ⊗ gᵢ • m⟧ over right coset representatives gᵢ; in the G-coinvariants of Ind_S^G Res_S M this is the class of ⟦1 ⊗ ∑_{q ∈ G ⧸ S} q⁻¹ • m⟧. The right coset S g is matched with the left coset g⁻¹ S, and each summand depends only on its coset.