Module

FiniteSupport.lean

Nyll.ValuedFieldTheory.LocalField.Unramified.FiniteSupport

3 declarations indexed from sourceView source ↗

Module documentation

Finite support in the maximal unramified field

The maximal unramified subextension is defined as a compositum. Compactness of a simple intermediate field and stability under finite composita imply that every one of its elements already belongs to a single finite unramified subextension. This is the finite-support fact used in the maximal-residue theorem.

Imports2

Imported by3

theorem

finiteUnramifiedSubextension_bot

L32 ↗

AlgebraicNumberTheory.Valuations.finiteUnramifiedSubextension_bot

Documentation

The base field, viewed as the bottom intermediate field, is finite unramified. This supplies the empty finite-compositum case.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section FiniteSupport
variable {K L : Type u} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem finiteUnramifiedSubextension_bot
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation) :
    FiniteUnramifiedSubextension v w hExt ⊥

theorem

finiteUnramifiedSubextension_finset_iSup

L70 ↗

AlgebraicNumberTheory.Valuations.finiteUnramifiedSubextension_finset_iSup

Documentation

A finite supremum of finite unramified intermediate fields is finite unramified.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section FiniteSupport
variable {K L : Type u} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem finiteUnramifiedSubextension_finset_iSup
    {ι : Type*}
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation)
    (s : Finset ι) (F : ι → IntermediateField K L)
    (hs : ∀ i ∈ s, FiniteUnramifiedSubextension v w hExt (F i)) :
    FiniteUnramifiedSubextension v w hExt
      (⨆ i : ι, ⨆ (_h : i ∈ s), F i)

theorem

exists_finiteUnramifiedSubextension_of_mem_maximal

L134 ↗

AlgebraicNumberTheory.Valuations.exists_finiteUnramifiedSubextension_of_mem_maximal

Documentation

Every element of the maximal unramified subextension belongs to one finite unramified intermediate field.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section FiniteSupport
variable {K L : Type u} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem exists_finiteUnramifiedSubextension_of_mem_maximal
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation)
    {x : L}
    (hx : x ∈ maximalUnramifiedSubextension v w hExt) :
    ∃ E : IntermediateField K L,
      x ∈ E ∧ FiniteUnramifiedSubextension v w hExt E

Module documentation

Finite support in the maximal unramified field

Declarations

finiteUnramifiedSubextension_bot

finiteUnramifiedSubextension_finset_iSup

exists_finiteUnramifiedSubextension_of_mem_maximal