NYLL
Module

ProlongationDiscrete.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.ProlongationDiscrete
3 declarations indexed from sourceView source ↗

Module documentation

Discrete prolongations to finite separable extensions

Finite separable field extensions carry discrete prolongations of the original valuation. These can use the original value-group universe and preserve the residue characteristic.

Imports6
Imported by6

Declarations

theorem

isRankOneDiscrete_of_finite_separable

L28 ↗
ValuationTheory.DiscreteValuationField.DVF.isRankOneDiscrete_of_finite_separable
Documentation

Every prolongation to a finite separable extension remains discrete of rank one. The integral closure localized at the prolongation's center supplies its DVR.

Source context 2 commands

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

namespace ValuationTheory.DiscreteValuationField
universe u v w z
Lean source · statement
theorem DVF.isRankOneDiscrete_of_finite_separable
    {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (base : DVF.{u, v} K) {Γ : Type z} [LinearOrderedCommGroupWithZero Γ]
    (vL : _root_.Valuation L Γ) [base.valuation.HasExtension vL] :
    vL.IsRankOneDiscrete
theorem

exists_extension_on_valueGroup

L95 ↗
ValuationTheory.DiscreteValuationField.DVF.exists_extension_on_valueGroup
Documentation

A finite separable extension admits a discrete valuation in the original value-group universe.

Source context 2 commands

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

namespace ValuationTheory.DiscreteValuationField
universe u v w z
Lean source · statement
theorem DVF.exists_extension_on_valueGroup
    {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (base : DVF.{u, v} K) :
    ∃ vL : _root_.Valuation L base.ValueGroup,
      vL.IsRankOneDiscrete ∧ base.valuation.HasExtension vL
theorem

exists_extension_residueChar

L126 ↗
ValuationTheory.DiscreteValuationField.DVF.exists_extension_residueChar
Documentation

A finite separable extension carries a discrete prolongation with the same residue characteristic.

Source context 2 commands

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

namespace ValuationTheory.DiscreteValuationField
universe u v w z
Lean source · statement
theorem DVF.exists_extension_residueChar
    {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (base : DVF.{u, v} K) (p : ℕ) [CharP base.residueField p] :
    ∃ target : DVF.{w,v} L, base.valuation.HasExtension target.valuation ∧
      CharP target.residueField p

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