The absolute Artin map of a class formation

Let cf be a class formation on a formation F over a profinite group G, with ground level A^G. Every open normal subgroup V of G gives a finite normal layer V ◁ G, with Artin map cf.artinMap (NormalLayer.ofOpenNormal V) : A^G → (G/V)^ab. These maps are compatible with the quotient maps between the Galois groups of nested layers (ClassFormation.artinMap_quotient), so they pass to the inverse limit. The limit of the finite quotients (G/V)^ab is the topological abelianization G^ab = G ⧸ closure [G, G], which is again profinite. This gives the absolute Artin map

cf.absoluteArtinMap : A^G → G^ab.

The map is characterized by its finite restrictions. Write NormalLayer.abelianizationRestrict V : G^ab → (G/V)^ab for the projection. The composite of the absolute map with this projection is the finite Artin map of the layer V ◁ G (abelianizationRestrict_absoluteArtinMap), and no other homomorphism has this property (eq_absoluteArtinMap_of_forall_abelianizationRestrict). Every finite Artin map is surjective, so the absolute map has dense image (denseRange_absoluteArtinMap). It need not be surjective: for a local field the source is Kˣ and the target is the abelianized absolute Galois group. Since the kernel of each finite Artin map is the norm subgroup of its layer, the preimage of every open subgroup of G^ab is the norm subgroup of a layer (exists_absoluteArtinMap_mem_iff), and the kernel of the absolute map is the intersection of all norm subgroups (absoluteArtinMap_eq_zero_iff).

The construction runs over the open normal subgroups U of G^ab. Each of them is the image of the open normal subgroup V of G it pulls back to, and G^ab ⧸ U is the abelianized Galois group (G/V)^ab of the layer of V. The limit description of the profinite group G^ab (TauCeti.existsUnique_monoidHom_mk'_comp_eq) then assembles the finite Artin maps into a single homomorphism.

Main definitions

• TauCeti.ClassFieldTheory.NormalLayer.abelianizationRestrict: the projection G^ab → (G/V)^ab onto the abelianized Galois group of the layer of an open normal subgroup.
• TauCeti.ClassFieldTheory.ClassFormation.absoluteArtinMap: the absolute Artin map A^G → G^ab.

Main results

• TauCeti.ClassFieldTheory.ClassFormation.abelianizationRestrict_absoluteArtinMap: the finite restrictions of the absolute Artin map are the finite Artin maps.
• TauCeti.ClassFieldTheory.ClassFormation.eq_absoluteArtinMap_of_forall_abelianizationRestrict: the absolute Artin map is the unique homomorphism with these restrictions.
• TauCeti.ClassFieldTheory.NormalLayer.eq_of_forall_le_abelianizationRestrict_eq: elements of G^ab are determined by their projections to the layers below any fixed open normal subgroup.
• TauCeti.ClassFieldTheory.ClassFormation.denseRange_absoluteArtinMap: the absolute Artin map has dense image.
• TauCeti.ClassFieldTheory.ClassFormation.exists_absoluteArtinMap_mem_iff: the preimage of an open subgroup of G^ab under the absolute Artin map is the norm subgroup of a layer.
• TauCeti.ClassFieldTheory.ClassFormation.absoluteArtinMap_eq_zero_iff: the kernel of the absolute Artin map is the intersection of the norm subgroups of all layers.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV.
• J. Neukirch, Algebraic Number Theory, Chapter IV, §6.

The projections of the topological abelianization

def TauCeti.ClassFieldTheory.NormalLayer.abelianizationRestrict {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (V : OpenNormalSubgroup G) : Additive (TopologicalAbelianization G) →+ Additive (Abelianization (ofOpenNormal V).Gal)

The projection G^ab → (G/V)^ab from the topological abelianization of G onto the abelianized Galois group of the layer V ◁ G of an open normal subgroup V, written additively. It sends the class of g ∈ G to the class of g (abelianizationRestrict_mk). In Galois language, it restricts an automorphism of the maximal abelian extension to the maximal abelian subextension of the finite layer cut out by V.

@[simp]

theorem TauCeti.ClassFieldTheory.NormalLayer.abelianizationRestrict_mk {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (V : OpenNormalSubgroup G) (g : ↥(ofOpenNormal V).ground) : (abelianizationRestrict V) (Additive.ofMul ↑↑g) = Additive.ofMul (Abelianization.of ↑g)

The projection G^ab → (G/V)^ab sends the class of g to the class of g.

theorem TauCeti.ClassFieldTheory.NormalLayer.abelianizationRestrict_surjective {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (V : OpenNormalSubgroup G) : Function.Surjective ⇑(abelianizationRestrict V)

The projection G^ab → (G/V)^ab is surjective.

@[simp]

theorem TauCeti.ClassFieldTheory.LayerRefinement.quotientHom_abelianizationRestrict {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V W : OpenNormalSubgroup G} (T : LayerRefinement (NormalLayer.ofOpenNormal V) (NormalLayer.ofOpenNormal W)) (x : Additive (TopologicalAbelianization G)) : T.quotientHom ((NormalLayer.abelianizationRestrict W) x) = (NormalLayer.abelianizationRestrict V) x

The projections of G^ab are compatible with refinement: for open normal subgroups W ≤ V of G, projecting to (G/W)^ab and then to the quotient (G/V)^ab is the projection to (G/V)^ab.

Finite quotients of the topological abelianization

theorem TauCeti.ClassFieldTheory.NormalLayer.exists_abelianizationRestrict_eq_zero_iff {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : OpenSubgroup (TopologicalAbelianization G)) : ∃ (V : OpenNormalSubgroup G), ∀ (x : TopologicalAbelianization G), (abelianizationRestrict V) (Additive.ofMul x) = 0 ↔ x ∈ U

Every open subgroup of G^ab is cut out by a finite layer. For every open subgroup U of G^ab there is an open normal subgroup V of G (the preimage of U) such that U is the kernel of the projection G^ab → (G/V)^ab.

The absolute Artin map

noncomputable def TauCeti.ClassFieldTheory.ClassFormation.absoluteArtinMap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) : ↥(F.level ⊤) →+ Additive (TopologicalAbelianization G)

The absolute Artin map A^G → G^ab of a class formation over a profinite group G: the inverse limit of the finite Artin maps A^G → (G/V)^ab of the layers V ◁ G. Its composite with the projection onto each (G/V)^ab is the finite Artin map (abelianizationRestrict_absoluteArtinMap), and it is the only homomorphism with this property (eq_absoluteArtinMap_of_forall_abelianizationRestrict).

@[simp]

theorem TauCeti.ClassFieldTheory.ClassFormation.abelianizationRestrict_absoluteArtinMap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (V : OpenNormalSubgroup G) (a : ↥(F.level ⊤)) : (NormalLayer.abelianizationRestrict V) (cf.absoluteArtinMap a) = (cf.artinMap (NormalLayer.ofOpenNormal V)) ((NormalLayer.groundEquivOfOpenNormal F V) a)

The finite restrictions of the absolute Artin map are the finite Artin maps: projecting the absolute Artin symbol of a ∈ A^G to the abelianized Galois group (G/V)^ab of the layer V ◁ G gives the Artin symbol of a for that layer.

theorem TauCeti.ClassFieldTheory.NormalLayer.eq_of_forall_abelianizationRestrict_eq {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {x y : Additive (TopologicalAbelianization G)} (h : ∀ (V : OpenNormalSubgroup G), (abelianizationRestrict V) x = (abelianizationRestrict V) y) : x = y

Elements of G^ab with the same projection to (G/V)^ab for every open normal subgroup V of G are equal.

theorem TauCeti.ClassFieldTheory.NormalLayer.eq_of_forall_le_abelianizationRestrict_eq {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (N : OpenNormalSubgroup G) {x y : Additive (TopologicalAbelianization G)} (h : ∀ V ≤ N, (abelianizationRestrict V) x = (abelianizationRestrict V) y) : x = y

Elements of G^ab with the same projection to (G/V)^ab for every open normal subgroup V of G contained in a fixed open normal subgroup N are equal: the layers below N are cofinal.

theorem TauCeti.ClassFieldTheory.ClassFormation.eq_absoluteArtinMap_of_forall_abelianizationRestrict {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (φ : ↥(F.level ⊤) →+ Additive (TopologicalAbelianization G)) (hφ : ∀ (V : OpenNormalSubgroup G) (a : ↥(F.level ⊤)), (NormalLayer.abelianizationRestrict V) (φ a) = (cf.artinMap (NormalLayer.ofOpenNormal V)) ((NormalLayer.groundEquivOfOpenNormal F V) a)) : φ = cf.absoluteArtinMap

Uniqueness of the absolute Artin map: a homomorphism A^G → G^ab whose projection to (G/V)^ab is the finite Artin map of the layer V ◁ G, for every open normal subgroup V, is the absolute Artin map.

theorem TauCeti.ClassFieldTheory.ClassFormation.abelianizationRestrict_absoluteArtinMap_eq_zero_iff {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (V : OpenNormalSubgroup G) (a : ↥(F.level ⊤)) : (NormalLayer.abelianizationRestrict V) (cf.absoluteArtinMap a) = 0 ↔ (NormalLayer.groundEquivOfOpenNormal F V) a ∈ (NormalLayer.ofOpenNormal V).normSubgroup F

The absolute Artin symbol of a ∈ A^G dies in (G/V)^ab exactly when a is a norm from the layer V ◁ G.

theorem TauCeti.ClassFieldTheory.ClassFormation.exists_absoluteArtinMap_mem_iff {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (U : OpenSubgroup (TopologicalAbelianization G)) : ∃ (V : OpenNormalSubgroup G), ∀ (a : ↥(F.level ⊤)), Additive.toMul (cf.absoluteArtinMap a) ∈ U ↔ (NormalLayer.groundEquivOfOpenNormal F V) a ∈ (NormalLayer.ofOpenNormal V).normSubgroup F

The preimage of an open subgroup under the absolute Artin map is a norm subgroup. For every open subgroup U of G^ab there is an open normal subgroup V of G such that the absolute Artin symbol of a ∈ A^G lies in U exactly when a is a norm from the layer V ◁ G.

theorem TauCeti.ClassFieldTheory.ClassFormation.absoluteArtinMap_eq_zero_iff {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (a : ↥(F.level ⊤)) : cf.absoluteArtinMap a = 0 ↔ ∀ (V : OpenNormalSubgroup G), (NormalLayer.groundEquivOfOpenNormal F V) a ∈ (NormalLayer.ofOpenNormal V).normSubgroup F

The kernel of the absolute Artin map is the intersection of the norm subgroups: the absolute Artin symbol of a ∈ A^G vanishes exactly when a is a norm from every layer V ◁ G.

theorem TauCeti.ClassFieldTheory.ClassFormation.denseRange_absoluteArtinMap {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) : DenseRange ⇑cf.absoluteArtinMap

The absolute Artin map has dense image: modulo every open normal subgroup of G^ab it is a finite Artin map, which is surjective.