Module

DirectedIntermediateFields.lean

Nyll.AnabelianGeometry.KummerTheory.DirectedIntermediateFields

3 declarations indexed from sourceView source ↗

Module documentation

Finite subfields in directed unions

A finite extension contained in a directed union already lies in one member. In particular, its intersection with the entire union is attained at a finite level. This is the finite-level input for cyclotomic towers.

Imports1

Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Imported by1

Nyll.AnabelianGeometry.KummerTheory.All

theorem

finiteDimensional_isCompactElement

L23 ↗

AnabelianGeometry.KummerTheory.finiteDimensional_isCompactElement

Documentation

A finite-dimensional intermediate field is compact in the lattice of intermediate fields, even when the ambient extension is infinite.

Source context 2 commands

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

namespace AnabelianGeometry.KummerTheory
variable {F L : Type*} [Field F] [Field L] [Algebra F L]

Lean source · statement

theorem finiteDimensional_isCompactElement (E : IntermediateField F L)
    [FiniteDimensional F E] : IsCompactElement E

theorem

exists_le_of_finiteDimensional_of_directed

L31 ↗

AnabelianGeometry.KummerTheory.exists_le_of_finiteDimensional_of_directed

Documentation

A finite extension inside a directed union is contained in one level.

Source context 2 commands

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

namespace AnabelianGeometry.KummerTheory
variable {F L : Type*} [Field F] [Field L] [Algebra F L]

Lean source · statement

theorem exists_le_of_finiteDimensional_of_directed
    {ι : Type*} [Nonempty ι] (C : ι → IntermediateField F L)
    (hC : Directed (· ≤ ·) C) (E : IntermediateField F L)
    [FiniteDimensional F E] (hE : E ≤ ⨆ i, C i) :
    ∃ i, E ≤ C i

theorem

exists_inf_iSup_eq_inf_of_finiteDimensional

L51 ↗

AnabelianGeometry.KummerTheory.exists_inf_iSup_eq_inf_of_finiteDimensional

Documentation

The intersection of a finite extension with a directed union is already attained at one level of the union.

Source context 2 commands

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

namespace AnabelianGeometry.KummerTheory
variable {F L : Type*} [Field F] [Field L] [Algebra F L]

Lean source · statement

theorem exists_inf_iSup_eq_inf_of_finiteDimensional
    {ι : Type*} [Nonempty ι] (C : ι → IntermediateField F L)
    (hC : Directed (· ≤ ·) C) (E : IntermediateField F L)
    [FiniteDimensional F E] :
    ∃ i, E ⊓ (⨆ j, C j) = E ⊓ C i

Module documentation

Finite subfields in directed unions

Declarations

finiteDimensional_isCompactElement

exists_le_of_finiteDimensional_of_directed

exists_inf_iSup_eq_inf_of_finiteDimensional