Module

MaximalEverywhereUnramifiedProPCofinality.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.MaximalEverywhereUnramifiedProPCofinality

4 declarations indexed from sourceView source ↗

Module documentation

Cofinality of finite everywhere-unramified pro-p extensions

For odd p, the bundled finite extensions are directed under binary compositum. Compactness therefore upgrades finite support in the maximal compositum to containment in one bundled extension.

Imports1

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.MaximalEverywhereUnramifiedProPFiniteSupport

Imported by2

theorem

finite_iSup_extension_le_extension

L25 ↗

ClassFieldTower.Martinet.finite_iSup_extension_le_extension

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet

Lean source · statement

theorem finite_iSup_extension_le_extension
    {F : Type u} [Field F] [NumberField F]
    {p : ℕ} [Fact p.Prime]
    (hpOdd : Odd p)
    (s : Finset (FiniteEverywhereUnramifiedProPExtension F p)) :
    ∃ C : FiniteEverywhereUnramifiedProPExtension F p,
      (⨆ E ∈ s, E.field) ≤ C.field

theorem

finiteDimensional_le_maximalEverywhereUnramifiedProP_exists_extension

L44 ↗

ClassFieldTower.Martinet.finiteDimensional_le_maximalEverywhereUnramifiedProP_exists_extension

Documentation

Every finite-dimensional intermediate field below the maximal compositum is contained in one bundled finite everywhere-unramified pro-p extension.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet

Lean source · statement

theorem finiteDimensional_le_maximalEverywhereUnramifiedProP_exists_extension
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact p.Prime]
    (hpOdd : Odd p)
    (L : IntermediateField F (AlgebraicClosure F))
    [FiniteDimensional F L]
    (hL : L ≤ maximalEverywhereUnramifiedProP F p) :
    ∃ C : FiniteEverywhereUnramifiedProPExtension F p, L ≤ C.field

theorem

mem_maximalEverywhereUnramifiedProP_exists_extension

L60 ↗

ClassFieldTower.Martinet.mem_maximalEverywhereUnramifiedProP_exists_extension

Documentation

Every element of the maximal compositum lies in one bundled finite everywhere-unramified pro-p extension.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet

Lean source · statement

theorem mem_maximalEverywhereUnramifiedProP_exists_extension
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact p.Prime]
    (hpOdd : Odd p)
    {x : AlgebraicClosure F}
    (hx : x ∈ maximalEverywhereUnramifiedProP F p) :
    ∃ C : FiniteEverywhereUnramifiedProPExtension F p, x ∈ C.field

theorem

isEverywhereUnramified_of_le_maximalEverywhereUnramifiedProP

L81 ↗

ClassFieldTower.Martinet.isEverywhereUnramified_of_le_maximalEverywhereUnramifiedProP

Documentation

A finite Galois intermediate field below the maximal compositum is everywhere unramified over the base field.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet

Lean source · statement

theorem isEverywhereUnramified_of_le_maximalEverywhereUnramifiedProP
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact p.Prime]
    (hpOdd : Odd p)
    (L : IntermediateField F (AlgebraicClosure F))
    [FiniteDimensional F L] [IsGalois F L] [NumberField L]
    (hL : L ≤ maximalEverywhereUnramifiedProP F p) :
    IsEverywhereUnramified F L

Module documentation

Cofinality of finite everywhere-unramified pro-p extensions

Declarations

finite_iSup_extension_le_extension

finiteDimensional_le_maximalEverywhereUnramifiedProP_exists_extension

mem_maximalEverywhereUnramifiedProP_exists_extension

isEverywhereUnramified_of_le_maximalEverywhereUnramifiedProP