NYLL
Module

MaximalSubextension.lean

Nyll.ValuedFieldTheory.LocalField.Unramified.MaximalSubextension
6 declarations indexed from sourceView source ↗

Module documentation

The maximal unramified subextension

Let L/K be an algebraic valued extension. Its maximal unramified subextension is the compositum, inside L, of all unramified subextensions. Since the finite unramified-extension definition defines an arbitrary unramified extension as a union of finite unramified subextensions, this compositum is the supremum of the finite unramified intermediate fields.

Imports1
Imported by4

Declarations

def

finiteUnramifiedSubextensions

L31 ↗
AlgebraicNumberTheory.Valuations.finiteUnramifiedSubextensions
Documentation

The finite unramified intermediate fields occurring in the finite unramified-extension definition.

Source context 5 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
section MaximalUnramifiedSubextension
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
def finiteUnramifiedSubextensions
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) :
    Set (IntermediateField K L)
theorem

mem_finiteUnramifiedSubextensions_iff

L39 ↗
AlgebraicNumberTheory.Valuations.mem_finiteUnramifiedSubextensions_iff
Source context 5 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
section MaximalUnramifiedSubextension
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem mem_finiteUnramifiedSubextensions_iff
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    {E : IntermediateField K L} :
    E ∈ finiteUnramifiedSubextensions v w hExt ↔
      FiniteUnramifiedSubextension v w hExt E
def

maximalUnramifiedSubextension

L54 ↗
AlgebraicNumberTheory.Valuations.maximalUnramifiedSubextension
Documentation

The maximal unramified subextension T/K of L/K.

The supremum is the field compositum. Indexing by finite unramified subextensions is literal the finite unramified-extension definition: every arbitrary unramified subextension is their union.

Source context 5 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
section MaximalUnramifiedSubextension
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
def maximalUnramifiedSubextension
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) :
    IntermediateField K L
theorem

finiteUnramifiedSubextension_le_maximal

L62 ↗
AlgebraicNumberTheory.Valuations.finiteUnramifiedSubextension_le_maximal
Documentation

Every finite unramified subextension is contained in T.

Source context 5 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
section MaximalUnramifiedSubextension
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem finiteUnramifiedSubextension_le_maximal
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    {E : IntermediateField K L}
    (hE : FiniteUnramifiedSubextension v w hExt E) :
    E ≤ maximalUnramifiedSubextension v w hExt
theorem

maximalUnramifiedSubextension_le

L74 ↗
AlgebraicNumberTheory.Valuations.maximalUnramifiedSubextension_le
Documentation

T is the least intermediate field containing every finite unramified subextension.

Source context 5 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
section MaximalUnramifiedSubextension
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem maximalUnramifiedSubextension_le
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    {M : IntermediateField K L}
    (hM : ∀ E : IntermediateField K L,
      FiniteUnramifiedSubextension v w hExt E → E ≤ M) :
    maximalUnramifiedSubextension v w hExt ≤ M
theorem

maximalUnramifiedSubextension_le_iff

L87 ↗
AlgebraicNumberTheory.Valuations.maximalUnramifiedSubextension_le_iff
Documentation

The least-upper-bound characterization of the maximal-unramified-subextension definition.

Source context 5 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
section MaximalUnramifiedSubextension
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem maximalUnramifiedSubextension_le_iff
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    {M : IntermediateField K L} :
    maximalUnramifiedSubextension v w hExt ≤ M ↔
      ∀ E : IntermediateField K L,
        FiniteUnramifiedSubextension v w hExt E → E ≤ M

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.