NYLL
Module

Canonical.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValuedExtension.Canonical
11 declarations indexed from sourceView source ↗

Module documentation

Tame predicates for finite separable valued extensions

For a finite separable extension of complete discretely valued fields, the ambient valued extension is defectless. Consequently tameness is controlled directly by residue separability and the ramification index; no auxiliary extension record or canonicalization constructor is needed.

The final section compares this canonical API with Neu1999's exponential- valuation presentation when both presentations determine the same valuation subrings.

Imports32
Imported by3

Declarations

theorem

ramificationIndex_dvd_degree_of_finite_separable

L69 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex_dvd_degree_of_finite_separable
Documentation

In a finite separable extension, the ramification index divides the field degree.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
variable [Algebra.IsSeparable K L]
variable [IsScalarTower base.valuationSubring target.valuationSubring L]
Lean source · statement
theorem ramificationIndex_dvd_degree_of_finite_separable :
    ramificationIndex base.toDVF target.toDVF ∣
      degree base.toDVF target.toDVF
theorem

isTamelyRamified_iff_of_finite_separable

L81 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.isTamelyRamified_iff_of_finite_separable
Documentation

For a finite separable valued extension, tameness is exactly residue separability together with the prime-to-residue-characteristic condition on the ramification index.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
variable [Algebra.IsSeparable K L]
variable [IsScalarTower base.valuationSubring target.valuationSubring L]
Lean source · statement
theorem isTamelyRamified_iff_of_finite_separable :
    IsTamelyRamified base.toDVF target.toDVF ↔
      Algebra.IsSeparable base.residueField target.residueField ∧
        base.toDVF.PrimeToResidueCharacteristic
          (ramificationIndex base.toDVF target.toDVF)
theorem

isTamelyRamified_of_residue_isSeparable_of_primeTo_ramificationIndex

L97 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.isTamelyRamified_of_residue_isSeparable_of_primeTo_ramificationIndex
Documentation

Residue separability and the prime-to condition on the ramification index imply tameness for a finite separable valued extension.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
variable [Algebra.IsSeparable K L]
variable [IsScalarTower base.valuationSubring target.valuationSubring L]
Lean source · statement
theorem isTamelyRamified_of_residue_isSeparable_of_primeTo_ramificationIndex
    (hres : Algebra.IsSeparable base.residueField target.residueField)
    (hprime :
      base.toDVF.PrimeToResidueCharacteristic
        (ramificationIndex base.toDVF target.toDVF)) :
    IsTamelyRamified base.toDVF target.toDVF
theorem

isTamelyRamified_of_residue_isSeparable_of_primeTo_degree

L107 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.isTamelyRamified_of_residue_isSeparable_of_primeTo_degree
Documentation

A prime-to condition on the field degree implies the corresponding condition on the ramification index and hence tameness.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
variable [Algebra.IsSeparable K L]
variable [IsScalarTower base.valuationSubring target.valuationSubring L]
Lean source · statement
theorem isTamelyRamified_of_residue_isSeparable_of_primeTo_degree
    (hres : Algebra.IsSeparable base.residueField target.residueField)
    (hprime :
      base.toDVF.PrimeToResidueCharacteristic
        (degree base.toDVF target.toDVF)) :
    IsTamelyRamified base.toDVF target.toDVF
theorem

isTamelyRamified_of_isUnramified_of_residue_isSeparable

L120 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.isTamelyRamified_of_isUnramified_of_residue_isSeparable
Documentation

An unramified finite separable valued extension with separable residue extension is tame.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
variable [Algebra.IsSeparable K L]
variable [IsScalarTower base.valuationSubring target.valuationSubring L]
Lean source · statement
theorem isTamelyRamified_of_isUnramified_of_residue_isSeparable
    (hun : IsUnramified base.toDVF target.toDVF)
    (hres : Algebra.IsSeparable base.residueField target.residueField) :
    IsTamelyRamified base.toDVF target.toDVF
theorem

isTotallyTamelyRamified_iff_of_finite_separable

L133 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.isTotallyTamelyRamified_iff_of_finite_separable
Documentation

Total tame ramification of a finite separable valued extension is residue separability, the prime-to condition on the ramification index, and residue degree one.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
variable [Algebra.IsSeparable K L]
variable [IsScalarTower base.valuationSubring target.valuationSubring L]
Lean source · statement
theorem isTotallyTamelyRamified_iff_of_finite_separable :
    IsTotallyTamelyRamified base.toDVF target.toDVF ↔
      Algebra.IsSeparable base.residueField target.residueField ∧
        base.toDVF.PrimeToResidueCharacteristic
          (ramificationIndex base.toDVF target.toDVF) ∧
        residueDegree base.toDVF target.toDVF = 1
theorem

isTotallyTamelyRamified_iff_primeTo_degree_of_finite_separable

L152 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.isTotallyTamelyRamified_iff_primeTo_degree_of_finite_separable
Documentation

Degree form of the total-tameness criterion.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
variable [Algebra.IsSeparable K L]
variable [IsScalarTower base.valuationSubring target.valuationSubring L]
Lean source · statement
theorem isTotallyTamelyRamified_iff_primeTo_degree_of_finite_separable :
    IsTotallyTamelyRamified base.toDVF target.toDVF ↔
      Algebra.IsSeparable base.residueField target.residueField ∧
        base.toDVF.PrimeToResidueCharacteristic
          (degree base.toDVF target.toDVF) ∧
        residueDegree base.toDVF target.toDVF = 1
theorem

isTotallyTamelyRamified_of_residue_isSeparable_of_primeTo_ramificationIndex_of_residueDegree_eq_one

L175 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.isTotallyTamelyRamified_of_residue_isSeparable_of_primeTo_ramificationIndex_of_residueDegree_eq_one
Documentation

Introduction form of the direct total-tameness criterion.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
variable [Algebra.IsSeparable K L]
variable [IsScalarTower base.valuationSubring target.valuationSubring L]
Lean source · statement
theorem
 isTotallyTamelyRamified_of_residue_isSeparable_of_primeTo_ramificationIndex_of_residueDegree_eq_one
    (hres : Algebra.IsSeparable base.residueField target.residueField)
    (hprime :
      base.toDVF.PrimeToResidueCharacteristic
        (ramificationIndex base.toDVF target.toDVF))
    (hf : residueDegree base.toDVF target.toDVF = 1) :
    IsTotallyTamelyRamified base.toDVF target.toDVF
theorem

isTotallyTamelyRamified_of_residue_isSeparable_of_primeTo_degree_of_residueDegree_eq_one

L187 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.isTotallyTamelyRamified_of_residue_isSeparable_of_primeTo_degree_of_residueDegree_eq_one
Documentation

Introduction form of the degree-based total-tameness criterion.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace ValuationTheory.DiscreteValuationField
namespace ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
variable [Algebra.IsSeparable K L]
variable [IsScalarTower base.valuationSubring target.valuationSubring L]
Lean source · statement
theorem isTotallyTamelyRamified_of_residue_isSeparable_of_primeTo_degree_of_residueDegree_eq_one
    (hres : Algebra.IsSeparable base.residueField target.residueField)
    (hprime :
      base.toDVF.PrimeToResidueCharacteristic
        (degree base.toDVF target.toDVF))
    (hf : residueDegree base.toDVF target.toDVF = 1) :
    IsTotallyTamelyRamified base.toDVF target.toDVF
theorem

residue_isSeparable_of_bookFiniteTame

L204 ↗
TameAbhyankar.residue_isSeparable_of_bookFiniteTame
Source context 4 commands

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

noncomputable section
universe u v w x
namespace TameAbhyankar
open AlgebraicNumberTheory.Valuations
Lean source · statement
theorem residue_isSeparable_of_bookFiniteTame
    {K : Type u} {L : Type u} [Field K] [Field L]
    [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    {base : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K}
    {target : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, x} L}
    [base.valuation.HasExtension target.valuation]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (vK : LubinTate.Valuations.ExponentialValuation K)
    (vL : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, vL (algebraMap K L a) = vK a)
    (hTame : FiniteTamelyRamifiedExtension vK vL hExt)
    (hV : LubinTate.Valuations.exponentialValuationSubringAsValuationSubring vK =
      base.valuation.valuationSubring)
    (hW : LubinTate.Valuations.exponentialValuationSubringAsValuationSubring vL =
      target.valuation.valuationSubring) :
    Algebra.IsSeparable base.residueField target.residueField
theorem

isTamelyRamified_of_bookFiniteTame

L265 ↗
TameAbhyankar.isTamelyRamified_of_bookFiniteTame
Documentation

A finite tame extension in the exponential-valuation (book) presentation is tame for the complete-DVF valued extension, provided the book and CompleteDVF valuation rings are the same.

The proof transports the two residue fields through residue-field ring equivalences, compares the local ramification indices through the induced ring equivalences, and transports the residue characteristic by ringChar.

Source context 4 commands

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

noncomputable section
universe u v w x
namespace TameAbhyankar
open AlgebraicNumberTheory.Valuations
Lean source · statement
theorem isTamelyRamified_of_bookFiniteTame
    {K : Type u} {L : Type u} [Field K] [Field L]
    [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    {base : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K}
    {target : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, x} L}
    [base.valuation.HasExtension target.valuation]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    (vK : LubinTate.Valuations.ExponentialValuation K)
    (vL : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, vL (algebraMap K L a) = vK a)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring vK).valuation)
    (hTame : FiniteTamelyRamifiedExtension vK vL hExt)
    (hV : LubinTate.Valuations.exponentialValuationSubringAsValuationSubring vK =
      base.valuation.valuationSubring)
    (hW : LubinTate.Valuations.exponentialValuationSubringAsValuationSubring vL =
      target.valuation.valuationSubring) :
    ValuationTheory.DiscreteValuationField.ValuedExtension.IsTamelyRamified
      base.toDVF target.toDVF

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