Class field towers

DefinitionEverywhere unramified extension#✓fully proved

Let \(M/F\) be an extension of number fields, with rings of integers \(\mathcal{O}_F\) and \(\mathcal{O}_M\). Then \(M/F\) is everywhere unramified when every prime ideal \(\mathfrak{P}\) of \(\mathcal{O}_M\) lying over a nonzero prime ideal \(\mathfrak{p}\) of \(\mathcal{O}_F\) has ramification index \(1\) over \(\mathcal{O}_F\), and every infinite place of \(M\) lying over a real place of \(F\) is real.

def IsEverywhereUnramified
    (F M : Type) [Field F] [Field M] [NumberField F] [NumberField M]
    [Algebra F M] : Prop :=
  (∀ (𝔭 : Ideal (𝓞 F)) (𝔓 : Ideal (𝓞 M)),
      𝔭.IsPrime → 𝔭 ≠ ⊥ →
      𝔓 ∈ 𝔭.primesOver (𝓞 M) →
      𝔓.ramificationIdx (𝓞 F) = 1) ∧
  (∀ w : NumberField.InfinitePlace F, w.IsReal →
    ∀ w' : NumberField.InfinitePlace M,
      w'.comap (algebraMap F M) = w → w'.IsReal)

Used by 1

Used byMaximal unramified pro-\(p\) extension

DefinitionMaximal unramified pro-\(p\) extension#✓fully proved

Let \(F\) be a number field, \(\overline{F}\) an algebraic closure of \(F\), and \(p\) a prime. The maximal unramified pro-\(p\) extension \(F^{\mathrm{un},p}\) of \(F\) is the compositum in \(\overline{F}\) of all intermediate fields \(F \subseteq M \subseteq \overline{F}\) such that \(M/F\) is finite, Galois and everywhere unramified, and its Galois group \(\mathrm{Gal}(M/F)\) is a \(p\)-group (each such \(M\) is a number field).

noncomputable def maximalUnramifiedProPF
    (F : Type) [Field F] [NumberField F]
    (p : ℕ) [Fact (Nat.Prime p)] :
    IntermediateField F (AlgebraicClosure F) :=
  ⨆ (M : IntermediateField F (AlgebraicClosure F))
      (_ : FiniteDimensional F M)
      (_ : IsGalois F M)
      (_ : IsPGroup p (M ≃ₐ[F] M))
      (_ : NumberField M)
      (_ : IsEverywhereUnramified F M),
    M

Uses 1 · Used by 2

Statement usesEverywhere unramified extension

Used byGalois group of the maximal unramified pro-\(p\) extension · Shafarevich's relation-rank bound

DefinitionGalois group of the maximal unramified pro-\(p\) extension#✓fully proved

For a number field \(F\) and a prime \(p\), this is the group \(\mathrm{Gal}(F^{\mathrm{un},p}/F)\) of field automorphisms of the maximal unramified pro-\(p\) extension \(F^{\mathrm{un},p}\) of \(F\) that fix \(F\), under composition and with the Krull topology.

noncomputable def MaxUnramifiedProPGaloisGroup
    (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact (Nat.Prime p)] :
    Type :=
  (maximalUnramifiedProPF F p) ≃ₐ[F] (maximalUnramifiedProPF F p)

Uses 1 · Used by 1

Statement usesMaximal unramified pro-\(p\) extension

Used byShafarevich's relation-rank bound

DefinitionGenerator rank of a topological group#✓fully proved

For a topological group \(G\), the generator rank \(d(G)\) is the least natural number \(k\) such that some finite subset \(S \subseteq G\) with \(k\) elements generates a dense subgroup of \(G\). If no finite subset of \(G\) generates a dense subgroup, then \(d(G) = 0\) by convention.

noncomputable def generatorRank
    (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ℕ :=
  sInf {k : ℕ | ∃ S : Finset G, S.card = k ∧
    (Subgroup.closure (S : Set G)).topologicalClosure = ⊤}

Used by 1

Used byShafarevich's relation-rank bound

DefinitionTrivial representation on \(\mathbb{Z}/p\mathbb{Z}\)#✓fully proved

For a natural number \(p\) and a topological group \(G\), this is \(\mathbb{Z}/p\mathbb{Z}\) with the discrete topology, regarded as a continuous representation of \(G\) over \(\mathbb{Z}/p\mathbb{Z}\) on which every element of \(G\) acts as the identity.

noncomputable def trivialZModpRep
    (p : ℕ) (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    TopRep (ZMod p) G :=
  TopRep.of (ContRepresentation.trivial (ZMod p) G (ZMod p))

Used by 2

Used byFinite-dimensional second cohomology mod \(p\) · Relation rank of a topological group

DefinitionRelation rank of a topological group#✓fully proved

For a prime \(p\) and a topological group \(G\), the relation rank \(r(G)\) is the dimension over \(\mathbb{F}_p\) of the continuous cohomology group \(H^2(G, \mathbb{F}_p)\) of degree \(2\), with coefficients in the trivial representation of \(G\) on \(\mathbb{F}_p\). If this space is infinite-dimensional, then \(r(G) = 0\) by convention.

noncomputable def relationRank
    (p : ℕ) [Fact p.Prime] (G : Type)
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ℕ :=
  Module.finrank (ZMod p)
    (continuousCohomology 2 (trivialZModpRep p G))

Uses 1 · Used by 1

Statement usesTrivial representation on \(\mathbb{Z}/p\mathbb{Z}\)

Used byShafarevich's relation-rank bound

DefinitionFinite-dimensional second cohomology mod \(p\)#✓fully proved

For a prime \(p\) and a topological group \(G\), this is the statement that the continuous cohomology group \(H^2(G, \mathbb{F}_p)\) of degree \(2\), with coefficients in the trivial representation of \(G\) on \(\mathbb{F}_p\), is finite-dimensional over \(\mathbb{F}_p\).

def H2Finite (p : ℕ) [Fact p.Prime] (G : Type)
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop :=
  FiniteDimensional (ZMod p)
    (continuousCohomology 2 (trivialZModpRep p G))

Uses 1 · Used by 1

Statement usesTrivial representation on \(\mathbb{Z}/p\mathbb{Z}\)

Used byShafarevich's relation-rank bound

TheoremShafarevich's relation-rank bound#●ready to prove

Let \(F\) be a number field, let \(p\) be an odd prime, and let \(G = \mathrm{Gal}(F^{\mathrm{un},p}/F)\) be the Galois group of the maximal unramified pro-\(p\) extension of \(F\). Write \(d(G)\) for the generator rank and \(r(G)\) for the relation rank of \(G\), \(r_1\) and \(r_2\) for the numbers of real and complex places of \(F\), and \(\delta\) for \(1\) if \(F\) contains a primitive \(p\)-th root of unity and \(0\) otherwise. Then the continuous cohomology group \(H^2(G, \mathbb{F}_p)\) with trivial coefficients is finite-dimensional over \(\mathbb{F}_p\), and

\[r(G) \le d(G) + (r_1 + r_2 - 1) + \delta.\]

public theorem_wanted shafarevich_relation_rank_bound
    (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime] (_hpOdd : Odd p) :
    H2Finite p (MaxUnramifiedProPGaloisGroup F p) ∧
      (open Classical in
       relationRank p (MaxUnramifiedProPGaloisGroup F p) ≤
        generatorRank (MaxUnramifiedProPGaloisGroup F p) +
          (NumberField.InfinitePlace.nrRealPlaces F +
            NumberField.InfinitePlace.nrComplexPlaces F - 1) +
          (if ∃ ζ : F, IsPrimitiveRoot ζ p then 1 else 0))

Sources

• D. C. Mayer, New number fields with known p-class tower, Tatra Mt. Math. Publ. 64 (2015), 21–57 (Theorem 5.1, S=∅; arXiv:1510.00565); H. Koch, Galois Theory of p-Extensions, Springer 2002 (Theorems 11.5 and 11.8); I. R. Shafarevich, Extensions with prescribed ramification points (1963). Lean hypothesis: https://github.com/logical-intelligence/erdos-unit-distance (Hyp_ShafarevichRelationRankBound). Problem shafarevich_relation_rank_bound of the lean-eval benchmark.

Uses 5

Statement usesFinite-dimensional second cohomology mod \(p\) · Galois group of the maximal unramified pro-\(p\) extension · Generator rank of a topological group · Maximal unramified pro-\(p\) extension · Relation rank of a topological group

7 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.