The transfer on first homology is the Verlagerung

Let S be a finite-index subgroup of a group G and A a trivial representation over a commutative ring k. With trivial coefficients, first group homology is the abelianization tensored with the coefficients, H₁(G, A) ≃ Gᵃᵇ ⊗ A (Mathlib's groupHomology.H1AddEquivOfIsTrivial). This file proves that, under these identifications, the homological transfer H₁(G, A) ⟶ H₁(S, A) of TauCeti.groupHomology.transfer is the group-theoretic transfer (Verlagerung) Gᵃᵇ → Sᵃᵇ of Mathlib's MonoidHom.transfer, tensored with A.

This is the homological form of the classical fact that the transfer in degree one is the Verlagerung. Through the comparison of negative Tate degrees with group homology it identifies restriction in Tate degree -2 with the Verlagerung (TauCeti.TateCohomology.HNegTwoAddEquivTensorOfIsTrivial_HNegTwoRes), which is the form in which restriction enters the reciprocity map of class field theory.

Main results

• TauCeti.groupHomology.transfer_mkH1OfIsTrivial: the transfer sends the class of g ⊗ a to the class of V(g) ⊗ a, where V : Gᵃᵇ → Sᵃᵇ is the Verlagerung.
• TauCeti.groupHomology.H1AddEquivOfIsTrivial_transfer: the same statement for every class, through H₁(G, A) ≃ Gᵃᵇ ⊗ A and H₁(S, A) ≃ Sᵃᵇ ⊗ A.

References

• K. S. Brown, Cohomology of Groups, Chapter III, §9.
• J.-P. Serre, Local Fields, Chapter VII, §8.
• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §4.

@[simp]

theorem TauCeti.groupHomology.transfer_mkH1OfIsTrivial {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.FiniteIndex] (A : Rep.{u, u, u} k G) [A.IsTrivial] (x : Additive (Abelianization G)) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (transfer A S 1)) (((groupHomology.mkH1OfIsTrivial A) x) a) = ((groupHomology.mkH1OfIsTrivial (Rep.res S.subtype A)) ((MonoidHom.toAdditive (Abelianization.lift Abelianization.of.transfer)) x)) a

The transfer on H₁ with trivial coefficients is the Verlagerung. For a subgroup S of a group G, a finite-index subgroup S, and trivial coefficients A, the transfer H₁(G, A) ⟶ H₁(S, A) sends the class of x ⊗ a to the class of V x ⊗ a, where V : Gᵃᵇ → Sᵃᵇ is the group-theoretic transfer MonoidHom.transfer of Abelianization.of : S →* Sᵃᵇ, descended to Gᵃᵇ.

@[simp]

theorem TauCeti.groupHomology.H1AddEquivOfIsTrivial_transfer {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.FiniteIndex] (A : Rep.{u, u, u} k G) [A.IsTrivial] (x : ↑(groupHomology.H1 A)) : (groupHomology.H1AddEquivOfIsTrivial (Rep.res S.subtype A)) ((CategoryTheory.ConcreteCategory.hom (transfer A S 1)) x) = (LinearMap.rTensor (↑A) (MonoidHom.toAdditive (Abelianization.lift Abelianization.of.transfer)).toIntLinearMap) ((groupHomology.H1AddEquivOfIsTrivial A) x)

The transfer on H₁ with trivial coefficients is the Verlagerung, read through the identifications H₁(G, A) ≃ Gᵃᵇ ⊗ A and H₁(S, A) ≃ Sᵃᵇ ⊗ A: the transfer becomes V ⊗ A, for V : Gᵃᵇ → Sᵃᵇ the group-theoretic transfer.