Abelian layers of a formation

An open normal subgroup V of a topological group has abelian quotient precisely when it contains the closure of the commutator subgroup. This file packages that condition as IsAbelianClassFieldLayer V and identifies it with commutativity of G ⧸ V.

Every open normal subgroup also has a canonical maximal abelian sublayer. In subgroup language it is

V ⊔ closure (commutator G),

the least abelian-layer subgroup containing V. When G is the relevant profinite Galois group, the corresponding fixed field is therefore the largest abelian subextension of the field cut out by V. This construction is the group-theoretic input to norm limitation: abstract reciprocity later shows that a layer and this maximal abelian sublayer have the same norm subgroup.

Under the profinite hypotheses used for finite normal layers, the final part of the file removes the algebraic abelianization from the quotient group. It supplies the canonical equivalence Abelianization (G ⧸ V) ≃* G ⧸ V used, when G is a Galois group, to state local and global class-field correspondences directly in terms of their abelian Galois groups.

Main definitions

• OpenNormalSubgroup.IsAbelianClassFieldLayer: the closed-commutator condition on an open normal subgroup.
• TauCeti.ClassFieldTheory.AbelianLayer: the subtype of open normal subgroups satisfying that condition.
• OpenNormalSubgroup.maximalAbelianLayer: the least abelian-layer subgroup above a given open normal subgroup.
• TauCeti.ClassFieldTheory.abelianizationGalEquiv: the canonical equivalence from the abelianization of an abelian layer's Galois group to that Galois group.

Main statements

• OpenNormalSubgroup.isAbelianClassFieldLayer_iff_isMulCommutative: the closed-commutator condition is equivalent to commutativity of G ⧸ V.
• OpenNormalSubgroup.le_maximalAbelianLayer and OpenNormalSubgroup.maximalAbelianLayer_le: the universal property of the maximal abelian sublayer.
• OpenNormalSubgroup.maximalAbelianLayer_eq_self_iff: the construction fixes exactly the abelian layers.
• OpenNormalSubgroup.subgroupGround_commutator: the preimage of the finite quotient's commutator is the maximal abelian sublayer subgroup.
• OpenNormalSubgroup.natCard_abelianization_gal_eq_degree_maximalAbelianLayer: the abelianized Galois group of a layer has the order of the Galois group of its maximal abelian sublayer.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §§4–5.
• J. Neukirch, Class Field Theory, Chapter III, §1.

Abelian layers

def OpenNormalSubgroup.IsAbelianClassFieldLayer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : OpenNormalSubgroup G) : Prop

An open normal subgroup cuts out an abelian class-field layer when it contains the topological closure of the commutator subgroup. The closure is essential: it is the kernel used by Mathlib's TopologicalAbelianization, and the unclosed commutator subgroup need not be closed in a profinite group.

@[reducible, inline]

abbrev TauCeti.ClassFieldTheory.AbelianLayer (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Type

Open normal subgroups whose quotient is abelian. For a profinite Galois group, these form the Galois-side carrier of class-field correspondences; subgroup inclusion becomes reverse inclusion on fixed fields.

theorem OpenNormalSubgroup.isAbelianClassFieldLayer_iff_isMulCommutative {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : OpenNormalSubgroup G) : V.IsAbelianClassFieldLayer ↔ IsMulCommutative (G ⧸ ↑V.toOpenSubgroup)

The closed-commutator condition on V is equivalent to commutativity of the quotient G ⧸ V.

theorem OpenNormalSubgroup.IsAbelianClassFieldLayer.mono {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {U V : OpenNormalSubgroup G} (hU : U.IsAbelianClassFieldLayer) (h : U ≤ V) : V.IsAbelianClassFieldLayer

A layer subgroup containing an abelian layer subgroup is abelian: a subextension of an abelian extension is abelian.

theorem OpenNormalSubgroup.IsAbelianClassFieldLayer.inf {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V W : OpenNormalSubgroup G} (hV : V.IsAbelianClassFieldLayer) (hW : W.IsAbelianClassFieldLayer) : (V ⊓ W).IsAbelianClassFieldLayer

The intersection of two abelian layer subgroups is abelian: the compositum of two abelian extensions is abelian.

The maximal abelian sublayer

def OpenNormalSubgroup.maximalAbelianLayer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : OpenNormalSubgroup G) : OpenNormalSubgroup G

The maximal abelian sublayer of V, represented on subgroups by V ⊔ closure (commutator G). It is the least abelian-layer subgroup containing V. When G is the relevant profinite Galois group, it cuts out the largest abelian subextension of the original fixed field.

@[simp]

theorem OpenNormalSubgroup.toSubgroup_maximalAbelianLayer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : OpenNormalSubgroup G) : ↑V.maximalAbelianLayer.toOpenSubgroup = ↑V.toOpenSubgroup ⊔ (commutator G).topologicalClosure

The subgroup underlying the maximal abelian sublayer of V is the join of V with the closure of the commutator subgroup of G.

theorem OpenNormalSubgroup.toSubgroup_maximalAbelianLayer_eq_commutator_sup {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : OpenNormalSubgroup G) : ↑V.maximalAbelianLayer.toOpenSubgroup = commutator G ⊔ ↑V.toOpenSubgroup

The closed commutator in the maximal abelian sublayer can be replaced by the algebraic commutator: the join with an open subgroup is already closed.

@[simp]

theorem OpenNormalSubgroup.mem_maximalAbelianLayer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V : OpenNormalSubgroup G} {x : G} : x ∈ V.maximalAbelianLayer ↔ x ∈ ↑V.toOpenSubgroup ⊔ (commutator G).topologicalClosure

An element lies in the maximal abelian sublayer of V exactly when it lies in the join of V with the closure of the commutator subgroup of G.

theorem OpenNormalSubgroup.le_maximalAbelianLayer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : OpenNormalSubgroup G) : V ≤ V.maximalAbelianLayer

Every layer subgroup lies in its maximal abelian sublayer subgroup.

@[simp]

theorem OpenNormalSubgroup.isAbelianClassFieldLayer_maximalAbelianLayer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : OpenNormalSubgroup G) : V.maximalAbelianLayer.IsAbelianClassFieldLayer

The maximal abelian sublayer is an abelian class-field layer.

theorem OpenNormalSubgroup.maximalAbelianLayer_le {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V W : OpenNormalSubgroup G} (hVW : V ≤ W) (hW : W.IsAbelianClassFieldLayer) : V.maximalAbelianLayer ≤ W

The universal property of the maximal abelian sublayer: it is the least abelian-layer subgroup containing V.

@[simp]

theorem OpenNormalSubgroup.maximalAbelianLayer_sup {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V W : OpenNormalSubgroup G) : (V ⊔ W).maximalAbelianLayer = V.maximalAbelianLayer ⊔ W.maximalAbelianLayer

The maximal abelian sublayer of a join is the join of the maximal abelian sublayers: the maximal abelian subextension of an intersection of two finite Galois extensions is the intersection of their maximal abelian subextensions.

@[simp]

theorem OpenNormalSubgroup.maximalAbelianLayer_eq_self_iff {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : OpenNormalSubgroup G) : V.maximalAbelianLayer = V ↔ V.IsAbelianClassFieldLayer

A layer is already abelian exactly when its maximal abelian sublayer is itself.

theorem OpenNormalSubgroup.subgroupGround_commutator {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (V : OpenNormalSubgroup G) : (TauCeti.ClassFieldTheory.NormalLayer.ofOpenNormal V).subgroupGround (commutator (TauCeti.ClassFieldTheory.NormalLayer.ofOpenNormal V).Gal) = ↑V.maximalAbelianLayer.toOpenSubgroup

The preimage of the commutator of a finite layer's Galois group cuts out its maximal abelian subextension. This identifies the ground subgroup used by transfer with the canonical maximal abelian sublayer.

Finite Galois groups of abelian layers

theorem TauCeti.ClassFieldTheory.isMulCommutative_gal_ofOpenNormal {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V : OpenNormalSubgroup G} (hV : V.IsAbelianClassFieldLayer) : IsMulCommutative (NormalLayer.ofOpenNormal V).Gal

The finite Galois group of an abelian open normal layer is commutative.

noncomputable def TauCeti.ClassFieldTheory.abelianizationGalEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V : OpenNormalSubgroup G} (hV : V.IsAbelianClassFieldLayer) : Abelianization (NormalLayer.ofOpenNormal V).Gal ≃* (NormalLayer.ofOpenNormal V).Gal

For an abelian layer, the canonical quotient map to its algebraic abelianization is an isomorphism. This equivalence removes the redundant abelianization from the target of the Artin equivalence.

@[simp]

theorem TauCeti.ClassFieldTheory.abelianizationGalEquiv_symm_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V : OpenNormalSubgroup G} (hV : V.IsAbelianClassFieldLayer) (x : (NormalLayer.ofOpenNormal V).Gal) : (abelianizationGalEquiv hV).symm x = Abelianization.of x

The inverse of abelianizationGalEquiv is the canonical abelianization map.

@[simp]

theorem TauCeti.ClassFieldTheory.abelianizationGalEquiv_of {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V : OpenNormalSubgroup G} (hV : V.IsAbelianClassFieldLayer) (x : (NormalLayer.ofOpenNormal V).Gal) : (abelianizationGalEquiv hV) (Abelianization.of x) = x

The abelianization equivalence sends the canonical class of an element back to that element.

theorem OpenNormalSubgroup.natCard_abelianization_gal_eq_degree_maximalAbelianLayer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (V : OpenNormalSubgroup G) : Nat.card (Abelianization (TauCeti.ClassFieldTheory.NormalLayer.ofOpenNormal V).Gal) = (TauCeti.ClassFieldTheory.NormalLayer.ofOpenNormal V.maximalAbelianLayer).degree

The abelianized Galois group of a layer has the order of the Galois group of its maximal abelian sublayer: (G ⧸ V)^ab has [G : V · closure [G, G]] elements. This is the counting input to norm limitation.