The induction on the index in the proof of the existence theorem

Let F be a formation on a profinite group G, with level A^W for an open subgroup W, the module of the field E that W cuts out. A subgroup N ⊆ A^W contains a norm group if it contains the image of the norm N_{W/W'} : A^{W'} → A^W from some open W' ≤ W, the norm group of a finite, not necessarily Galois, extension of E. In a class formation such a subgroup of the ground level A^G is the norm subgroup of an abelian layer (ClassFormation.exists_abelianLayer_normSubgroup_eq_of_range_levelNorm_le).

This file proves the induction on the index by which the global existence theorem is deduced from its Kummer case (Milne, Class Field Theory, VII, Theorem 9.5, from Lemmas 9.3 and 9.4). Fix, for every open subgroup W, a class of admissible subgroups of A^W, closed under enlargement and under preimages by the norms N_{W/W'}. For the idele classes these are the open subgroups of C_E. Suppose that for every prime p and every open W there is an open W' ≤ W such that over W' every admissible subgroup of finite index containing p · A^{W'} contains a norm group. For the idele classes, W' cuts out E(ζ_p), and the hypothesis is the Kummer case. Then every admissible subgroup of finite index of every level contains a norm group (Formation.exists_range_levelNorm_le_of_forall_prime). In a class formation, every admissible subgroup of finite index of the ground level is therefore the norm subgroup of an abelian layer (ClassFormation.exists_abelianLayer_normSubgroup_eq_of_forall_prime).

The proof is by strong induction on the index n of N ⊆ A^W, simultaneously for all W. If n > 1, choose a prime p ∣ n and the open W' ≤ W of the hypothesis. By descent along the norm (Milne VII, Lemma 9.4) it suffices that the preimage N' of N in A^{W'} contains a norm group, and the index of N' is at most n. If it is smaller, the induction hypothesis applies. Otherwise p divides the order of A^{W'}/N'. The preimage N₁ of p · (A^{W'}/N') then contains N' and p · A^{W'}, and it is proper, because multiplication by p on the finite group A^{W'}/N' is not injective by Cauchy's theorem, hence not surjective. By the hypothesis N₁ contains the norm group of some W₁ ≤ W'. The preimage of N' in A^{W₁} has index at most [N₁ : N'] < n, so it contains a norm group by induction, and so does N'.

The induction is not an existence theorem: the class-formation axioms do not imply the Kummer hypothesis, which is an arithmetic statement about each setting.

Main statements

• TauCeti.ClassFieldTheory.Formation.exists_range_levelNorm_le_of_forall_prime: from the Kummer case, every admissible subgroup of finite index of a level contains a norm group.
• TauCeti.ClassFieldTheory.ClassFormation.exists_abelianLayer_normSubgroup_eq_of_forall_prime: in a class formation, every admissible subgroup of finite index of the ground level is then the norm subgroup of an abelian layer.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, §9, Lemmas 9.3 and 9.4 and Theorem 9.5.
• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §6.

theorem TauCeti.ClassFieldTheory.Formation.exists_range_levelNorm_le_of_forall_prime {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (P : (W : OpenSubgroup G) → AddSubgroup ↥(F.level W) → Prop) (hP_mono : ∀ {W : OpenSubgroup G} {N N' : AddSubgroup ↥(F.level W)}, P W N → N ≤ N' → P W N') (hP_comap : ∀ {W W' : OpenSubgroup G} (h : W' ≤ W) {N : AddSubgroup ↥(F.level W)}, P W N → P W' (AddSubgroup.comap (F.levelNorm h) N)) (hkummer : ∀ (p : ℕ), Nat.Prime p → ∀ (W : OpenSubgroup G), ∃ W' ≤ W, ∀ (N : AddSubgroup ↥(F.level W')), P W' N → N.FiniteIndex → (∀ (a : ↥(F.level W')), p • a ∈ N) → ∃ (W'' : OpenSubgroup G) (h : W'' ≤ W'), (F.levelNorm h).range ≤ N) {W : OpenSubgroup G} (N : AddSubgroup ↥(F.level W)) (hN : P W N) [N.FiniteIndex] : ∃ (W' : OpenSubgroup G) (h : W' ≤ W), (F.levelNorm h).range ≤ N

The induction on the index in the existence theorem (Milne VII, Theorem 9.5). Let P W be a class of admissible subgroups of the level A^W, for each open subgroup W (the open subgroups of C_E for the idele classes), closed under enlargement and under preimages by the norms between levels. Suppose that for every prime p and every open W there is an open W' ≤ W over which every admissible subgroup of finite index containing p · A^{W'} contains the norm group of an open subgroup of W'; for the idele classes, W' cuts out E(ζ_p) and this is the Kummer case (Milne VII, Lemma 9.3). Then every admissible subgroup of finite index of a level A^W contains the norm group N_{W/W'}(A^{W'}) of an open subgroup W' ≤ W.

theorem TauCeti.ClassFieldTheory.ClassFormation.exists_abelianLayer_normSubgroup_eq_of_forall_prime {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (P : (W : OpenSubgroup G) → AddSubgroup ↥(F.level W) → Prop) (hP_mono : ∀ {W : OpenSubgroup G} {N N' : AddSubgroup ↥(F.level W)}, P W N → N ≤ N' → P W N') (hP_comap : ∀ {W W' : OpenSubgroup G} (h : W' ≤ W) {N : AddSubgroup ↥(F.level W)}, P W N → P W' (AddSubgroup.comap (F.levelNorm h) N)) (hkummer : ∀ (p : ℕ), Nat.Prime p → ∀ (W : OpenSubgroup G), ∃ W' ≤ W, ∀ (N : AddSubgroup ↥(F.level W')), P W' N → N.FiniteIndex → (∀ (a : ↥(F.level W')), p • a ∈ N) → ∃ (W'' : OpenSubgroup G) (h : W'' ≤ W'), (F.levelNorm h).range ≤ N) (N : Submodule ℤ ↥(F.level ⊤)) (hN : P ⊤ N.toAddSubgroup) [N.toAddSubgroup.FiniteIndex] : ∃ (V : OpenNormalSubgroup G), V.IsAbelianClassFieldLayer ∧ F.normSubgroup V = N

Existence from the Kummer case, in a class formation (Milne VII, Theorem 9.5). Under the hypotheses of Formation.exists_range_levelNorm_le_of_forall_prime, namely a class P of admissible subgroups of the levels, closed under enlargement and under preimages by norms, and the Kummer case over a suitable open subgroup of every open subgroup for every prime, every admissible subgroup of finite index of the ground level A^G is the norm subgroup of an abelian layer.