NYLL
Module

Definitions.lean

Nyll.SchemeTheory.AbhyankarLemma.Kummer.Definitions
9 declarations indexed from sourceView source ↗

Module documentation

Tame ramification for algebraic valued extensions

Suppose that the residue characteristic p = char(kappa) is positive. An algebraic valued extension L/K is tamely ramified when its residue extension is separable and [L : T] is prime to p, where T/K is the maximal unramified subextension. For an infinite extension, the degree condition means that every finite intermediate extension of L/T has degree prime to p.

The definitions below use the characteristic of the actual residue field of the valuation on K; there is no independent natural-number parameter that could be filled by an unrelated prime.

Imports2
Imported by2

Declarations

def

residueCharacteristic

L38 ↗
AlgebraicNumberTheory.Valuations.residueCharacteristic
Documentation

The actual residue characteristic p = char(kappa) used in the tame ramification predicate.

Source context 6 commands

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

noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
section TamelyRamifiedExtensions
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
def residueCharacteristic (v : LubinTate.Valuations.ExponentialValuation K) : ℕ
def

PositiveResidueCharacteristic

L43 ↗
AlgebraicNumberTheory.Valuations.PositiveResidueCharacteristic
Documentation

Positive residue characteristic is exactly the nonvanishing of the actual residue characteristic.

Source context 6 commands

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

noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
section TamelyRamifiedExtensions
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
def PositiveResidueCharacteristic
    (v : LubinTate.Valuations.ExponentialValuation K) : Prop
theorem

residueCharacteristic_prime

L50 ↗
AlgebraicNumberTheory.Valuations.residueCharacteristic_prime
Documentation

In positive residue characteristic, the actual residue characteristic is prime. Thus later uses may obtain Fact p.Prime from the positivity clause of the tame-ramification predicate rather than assume an unrelated certificate.

Source context 6 commands

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

noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
section TamelyRamifiedExtensions
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem residueCharacteristic_prime
    (v : LubinTate.Valuations.ExponentialValuation K)
    (hp : PositiveResidueCharacteristic v) :
    Nat.Prime (residueCharacteristic v)
theorem

residueCharacteristicPrimeFact

L60 ↗
AlgebraicNumberTheory.Valuations.residueCharacteristicPrimeFact
Documentation

A Fact form of residueCharacteristic_prime, for APIs which take primality through typeclass inference.

Source context 6 commands

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

noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
section TamelyRamifiedExtensions
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem residueCharacteristicPrimeFact
    (v : LubinTate.Valuations.ExponentialValuation K)
    (hp : PositiveResidueCharacteristic v) :
    Fact (Nat.Prime (residueCharacteristic v))
def

FiniteSubextensionDegreesPrimeTo

L71 ↗
AlgebraicNumberTheory.Valuations.FiniteSubextensionDegreesPrimeTo
Documentation

The infinite-degree clause for tame ramification: every finite intermediate extension of L/T has degree prime to p.

Finiteness is supplied by the quantified datum hE; it is not an ambient finite-dimensionality assumption hidden in the definition.

Source context 6 commands

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

noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
section TamelyRamifiedExtensions
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
def FiniteSubextensionDegreesPrimeTo
    (T : IntermediateField K L) (p : ℕ) : Prop
theorem

finiteSubextensionDegreesPrimeTo_iff

L79 ↗
AlgebraicNumberTheory.Valuations.finiteSubextensionDegreesPrimeTo_iff
Documentation

For a finite ambient extension, the infinite-extension clause is equivalent to the single condition that [L : T] is prime to p.

Source context 6 commands

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

noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
section TamelyRamifiedExtensions
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem finiteSubextensionDegreesPrimeTo_iff
    [FiniteDimensional K L]
    (T : IntermediateField K L) (p : ℕ) :
    FiniteSubextensionDegreesPrimeTo T p ↔
      Nat.Coprime (Module.finrank T L) p
def

FiniteTamelyRamifiedExtension

L104 ↗
AlgebraicNumberTheory.Valuations.FiniteTamelyRamifiedExtension
Documentation

Tame ramification for a finite extension.

Here T is the actual maximal unramified subextension and p is the actual residue characteristic of K. The positivity clause records the standing condition p > 0; under that clause the two remaining conjuncts are exactly residue separability and ([L : T], p) = 1.

Source context 6 commands

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

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

AlgebraicTamelyRamifiedExtension

L120 ↗
AlgebraicNumberTheory.Valuations.AlgebraicTamelyRamifiedExtension
Documentation

Tame ramification for an arbitrary algebraic extension.

The finite-degree clause requires every finite intermediate extension of L/T has degree prime to the actual positive residue characteristic.

Source context 6 commands

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

noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
section TamelyRamifiedExtensions
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
def AlgebraicTamelyRamifiedExtension
    [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

finiteTamelyRamifiedExtension_iff_algebraic

L133 ↗
AlgebraicNumberTheory.Valuations.finiteTamelyRamifiedExtension_iff_algebraic
Documentation

On finite extensions the finite and arbitrary-algebraic tame-ramification predicates agree.

Source context 6 commands

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

noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
section TamelyRamifiedExtensions
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem finiteTamelyRamifiedExtension_iff_algebraic
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) :
    FiniteTamelyRamifiedExtension v w hExt ↔
      AlgebraicTamelyRamifiedExtension 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.