Module

EverywhereUnramifiedProPFiniteFamily.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.EverywhereUnramifiedProPFiniteFamily

3 declarations indexed from sourceView source ↗

Module documentation

Finite families of everywhere-unramified pro-p extensions

For an odd prime p, every finite family of bundled finite Galois everywhere-unramified p-extensions has a bundled compositum. Its underlying field is the finite supremum of the fields in the family.

Imports1

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.EverywhereUnramifiedProPCompositum

Imported by1

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.All

theorem

exists_finsetSup

L29 ↗

ClassFieldTower.Martinet.FiniteEverywhereUnramifiedProPExtension.exists_finsetSup

Documentation

A finite family of candidates has a candidate whose underlying field is the finite supremum of the family.

Source context 6 commands

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

noncomputable section
universe u v
namespace ClassFieldTower.Martinet
namespace FiniteEverywhereUnramifiedProPExtension
variable {F : Type u} [Field F] [NumberField F]
variable {p : ℕ} [Fact p.Prime]

Lean source · statement

theorem exists_finsetSup
    {I : Type v} (hpOdd : Odd p)
    (E : I → FiniteEverywhereUnramifiedProPExtension F p)
    (s : Finset I) :
    ∃ C : FiniteEverywhereUnramifiedProPExtension F p,
      C.field = ⨆ i, ⨆ (_ : i ∈ s), (E i).field

def

finsetSup

L48 ↗

ClassFieldTower.Martinet.FiniteEverywhereUnramifiedProPExtension.finsetSup

Documentation

A chosen bundled compositum for a finite family of candidates.

Source context 6 commands

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

noncomputable section
universe u v
namespace ClassFieldTower.Martinet
namespace FiniteEverywhereUnramifiedProPExtension
variable {F : Type u} [Field F] [NumberField F]
variable {p : ℕ} [Fact p.Prime]

Lean source · statement

def finsetSup
    {I : Type v} (hpOdd : Odd p)
    (E : I → FiniteEverywhereUnramifiedProPExtension F p)
    (s : Finset I) :
    FiniteEverywhereUnramifiedProPExtension F p

theorem

finsetSup_field

L58 ↗

ClassFieldTower.Martinet.FiniteEverywhereUnramifiedProPExtension.finsetSup_field

Documentation

The underlying field of the chosen finite-family compositum is exactly the finite supremum.

Source context 6 commands

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

noncomputable section
universe u v
namespace ClassFieldTower.Martinet
namespace FiniteEverywhereUnramifiedProPExtension
variable {F : Type u} [Field F] [NumberField F]
variable {p : ℕ} [Fact p.Prime]

Lean source · statement

theorem finsetSup_field
    {I : Type v} (hpOdd : Odd p)
    (E : I → FiniteEverywhereUnramifiedProPExtension F p)
    (s : Finset I) :
    (finsetSup hpOdd E s).field =
      ⨆ i, ⨆ (_ : i ∈ s), (E i).field

Module documentation

Finite families of everywhere-unramified pro-p extensions

Declarations

exists_finsetSup

finsetSup

finsetSup_field