NYLL
Module

Definitions.lean

Nyll.ValuedFieldTheory.LocalField.Unramified.Definitions
21 declarations indexed from sourceView source ↗

Module documentation

Finite and algebraic unramified valued extensions

Finite unramified valued extensions are expressed directly by the degree equality and residue separability condition.

Imports2
Imported by5

Declarations

def

IsFiniteUnramified

L31 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.IsFiniteUnramified
Documentation

A finite valued extension is unramified when its residue extension is separable and its field degree equals its residue degree.

Source context 6 commands

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

noncomputable section
universe u v w x
open ValuationTheory.DiscreteValuationField
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
Lean source · statement
def IsFiniteUnramified (base : DVF.{u, v} K) (target : DVF.{w, x} L)
    [base.valuation.HasExtension target.valuation] : Prop
def

IsFiniteUnramifiedSubextension

L48 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.IsFiniteUnramifiedSubextension
Documentation

A finite unramified subextension of an ambient valued extension.

Source context 8 commands

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

noncomputable section
universe u v w x
open ValuationTheory.DiscreteValuationField
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
section AlgebraicUnramified
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (ambient : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension ambient.valuation]
Lean source · statement
def IsFiniteUnramifiedSubextension (E : IntermediateField K L) : Prop
def

IsAlgebraicUnramifiedExtension

L66 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.IsAlgebraicUnramifiedExtension
Documentation

An algebraic unramified ambient extension.

The ambient extension is unramified when every finite set of elements lies in one finite unramified intermediate extension. This is the finite-support form of the phrase "a union of finite unramified subextensions" and is the form used in finite-support reductions for algebraic unramified extensions.

Source context 8 commands

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

noncomputable section
universe u v w x
open ValuationTheory.DiscreteValuationField
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
section AlgebraicUnramified
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (ambient : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension ambient.valuation]
Lean source · statement
def IsAlgebraicUnramifiedExtension : Prop
theorem

exists_isFiniteUnramifiedSubextension_of_fg

L75 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.exists_isFiniteUnramifiedSubextension_of_fg
Source context 9 commands

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

noncomputable section
universe u v w x
open ValuationTheory.DiscreteValuationField
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
section AlgebraicUnramified
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (ambient : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension ambient.valuation]
omit [base.valuation.HasExtension ambient.valuation] in
Lean source · statement
theorem exists_isFiniteUnramifiedSubextension_of_fg
    (h : IsAlgebraicUnramifiedExtension base ambient)
    {E : IntermediateField K L} (hE : E.FG) :
    ∃ U : IntermediateField K L,
      E ≤ U ∧ IsFiniteUnramifiedSubextension base ambient U
def

exponentialValuationRestrict

L101 ↗
AlgebraicNumberTheory.Valuations.exponentialValuationRestrict
Documentation

Restriction of an exponential valuation to an intermediate field. This is the valuation carried by each finite subextension in the union clause of the finite unramified-extension definition.

Source context 7 commands

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

noncomputable section
universe u v w x
open ValuationTheory.DiscreteValuationField
namespace AlgebraicNumberTheory
namespace Valuations
section UnramifiedExtensions
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · full declaration
def exponentialValuationRestrict
    (w : LubinTate.Valuations.ExponentialValuation L) (E : IntermediateField K L) :
    LubinTate.Valuations.ExponentialValuation E where
  toFun x := w (x : L)
  eq_top_iff x := by
    rw [w.eq_top_iff]
    simp
  map_mul x y := by
    exact w.map_mul (x : L) (y : L)
  add_le_min x y := by
    exact w.add_le_min (x : L) (y : L)
theorem

exponentialValuationRestrict_apply

L114 ↗
AlgebraicNumberTheory.Valuations.exponentialValuationRestrict_apply
Source context 7 commands

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

noncomputable section
universe u v w x
open ValuationTheory.DiscreteValuationField
namespace AlgebraicNumberTheory
namespace Valuations
section UnramifiedExtensions
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem exponentialValuationRestrict_apply
    (w : LubinTate.Valuations.ExponentialValuation L) (E : IntermediateField K L) (x : E) :
    exponentialValuationRestrict w E x = w (x : L)
theorem

exponentialValuationRestrict_extends

L121 ↗
AlgebraicNumberTheory.Valuations.exponentialValuationRestrict_extends
Documentation

Exact extension is preserved when the target valuation is restricted to an intermediate field.

Source context 7 commands

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

noncomputable section
universe u v w x
open ValuationTheory.DiscreteValuationField
namespace AlgebraicNumberTheory
namespace Valuations
section UnramifiedExtensions
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem exponentialValuationRestrict_extends
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (E : IntermediateField K L) (a : K) :
    exponentialValuationRestrict w E (algebraMap K E a) = v a
def

unramifiedValuationRingValuationRingMap

L135 ↗
AlgebraicNumberTheory.Valuations.unramifiedValuationRingValuationRingMap
Documentation

The valuation-ring map associated with an exact extension of exponential exponential valuations. the fundamental inequality uses the same map internally; it is exposed here because the finite unramified-extension definition also asks for separability of the actual residue-field extension.

Source context 7 commands

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

noncomputable section
universe u v w x
open ValuationTheory.DiscreteValuationField
namespace AlgebraicNumberTheory
namespace Valuations
section UnramifiedExtensions
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
def unramifiedValuationRingValuationRingMap
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) :
    LubinTate.Valuations.exponentialValuationSubring v →+*
      LubinTate.Valuations.exponentialValuationSubring w
theorem

unramifiedValuationRingValuationRingMap_apply

L147 ↗
AlgebraicNumberTheory.Valuations.unramifiedValuationRingValuationRingMap_apply
Source context 7 commands

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

noncomputable section
universe u v w x
open ValuationTheory.DiscreteValuationField
namespace AlgebraicNumberTheory
namespace Valuations
section UnramifiedExtensions
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem unramifiedValuationRingValuationRingMap_apply
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (a : LubinTate.Valuations.exponentialValuationSubring v) :
    ((unramifiedValuationRingValuationRingMap v w hExt a :
      LubinTate.Valuations.exponentialValuationSubring w) : L) =
        algebraMap K L (a : K)
theorem

unramifiedValuationRingValuationRingMap_isLocalHom

L159 ↗
AlgebraicNumberTheory.Valuations.unramifiedValuationRingValuationRingMap_isLocalHom
Documentation

Exact extension makes the finite unramified-extension valuation-ring map local, hence it induces the actual map of residue fields used below.

Source context 7 commands

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

noncomputable section
universe u v w x
open ValuationTheory.DiscreteValuationField
namespace AlgebraicNumberTheory
namespace Valuations
section UnramifiedExtensions
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem unramifiedValuationRingValuationRingMap_isLocalHom
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) :
    IsLocalHom (unramifiedValuationRingValuationRingMap v w hExt)
def

ResidueExtensionIsSeparable

L177 ↗
AlgebraicNumberTheory.Valuations.ResidueExtensionIsSeparable
Documentation

Separability of the actual residue-field extension induced by an exact extension of exponential valuations.

Source context 7 commands

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

noncomputable section
universe u v w x
open ValuationTheory.DiscreteValuationField
namespace AlgebraicNumberTheory
namespace Valuations
section UnramifiedExtensions
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
def ResidueExtensionIsSeparable
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) : Prop
def

FiniteUnramifiedExtension

L200 ↗
AlgebraicNumberTheory.Valuations.FiniteUnramifiedExtension
Documentation

Literal finite-extension form for the general exponential valuations.

The first conjunct is separability of the actual residue-field extension. The second is exactly [L : K] = [lambda : kappa], with the right-hand side given by the actual residue finrank from the fundamental inequality. In particular no separability assumption on the field extension L/K is inserted.

Source context 7 commands

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

noncomputable section
universe u v w x
open ValuationTheory.DiscreteValuationField
namespace AlgebraicNumberTheory
namespace Valuations
section UnramifiedExtensions
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
def FiniteUnramifiedExtension
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) : Prop
theorem

finiteUnramifiedExtension_residue_isSeparable

L211 ↗
AlgebraicNumberTheory.Valuations.finiteUnramifiedExtension_residue_isSeparable
Documentation

Projection of residue separability in the literal finite the finite unramified-extension definition predicate.

Source context 7 commands

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

noncomputable section
universe u v w x
open ValuationTheory.DiscreteValuationField
namespace AlgebraicNumberTheory
namespace Valuations
section UnramifiedExtensions
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem finiteUnramifiedExtension_residue_isSeparable
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (h : FiniteUnramifiedExtension v w hExt) :
    ResidueExtensionIsSeparable v w hExt
theorem

finiteUnramifiedExtension_degree_eq_residueDegree

L223 ↗
AlgebraicNumberTheory.Valuations.finiteUnramifiedExtension_degree_eq_residueDegree
Documentation

Projection of the degree equality in the literal finite the finite unramified-extension definition predicate.

Source context 7 commands

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

noncomputable section
universe u v w x
open ValuationTheory.DiscreteValuationField
namespace AlgebraicNumberTheory
namespace Valuations
section UnramifiedExtensions
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem finiteUnramifiedExtension_degree_eq_residueDegree
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (h : FiniteUnramifiedExtension v w hExt) :
    Module.finrank K L = exponentialResidueDegree v w hExt
def

FiniteUnramifiedSubextension

L234 ↗
AlgebraicNumberTheory.Valuations.FiniteUnramifiedSubextension
Documentation

A finite intermediate extension is unramified when its restricted valuation satisfies the literal finite condition of the finite unramified-extension definition.

Source context 7 commands

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

noncomputable section
universe u v w x
open ValuationTheory.DiscreteValuationField
namespace AlgebraicNumberTheory
namespace Valuations
section UnramifiedExtensions
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
def FiniteUnramifiedSubextension
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (E : IntermediateField K L) : Prop
theorem

finiteDimensional_of_finiteUnramifiedSubextension

L248 ↗
AlgebraicNumberTheory.Valuations.finiteDimensional_of_finiteUnramifiedSubextension
Documentation

A finite unramified intermediate extension is finite-dimensional over the base field; this extracts the genuine finiteness datum from the finite unramified-extension definition.

Source context 7 commands

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

noncomputable section
universe u v w x
open ValuationTheory.DiscreteValuationField
namespace AlgebraicNumberTheory
namespace Valuations
section UnramifiedExtensions
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem finiteDimensional_of_finiteUnramifiedSubextension
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    {E : IntermediateField K L}
    (h : FiniteUnramifiedSubextension v w hExt E) :
    FiniteDimensional K E
def

finiteUnramifiedSubextensionUnion

L260 ↗
AlgebraicNumberTheory.Valuations.finiteUnramifiedSubextensionUnion
Documentation

The literal set-theoretic union of all finite unramified intermediate extensions.

Source context 7 commands

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

noncomputable section
universe u v w x
open ValuationTheory.DiscreteValuationField
namespace AlgebraicNumberTheory
namespace Valuations
section UnramifiedExtensions
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
def finiteUnramifiedSubextensionUnion
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) : Set L
def

AlgebraicUnramifiedExtension

L269 ↗
AlgebraicNumberTheory.Valuations.AlgebraicUnramifiedExtension
Documentation

Arbitrary algebraic-extension form: the ambient field is the union of its finite unramified subextensions.

Source context 7 commands

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

noncomputable section
universe u v w x
open ValuationTheory.DiscreteValuationField
namespace AlgebraicNumberTheory
namespace Valuations
section UnramifiedExtensions
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
def AlgebraicUnramifiedExtension
    [Algebra.IsAlgebraic K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) : Prop
theorem

algebraicUnramifiedExtension_iff

L277 ↗
AlgebraicNumberTheory.Valuations.algebraicUnramifiedExtension_iff
Documentation

Elementwise form of the finite-subextension union clause.

Source context 7 commands

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

noncomputable section
universe u v w x
open ValuationTheory.DiscreteValuationField
namespace AlgebraicNumberTheory
namespace Valuations
section UnramifiedExtensions
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem algebraicUnramifiedExtension_iff
    [Algebra.IsAlgebraic K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) :
    AlgebraicUnramifiedExtension v w hExt ↔
      ∀ x : L, ∃ E : IntermediateField K L,
        x ∈ E ∧ FiniteUnramifiedSubextension v w hExt E
def

AlgebraicUnramifiedExtensionFiniteSupport

L292 ↗
AlgebraicNumberTheory.Valuations.AlgebraicUnramifiedExtensionFiniteSupport
Documentation

Finite-support form used by the later base-change proof. It is kept separate from the literal union definition, so the finite unramified-extension definition itself does not silently assume closure of finite unramified extensions under compositum.

Source context 7 commands

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

noncomputable section
universe u v w x
open ValuationTheory.DiscreteValuationField
namespace AlgebraicNumberTheory
namespace Valuations
section UnramifiedExtensions
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
def AlgebraicUnramifiedExtensionFiniteSupport
    [Algebra.IsAlgebraic K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) : Prop
theorem

algebraicUnramifiedExtension_of_finiteSupport

L304 ↗
AlgebraicNumberTheory.Valuations.algebraicUnramifiedExtension_of_finiteSupport
Documentation

A finite-support presentation is, in particular, the literal union from the finite unramified-extension definition. The converse belongs after the compositum theorem rather than being built into the definition.

Source context 7 commands

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

noncomputable section
universe u v w x
open ValuationTheory.DiscreteValuationField
namespace AlgebraicNumberTheory
namespace Valuations
section UnramifiedExtensions
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem algebraicUnramifiedExtension_of_finiteSupport
    [Algebra.IsAlgebraic K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (h : AlgebraicUnramifiedExtensionFiniteSupport v w hExt) :
    AlgebraicUnramifiedExtension v w hExt

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