Module

ImmediateExtensions.lean

Nyll.SchemeTheory.AbhyankarLemma.Kummer.ImmediateExtensions

7 declarations indexed from sourceView source ↗

Module documentation

The immediate prime-to-p step in tame ramification

This file develops the primary-reduction calculation used in the trace argument: a monic polynomial whose reduction admits no nontrivial coprime factorization and has a residue root is a pure power of the corresponding linear factor.

Imports2

Imported by2

theorem

monic_eq_X_sub_C_pow_natDegree_of_primary_of_isRoot

L29 ↗

AlgebraicNumberTheory.Valuations.monic_eq_X_sub_C_pow_natDegree_of_primary_of_isRoot

Documentation

A monic primary polynomial over a field which has a root is the full power of that root's linear factor.

Source context 4 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem monic_eq_X_sub_C_pow_natDegree_of_primary_of_isRoot
    {k : Type*} [Field k]
    (q : Polynomial k) (hqmonic : q.Monic)
    (hprimary : ∀ a b : Polynomial k,
      q = a * b → IsCoprime a b →
        a.natDegree = 0 ∨ b.natDegree = 0)
    (c : k) (hc : q.IsRoot c) :
    q = (Polynomial.X - Polynomial.C c) ^ q.natDegree

theorem

natCast_ne_zero_of_coprime_residueCharacteristic

L86 ↗

AlgebraicNumberTheory.Valuations.natCast_ne_zero_of_coprime_residueCharacteristic

Documentation

An integer prime to the positive residue characteristic remains nonzero in the valued field. This is the small characteristic argument used twice in the trace proof for an immediate prime-to-characteristic extension.

Source context 4 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem natCast_ne_zero_of_coprime_residueCharacteristic
    {K : Type*} [Field K]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (hp : PositiveResidueCharacteristic v)
    (m : ℕ)
    (hcop : Nat.Coprime m (residueCharacteristic v)) :
    (m : K) ≠ 0

theorem

minpoly_nextCoeff_eq_zero_of_trace_eq_zero_of_coprime

L121 ↗

AlgebraicNumberTheory.Valuations.minpoly_nextCoeff_eq_zero_of_trace_eq_zero_of_coprime

Documentation

In a finite extension of degree prime to the positive residue characteristic, trace zero forces the next coefficient of the minimal polynomial to vanish. The possible multiplicity coming from the ambient extension is again prime to the residue characteristic.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section TraceCentering
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]

Lean source · statement

theorem minpoly_nextCoeff_eq_zero_of_trace_eq_zero_of_coprime
    (v : LubinTate.Valuations.ExponentialValuation K)
    (hp : PositiveResidueCharacteristic v)
    (hdegree : Nat.Coprime (Module.finrank K L)
      (residueCharacteristic v))
    (x : L) (htrace : Algebra.trace K L x = 0) :
    (minpoly K x).nextCoeff = 0

theorem

exists_nonzero_trace_zero_of_not_mem_bot_of_coprime

L150 ↗

AlgebraicNumberTheory.Valuations.exists_nonzero_trace_zero_of_not_mem_bot_of_coprime

Documentation

Trace centering for an immediate prime-to-characteristic extension. If an element is not already in the base field, subtracting its normalized trace produces a nonzero element of trace zero.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section TraceCentering
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]

Lean source · statement

theorem exists_nonzero_trace_zero_of_not_mem_bot_of_coprime
    (v : LubinTate.Valuations.ExponentialValuation K)
    (hp : PositiveResidueCharacteristic v)
    (hdegree : Nat.Coprime (Module.finrank K L)
      (residueCharacteristic v))
    (alpha : L) (halpha : alpha ∉ (⊥ : IntermediateField K L)) :
    ∃ beta : L, beta ≠ 0 ∧ Algebra.trace K L beta = 0

def

tameResidueFieldMap

L184 ↗

AlgebraicNumberTheory.Valuations.tameResidueFieldMap

Documentation

The actual residue-field map attached to an exact extension of exponential valuations.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section ImmediateInvariants
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

def tameResidueFieldMap
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) :
    IsLocalRing.ResidueField (LubinTate.Valuations.exponentialValuationSubring v) →+*
      IsLocalRing.ResidueField (LubinTate.Valuations.exponentialValuationSubring w)

theorem

exists_base_element_value_eq_of_valueSubgroup_eq

L198 ↗

AlgebraicNumberTheory.Valuations.exists_base_element_value_eq_of_valueSubgroup_eq

Documentation

Equality of the actual value subgroups means that every nonzero target element has the value of a nonzero base element.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section ImmediateInvariants
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
omit [Algebra K L] in

Lean source · statement

theorem exists_base_element_value_eq_of_valueSubgroup_eq
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hvalue : exponentialValueSubgroup w =
      exponentialValueSubgroup v)
    (x : L) (hx : x ≠ 0) :
    ∃ b : K, b ≠ 0 ∧ v b = w x

theorem

finrank_eq_one_of_valueSubgroup_eq_of_residue_surjective_of_coprime

L229 ↗

AlgebraicNumberTheory.Valuations.finrank_eq_one_of_valueSubgroup_eq_of_residue_surjective_of_coprime

Documentation

The immediate prime-to-p lemma for tame ramification.

If the value groups agree, the residue map is onto, and the finite degree is prime to the positive residue characteristic, then the extension is trivial. The proof uses a trace argument and does not assume discreteness or a fundamental identity.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section ImmediatePrimeToP
variable {K L : Type u} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]

Lean source · statement

theorem finrank_eq_one_of_valueSubgroup_eq_of_residue_surjective_of_coprime
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation)
    (hp : PositiveResidueCharacteristic v)
    (hdegree : Nat.Coprime (Module.finrank K L)
      (residueCharacteristic v))
    (hvalue : exponentialValueSubgroup w =
      exponentialValueSubgroup v)
    (hresidue : Function.Surjective (tameResidueFieldMap v w hExt)) :
    Module.finrank K L = 1

Module documentation

The immediate prime-to-p step in tame ramification

Declarations

monic_eq_X_sub_C_pow_natDegree_of_primary_of_isRoot

natCast_ne_zero_of_coprime_residueCharacteristic

minpoly_nextCoeff_eq_zero_of_trace_eq_zero_of_coprime

exists_nonzero_trace_zero_of_not_mem_bot_of_coprime

tameResidueFieldMap

exists_base_element_value_eq_of_valueSubgroup_eq

finrank_eq_one_of_valueSubgroup_eq_of_residue_surjective_of_coprime