Maps between abelianized Galois groups of finite normal layers

The functoriality of the Artin map compares operations on formation levels with three canonical homomorphisms between the abelianizations of finite-layer Galois groups, and with the equivalence induced directly by conjugation. This file constructs the homomorphisms and proves coherence laws for the conjugation equivalence obtained from Mathlib's MulEquiv.abelianizationCongr.

For a restriction of layers K/E inside K/F, the inclusion

Gal(K/E) ↪ Gal(K/F)

induces LayerRestriction.inclusionHom on abelianizations. In the other direction, LayerRestriction.transferHom is the group-theoretic transfer (Verlagerung). It is formed by identifying Gal(K/E) with the range of the inclusion, applying Mathlib's MonoidHom.transfer, and then using the universal property of the abelianization. The index of that range is the relative degree [E : F]. Like the inclusion, the transfer is functorial along a tower of restrictions, because the group-theoretic transfer is transitive (MonoidHom.transfer_transfer).

For a refinement L/F of K/F, the quotient map

Gal(L/F) → Gal(K/F)

induces LayerRefinement.quotientHom. The inclusion and quotient maps inherit identity and tower laws from Abelianization.map; these laws make the maps usable without unfolding their bodies. Conjugation of a layer similarly induces an equivalence on abelianizations from NormalLayer.conjugateGalEquiv and Mathlib's MulEquiv.abelianizationCongr.

Main definitions and results

• TauCeti.ClassFieldTheory.LayerRestriction.inclusionHom: the map on abelianizations induced by inclusion of Galois groups.
• TauCeti.ClassFieldTheory.LayerRestriction.transferHom: group-theoretic transfer between the same abelianizations, in the opposite direction.
• TauCeti.ClassFieldTheory.LayerRestriction.transferHom_trans: the transfer is functorial along a tower of restrictions.
• TauCeti.ClassFieldTheory.LayerRefinement.quotientHom: the map on abelianizations induced by a quotient of Galois groups.
• NormalLayer.conjugateGalEquiv_abelianizationCongr_one: conjugation by one is the identity on abelianized Galois groups.
• NormalLayer.conjugateGalEquiv_abelianizationCongr_trans: conjugation on abelianized Galois groups composes.

References

• E. Artin and J. Tate, Class Field Theory, Chapter IV, §6 and Chapter XIV, §4.
• K. S. Brown, Cohomology of Groups, Chapter III, §9.

theorem TauCeti.ClassFieldTheory.LayerRestriction.index_range_galHom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) : T.galHom.range.index = T.relativeDegree

The index of the image of Gal(K/E) in Gal(K/F) is the relative degree [E : F].

def TauCeti.ClassFieldTheory.LayerRestriction.inclusionHom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) : Additive (Abelianization small.Gal) →+ Additive (Abelianization big.Gal)

The map (U'/V)^ab → (U/V)^ab induced by the inclusion U'/V → U/V attached to a restriction of layers. The additive type tags match the additive convention of Tate cohomology.

theorem TauCeti.ClassFieldTheory.LayerRestriction.inclusionHom_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (x : Additive (Abelianization small.Gal)) : T.inclusionHom x = (MonoidHom.toAdditive (Abelianization.map T.galHom)) x

Inclusion on abelianized Galois groups is induced by the layer's Galois-group homomorphism.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.inclusionHom_of {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (x : small.Gal) : T.inclusionHom (Additive.ofMul (Abelianization.of x)) = Additive.ofMul (Abelianization.of (T.galHom x))

The inclusion map sends the abelianization class of x to the class of its image in the larger Galois group.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.inclusionHom_self {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {L : NormalLayer G} (T : LayerRestriction L L) : T.inclusionHom = AddMonoidHom.id (Additive (Abelianization L.Gal))

Inclusion on abelianized Galois groups is the identity for the trivial restriction.

theorem TauCeti.ClassFieldTheory.LayerRestriction.inclusionHom_trans {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {a b c : NormalLayer G} (T : LayerRestriction a b) (T' : LayerRestriction b c) : ⋯.inclusionHom = T'.inclusionHom.comp T.inclusionHom

Inclusion on abelianized Galois groups is functorial along a tower of restrictions.

noncomputable def TauCeti.ClassFieldTheory.LayerRestriction.transferHom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) : Additive (Abelianization big.Gal) →+ Additive (Abelianization small.Gal)

The group-theoretic transfer (U/V)^ab → (U'/V)^ab attached to a restriction of layers. Mathlib's transfer first gives a homomorphism from U/V to the abelianization of U'/V; the universal property of the source abelianization then supplies the displayed map.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRestriction.transferHom_of {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) (x : big.Gal) : T.transferHom (Additive.ofMul (Abelianization.of x)) = Additive.ofMul ((Abelianization.of.comp (MonoidHom.ofInjective ⋯).symm.toMonoidHom).transfer x)

On the class of an element, transferHom is Mathlib's group-theoretic transfer to the image of the smaller Galois group, transported back along the equivalence induced by galHom.

theorem TauCeti.ClassFieldTheory.LayerRestriction.transferHom_eq_map_comp_lift_transfer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {small big : NormalLayer G} (T : LayerRestriction small big) : T.transferHom = (MonoidHom.toAdditive (Abelianization.map ↑(MonoidHom.ofInjective ⋯).symm)).comp (MonoidHom.toAdditive (Abelianization.lift Abelianization.of.transfer))

The transfer between the Galois groups of two layers is the transfer to the image subgroup, followed by transport back along the equivalence from the smaller Galois group to that image.

theorem TauCeti.ClassFieldTheory.LayerRestriction.transferHom_trans {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {a b c : NormalLayer G} (T : LayerRestriction a b) (T' : LayerRestriction b c) : ⋯.transferHom = T.transferHom.comp T'.transferHom

Transfer on abelianized Galois groups is functorial along a tower of restrictions: for F ⊆ E ⊆ E' ⊆ K, the transfer Gal(K/F)^ab → Gal(K/E')^ab is the transfer Gal(K/F)^ab → Gal(K/E)^ab followed by the transfer Gal(K/E)^ab → Gal(K/E')^ab.

def TauCeti.ClassFieldTheory.LayerRefinement.quotientHom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) : Additive (Abelianization new.Gal) →+ Additive (Abelianization old.Gal)

The quotient map (U/V')^ab → (U/V)^ab induced by the quotient homomorphism U/V' → U/V attached to a refinement of layers.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRefinement.quotientHom_of {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) (x : new.Gal) : T.quotientHom (Additive.ofMul (Abelianization.of x)) = Additive.ofMul (Abelianization.of (T.galHom x))

The quotient map sends the abelianization class of x to the class of its image in the quotient Galois group.

theorem TauCeti.ClassFieldTheory.LayerRefinement.quotientHom_surjective {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {old new : NormalLayer G} (T : LayerRefinement old new) : Function.Surjective ⇑T.quotientHom

The quotient map on abelianized Galois groups is surjective.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRefinement.quotientHom_self {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {L : NormalLayer G} (T : LayerRefinement L L) : T.quotientHom = AddMonoidHom.id (Additive (Abelianization L.Gal))

The quotient map on abelianized Galois groups is the identity for the trivial refinement.

theorem TauCeti.ClassFieldTheory.LayerRefinement.quotientHom_trans {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {a b c : NormalLayer G} (T : LayerRefinement a b) (T' : LayerRefinement b c) : ⋯.quotientHom = T.quotientHom.comp T'.quotientHom

Quotient maps on abelianized Galois groups are functorial along a tower of refinements.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateGalEquiv_abelianizationCongr_one {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) : (MulEquiv.toAdditive (L.conjugateGalEquiv 1).abelianizationCongr).trans (MulEquiv.toAdditive (MulEquiv.cast ⋯).abelianizationCongr) = AddEquiv.refl (Additive (Abelianization L.Gal))

Conjugation by 1 is the identity on abelianized Galois groups, after transporting along conjugate_one.

theorem TauCeti.ClassFieldTheory.NormalLayer.conjugateGalEquiv_abelianizationCongr_trans {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (L : NormalLayer G) (g h : G) : (MulEquiv.toAdditive (L.conjugateGalEquiv h).abelianizationCongr).trans (MulEquiv.toAdditive ((L.conjugate h).conjugateGalEquiv g).abelianizationCongr) = (MulEquiv.toAdditive (L.conjugateGalEquiv (g * h)).abelianizationCongr).trans (MulEquiv.toAdditive (MulEquiv.cast ⋯).abelianizationCongr)

Conjugation on abelianized Galois groups composes: conjugating by h and then by g is conjugating by g * h, up to transport along conjugate_conjugate.