Module

FiniteRealPExtensionSupport.lean

Nyll.SawinTotallyRealTowers.FiniteRealPExtensionSupport

3 declarations indexed from sourceView source ↗

Module documentation

Finite support in the real pro-p tower

Compact intermediate fields contained in the supremum of admissible finite layers lie in one layer, since the family is nonempty and directed. This applies both to finite-dimensional intermediate fields and to the field generated by finitely many elements.

Imports2

Imported by3

theorem

compact_le_iSup_realPExtension_exists_extension

L26 ↗

ClassFieldTower.Sawin.compact_le_iSup_realPExtension_exists_extension

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin

Lean source · statement

theorem compact_le_iSup_realPExtension_exists_extension
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (L : IntermediateField ℚ (AlgebraicClosure ℚ))
    (hCompact : IsCompactElement L)
    (hL : L ≤ ⨆ E : FiniteRealPExtension p T, E.val.toIntermediateField) :
    ∃ C : FiniteRealPExtension p T, L ≤ C.val.toIntermediateField

theorem

finiteDimensional_le_iSup_realPExtension_exists_extension

L48 ↗

ClassFieldTower.Sawin.finiteDimensional_le_iSup_realPExtension_exists_extension

Documentation

A finite-dimensional intermediate field in the supremum of admissible finite layers is contained in one admissible finite layer.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin

Lean source · statement

theorem finiteDimensional_le_iSup_realPExtension_exists_extension
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (L : IntermediateField ℚ (AlgebraicClosure ℚ)) [FiniteDimensional ℚ L]
    (hL : L ≤ ⨆ E : FiniteRealPExtension p T, E.val.toIntermediateField) :
    ∃ C : FiniteRealPExtension p T, L ≤ C.val.toIntermediateField

theorem

finset_subset_iSup_realPExtension_exists_extension

L58 ↗

ClassFieldTower.Sawin.finset_subset_iSup_realPExtension_exists_extension

Documentation

Finitely many elements of the supremum all belong to a single admissible finite layer.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin

Lean source · statement

theorem finset_subset_iSup_realPExtension_exists_extension
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (s : Finset (AlgebraicClosure ℚ))
    (hs : ∀ x ∈ s, x ∈ ⨆ E : FiniteRealPExtension p T, E.val.toIntermediateField) :
    ∃ C : FiniteRealPExtension p T, ∀ x ∈ s, x ∈ C.val.toIntermediateField

Module documentation

Finite support in the real pro-p tower

Declarations

compact_le_iSup_realPExtension_exists_extension

finiteDimensional_le_iSup_realPExtension_exists_extension

finset_subset_iSup_realPExtension_exists_extension