Module

MaximalEverywhereUnramifiedProPFiniteSupport.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.MaximalEverywhereUnramifiedProPFiniteSupport

3 declarations indexed from sourceView source ↗

Module documentation

Finite support in the maximal everywhere-unramified pro-p compositum

Finite-dimensional intermediate fields are compact in the lattice of intermediate fields. Consequently, an inclusion into the maximal compositum already factors through a supremum of finitely many bundled finite extensions.

Imports2

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.EverywhereUnramifiedProPCompositum
Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Imported by3

theorem

finiteDimensional_intermediateField_isCompactElement

L28 ↗

ClassFieldTower.Martinet.finiteDimensional_intermediateField_isCompactElement

Documentation

A finite-dimensional intermediate field is a compact element of the complete lattice of intermediate fields.

Source context 4 commands

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

open scoped NumberField
noncomputable section
universe u v
namespace ClassFieldTower.Martinet

Lean source · statement

theorem finiteDimensional_intermediateField_isCompactElement
    {F : Type u} {E : Type v}
    [Field F] [Field E] [Algebra F E]
    (L : IntermediateField F E) [FiniteDimensional F L] :
    IsCompactElement L

theorem

finiteDimensional_le_iSup_exists_finset

L40 ↗

ClassFieldTower.Martinet.finiteDimensional_le_iSup_exists_finset

Documentation

A finite-dimensional intermediate field below a supremum is already below a finite sub-supremum.

Source context 4 commands

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

open scoped NumberField
noncomputable section
universe u v
namespace ClassFieldTower.Martinet

Lean source · statement

theorem finiteDimensional_le_iSup_exists_finset
    {F : Type u} {E : Type v} {I : Type*}
    [Field F] [Field E] [Algebra F E]
    (L : IntermediateField F E) [FiniteDimensional F L]
    (f : I → IntermediateField F E)
    (hL : L ≤ ⨆ i, f i) :
    ∃ s : Finset I, L ≤ ⨆ i ∈ s, f i

theorem

finiteDimensional_le_maximalEverywhereUnramifiedProP_exists_finset

L52 ↗

ClassFieldTower.Martinet.finiteDimensional_le_maximalEverywhereUnramifiedProP_exists_finset

Documentation

A finite-dimensional intermediate field below the maximal compositum is already below the supremum of finitely many bundled extensions.

Source context 4 commands

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

open scoped NumberField
noncomputable section
universe u v
namespace ClassFieldTower.Martinet

Lean source · statement

theorem finiteDimensional_le_maximalEverywhereUnramifiedProP_exists_finset
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact p.Prime]
    (L : IntermediateField F (AlgebraicClosure F))
    [FiniteDimensional F L]
    (hL : L ≤ maximalEverywhereUnramifiedProP F p) :
    ∃ s : Finset (FiniteEverywhereUnramifiedProPExtension F p),
      L ≤ ⨆ E ∈ s, E.field

Module documentation

Finite support in the maximal everywhere-unramified pro-p compositum

Declarations

finiteDimensional_intermediateField_isCompactElement

finiteDimensional_le_iSup_exists_finset

finiteDimensional_le_maximalEverywhereUnramifiedProP_exists_finset