NYLL
Module

Basic.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.Basic
21 declarations indexed from sourceView source ↗

Module documentation

Tame ramification predicates

This file defines tame ramification directly for the ambient valued extension base / target. No proof-irrelevant extension record is introduced: complete and Henselian discretely valued fields use the same definitions through their canonical toDVF projections.

Imports1
Imported by4

Declarations

def

residueCharacteristic

L30 ↗
ValuationTheory.DiscreteValuationField.DVF.residueCharacteristic
Documentation

The residue characteristic of a discretely valued field, expressed as 0 in characteristic zero and as the positive prime characteristic otherwise.

Source context 5 commands

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

noncomputable section
universe u v w x
namespace ValuationTheory.DiscreteValuationField
namespace DVF
variable {K : Type u} [Field K]
Lean source · statement
def residueCharacteristic (F : DVF.{u, v} K) : ℕ
theorem

residueCharacteristic_eq_ringChar

L33 ↗
ValuationTheory.DiscreteValuationField.DVF.residueCharacteristic_eq_ringChar
Source context 5 commands

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

noncomputable section
universe u v w x
namespace ValuationTheory.DiscreteValuationField
namespace DVF
variable {K : Type u} [Field K]
Lean source · statement
theorem residueCharacteristic_eq_ringChar (F : DVF.{u, v} K) :
    F.residueCharacteristic = ringChar F.residueField
def

PrimeToResidueCharacteristic

L39 ↗
ValuationTheory.DiscreteValuationField.DVF.PrimeToResidueCharacteristic
Documentation

A natural number is prime to the residue characteristic. In residue characteristic zero this condition is vacuous.

Source context 5 commands

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

noncomputable section
universe u v w x
namespace ValuationTheory.DiscreteValuationField
namespace DVF
variable {K : Type u} [Field K]
Lean source · statement
def PrimeToResidueCharacteristic (F : DVF.{u, v} K) (n : ℕ) : Prop
theorem

primeToResidueCharacteristic_of_residueCharacteristic_eq_zero

L42 ↗
ValuationTheory.DiscreteValuationField.DVF.primeToResidueCharacteristic_of_residueCharacteristic_eq_zero
Source context 5 commands

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

noncomputable section
universe u v w x
namespace ValuationTheory.DiscreteValuationField
namespace DVF
variable {K : Type u} [Field K]
Lean source · statement
theorem primeToResidueCharacteristic_of_residueCharacteristic_eq_zero
    (F : DVF.{u, v} K) {n : ℕ}
    (hchar : F.residueCharacteristic = 0) :
    F.PrimeToResidueCharacteristic n
theorem

primeToResidueCharacteristic_iff_of_residueCharacteristic_ne_zero

L48 ↗
ValuationTheory.DiscreteValuationField.DVF.primeToResidueCharacteristic_iff_of_residueCharacteristic_ne_zero
Source context 5 commands

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

noncomputable section
universe u v w x
namespace ValuationTheory.DiscreteValuationField
namespace DVF
variable {K : Type u} [Field K]
Lean source · statement
theorem primeToResidueCharacteristic_iff_of_residueCharacteristic_ne_zero
    (F : DVF.{u, v} K) {n : ℕ}
    (hchar : F.residueCharacteristic ≠ 0) :
    F.PrimeToResidueCharacteristic n ↔
      Nat.Coprime n F.residueCharacteristic
theorem

residueCharacteristic_coprime_of_primeToResidueCharacteristic

L58 ↗
ValuationTheory.DiscreteValuationField.DVF.residueCharacteristic_coprime_of_primeToResidueCharacteristic
Source context 5 commands

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

noncomputable section
universe u v w x
namespace ValuationTheory.DiscreteValuationField
namespace DVF
variable {K : Type u} [Field K]
Lean source · statement
theorem residueCharacteristic_coprime_of_primeToResidueCharacteristic
    (F : DVF.{u, v} K) {n : ℕ}
    (hchar : F.residueCharacteristic ≠ 0)
    (hn : F.PrimeToResidueCharacteristic n) :
    Nat.Coprime n F.residueCharacteristic
theorem

primeToResidueCharacteristic_one

L65 ↗
ValuationTheory.DiscreteValuationField.DVF.primeToResidueCharacteristic_one
Source context 5 commands

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

noncomputable section
universe u v w x
namespace ValuationTheory.DiscreteValuationField
namespace DVF
variable {K : Type u} [Field K]
Lean source · statement
theorem primeToResidueCharacteristic_one (F : DVF.{u, v} K) :
    F.PrimeToResidueCharacteristic 1
def

IsTamelyRamified

L83 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.IsTamelyRamified
Documentation

A finite valued extension is tamely ramified when it is defectless, its residue-field extension is separable, and its ramification index is prime to the residue characteristic.

Source context 8 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]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
def IsTamelyRamified : Prop
theorem

isTamelyRamified_def

L88 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.isTamelyRamified_def
Source context 8 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]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem isTamelyRamified_def :
    IsTamelyRamified base target ↔
      IsDefectless base target ∧
        Algebra.IsSeparable base.residueField target.residueField ∧
          base.PrimeToResidueCharacteristic (ramificationIndex base target)
theorem

isDefectless

L95 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.IsTamelyRamified.isDefectless
Source context 8 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]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem IsTamelyRamified.isDefectless
    (hE : IsTamelyRamified base target) :
    IsDefectless base target
theorem

residue_isSeparable

L100 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.IsTamelyRamified.residue_isSeparable
Source context 8 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]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem IsTamelyRamified.residue_isSeparable
    (hE : IsTamelyRamified base target) :
    Algebra.IsSeparable base.residueField target.residueField
theorem

primeToResidueCharacteristic

L105 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.IsTamelyRamified.primeToResidueCharacteristic
Source context 8 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]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem IsTamelyRamified.primeToResidueCharacteristic
    (hE : IsTamelyRamified base target) :
    base.PrimeToResidueCharacteristic (ramificationIndex base target)
theorem

ramificationIndex_coprime_residueCharacteristic

L110 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.IsTamelyRamified.ramificationIndex_coprime_residueCharacteristic
Source context 8 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]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem IsTamelyRamified.ramificationIndex_coprime_residueCharacteristic
    (hE : IsTamelyRamified base target)
    (hchar : base.residueCharacteristic ≠ 0) :
    Nat.Coprime (ramificationIndex base target) base.residueCharacteristic
theorem

isTamelyRamified_of_isUnramified_of_isDefectless_of_residue_isSeparable

L117 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.isTamelyRamified_of_isUnramified_of_isDefectless_of_residue_isSeparable
Source context 8 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]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem isTamelyRamified_of_isUnramified_of_isDefectless_of_residue_isSeparable
    (hun : IsUnramified base target)
    (hdef : IsDefectless base target)
    (hres : Algebra.IsSeparable base.residueField target.residueField) :
    IsTamelyRamified base target
theorem

degree_eq_ramificationIndex_mul_residueDegree

L126 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.IsTamelyRamified.degree_eq_ramificationIndex_mul_residueDegree
Source context 8 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]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem IsTamelyRamified.degree_eq_ramificationIndex_mul_residueDegree
    (hE : IsTamelyRamified base target) :
    degree base target = ramificationIndex base target * residueDegree base target
def

IsTotallyTamelyRamified

L132 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.IsTotallyTamelyRamified
Documentation

Totally tamely ramified means tame and residue degree one.

Source context 8 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]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
def IsTotallyTamelyRamified : Prop
theorem

isTotallyTamelyRamified_def

L135 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.isTotallyTamelyRamified_def
Source context 8 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]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem isTotallyTamelyRamified_def :
    IsTotallyTamelyRamified base target ↔
      IsTamelyRamified base target ∧ IsTotallyRamified base target
theorem

isTamelyRamified

L140 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.IsTotallyTamelyRamified.isTamelyRamified
Source context 8 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]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem IsTotallyTamelyRamified.isTamelyRamified
    (hE : IsTotallyTamelyRamified base target) :
    IsTamelyRamified base target
theorem

isTotallyRamified

L145 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.IsTotallyTamelyRamified.isTotallyRamified
Source context 8 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]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem IsTotallyTamelyRamified.isTotallyRamified
    (hE : IsTotallyTamelyRamified base target) :
    IsTotallyRamified base target
theorem

ramificationIndex_eq_degree

L150 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.IsTotallyTamelyRamified.ramificationIndex_eq_degree
Source context 8 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]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem IsTotallyTamelyRamified.ramificationIndex_eq_degree
    (hE : IsTotallyTamelyRamified base target) :
    ramificationIndex base target = degree base target
theorem

primeToResidueCharacteristic_degree

L156 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.IsTotallyTamelyRamified.primeToResidueCharacteristic_degree
Source context 8 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]
variable (base : DVF.{u, v} K) (target : DVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem IsTotallyTamelyRamified.primeToResidueCharacteristic_degree
    (hE : IsTotallyTamelyRamified base target) :
    base.PrimeToResidueCharacteristic (degree base target)

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