Low-degree functoriality for finite normal layers

The Artin map is obtained by reading Tate's isomorphism between degrees -2 and 0 through the layer's low-degree identifications; the degree -2 one carries the sign normalization required by the character formula. This file records how the degree -2 identification behaves under a restriction of finite normal layers. Restriction in degree -2 is group-theoretic transfer, while corestriction is induced by inclusion of Galois groups.

These formulas identify the change-of-group legs in the Artin--Tate squares comparing the Artin maps of two layers: inclusion of ground levels against transfer, and the norm against inclusion of Galois groups.

Main results

• LayerRestriction.tateHMinusTwoEquivAbelianization_trivialTateRes: degree -2 restriction is the transfer on abelianized Galois groups.
• LayerRestriction.tateHMinusTwoEquivAbelianization_trivialTateCor: degree -2 corestriction is the inclusion on abelianized Galois groups.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, Section 4.
• J.-P. Serre, Local Fields, Chapter XI, Section 3.

theorem TauCeti.ClassFieldTheory.LayerRestriction.tateHMinusTwoEquivAbelianization_trivialTateRes {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (x : ↑(big.TrivialTateH (-2))) : small.tateHMinusTwoEquivAbelianization ((CategoryTheory.ConcreteCategory.hom (T.trivialTateRes (-2))) x) = T.transferHom (big.tateHMinusTwoEquivAbelianization x)

Restriction in Tate degree -2, read through the low-degree identifications of two layers, is group-theoretic transfer on their abelianized Galois groups.

theorem TauCeti.ClassFieldTheory.LayerRestriction.tateHMinusTwoEquivAbelianization_trivialTateCor {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (x : ↑(small.TrivialTateH (-2))) : big.tateHMinusTwoEquivAbelianization ((CategoryTheory.ConcreteCategory.hom (T.trivialTateCor (-2))) x) = T.inclusionHom (small.tateHMinusTwoEquivAbelianization x)

Corestriction in Tate degree -2, read through the low-degree identifications of two layers, is the map on abelianizations induced by inclusion of their Galois groups.