NYLL
Module

ResidueCharacteristic.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.ValuedExtension.ResidueCharacteristic
7 declarations indexed from sourceView source ↗

Module documentation

Residue characteristic lemmas for tame ramification

This file records the elementary residue-characteristic facts needed for tower and base-change forms of the tame Abhyankar lemma. The key point is that the residue characteristic is unchanged along a valued-field extension, so "prime to the residue characteristic" can be transported through the residue-field algebra induced by the extension.

Imports1
Imported by3

Declarations

theorem

of_dvd

L30 ↗
ValuationTheory.DiscreteValuationField.DVF.PrimeToResidueCharacteristic.of_dvd
Documentation

Being prime to the residue characteristic is inherited by divisors.

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_dvd
    {F : DVF.{u, v} K} {m n : ℕ}
    (hn : F.PrimeToResidueCharacteristic n) (hmn : m ∣ n) :
    F.PrimeToResidueCharacteristic m
theorem

mul

L43 ↗
ValuationTheory.DiscreteValuationField.DVF.PrimeToResidueCharacteristic.mul
Documentation

The product of two numbers prime to the residue characteristic is again prime to the residue characteristic.

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.mul
    {F : DVF.{u, v} K} {m n : ℕ}
    (hm : F.PrimeToResidueCharacteristic m)
    (hn : F.PrimeToResidueCharacteristic n) :
    F.PrimeToResidueCharacteristic (m * n)
theorem

primeToResidueCharacteristic_mul_iff

L59 ↗
ValuationTheory.DiscreteValuationField.DVF.primeToResidueCharacteristic_mul_iff
Documentation

A product is prime to the residue characteristic exactly when both factors are.

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_mul_iff
    (F : DVF.{u, v} K) {m n : ℕ} :
    F.PrimeToResidueCharacteristic (m * n) ↔
      F.PrimeToResidueCharacteristic m ∧
        F.PrimeToResidueCharacteristic n
theorem

residueCharacteristic_eq_of_hasExtension

L78 ↗
ValuationTheory.DiscreteValuationField.DVF.residueCharacteristic_eq_of_hasExtension
Documentation

The residue characteristic is unchanged by a valued-field extension.

Source context 9 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]
variable {L : Type w} [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 residueCharacteristic_eq_of_hasExtension :
    target.residueCharacteristic = base.residueCharacteristic
theorem

primeToResidueCharacteristic_target_iff

L86 ↗
ValuationTheory.DiscreteValuationField.DVF.primeToResidueCharacteristic_target_iff
Documentation

Along a valued-field extension, the prime-to-residue-characteristic condition may be checked on either residue field.

Source context 9 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]
variable {L : Type w} [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 primeToResidueCharacteristic_target_iff {n : ℕ} :
    target.PrimeToResidueCharacteristic n ↔
      base.PrimeToResidueCharacteristic n
theorem

primeToResidueCharacteristic_of_target

L95 ↗
ValuationTheory.DiscreteValuationField.DVF.primeToResidueCharacteristic_of_target
Documentation

Transport a prime-to-residue-characteristic statement from the target residue field to the base residue field.

Source context 9 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]
variable {L : Type w} [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 primeToResidueCharacteristic_of_target {n : ℕ}
    (hn : target.PrimeToResidueCharacteristic n) :
    base.PrimeToResidueCharacteristic n
theorem

primeToResidueCharacteristic_to_target

L102 ↗
ValuationTheory.DiscreteValuationField.DVF.primeToResidueCharacteristic_to_target
Documentation

Transport a prime-to-residue-characteristic statement from the base residue field to the target residue field.

Source context 9 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]
variable {L : Type w} [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 primeToResidueCharacteristic_to_target {n : ℕ}
    (hn : base.PrimeToResidueCharacteristic n) :
    target.PrimeToResidueCharacteristic n

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