NYLL
Module

Monogeneity.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Monogeneity
15 declarations indexed from sourceView source ↗

Module documentation

Monogeneity over a noncomplete discretely valued field

This file proves the algebraic, noncomplete form of the monogeneity argument used in the monogenic integral-generator theorem. The proof uses the finite integral closure supplied by unique extension, a primitive residue element, the representative adjustment , and Nakayama's lemma.

Imports5
Imported by3

Declarations

theorem

map_maximalIdeal_eq_pow_ramificationIdx_dvf

L44 ↗
RamificationTheory.HilbertRamification.Higher.map_maximalIdeal_eq_pow_ramificationIdx_dvf
Documentation

A local injection of DVRs maps the source maximal ideal to the power of the target maximal ideal indexed by its ramification index.

Source context 13 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
namespace Higher
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem map_maximalIdeal_eq_pow_ramificationIdx_dvf :
    Ideal.map (algebraMap base.valuationSubring target.valuationSubring)
        base.maximalIdeal =
      target.maximalIdeal ^
        Ideal.ramificationIdx' base.maximalIdeal target.maximalIdeal
theorem

residueField_finiteDimensional_of_moduleFinite_dvf

L82 ↗
RamificationTheory.HilbertRamification.Higher.residueField_finiteDimensional_of_moduleFinite_dvf
Documentation

Module finiteness of the valuation-ring extension implies finiteness of the residue-field extension, without completeness.

Source context 13 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
namespace Higher
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem residueField_finiteDimensional_of_moduleFinite_dvf
    [Module.Finite base.valuationSubring target.valuationSubring] :
    FiniteDimensional base.residueField target.residueField
theorem

exists_base_polynomial_lift_residue_eq_dvf

L99 ↗
RamificationTheory.HilbertRamification.Higher.exists_base_polynomial_lift_residue_eq_dvf
Documentation

Lift a residue polynomial coefficientwise to the base valuation ring.

Source context 13 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
namespace Higher
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem exists_base_polynomial_lift_residue_eq_dvf
    (fbar : base.residueField[X]) :
    ∃ P : base.valuationSubring[X], P.map base.residueMap = fbar
theorem

base_polynomial_lift_target_reduction_eq_dvf

L107 ↗
RamificationTheory.HilbertRamification.Higher.base_polynomial_lift_target_reduction_eq_dvf
Documentation

Reduction after extension of coefficients agrees with extension after reduction.

Source context 13 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
namespace Higher
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem base_polynomial_lift_target_reduction_eq_dvf
    {P : base.valuationSubring[X]} {fbar : base.residueField[X]}
    (hP : P.map base.residueMap = fbar) :
    (P.map (algebraMap base.valuationSubring target.valuationSubring)).map
        target.residueMap =
      fbar.map (algebraMap base.residueField target.residueField)
theorem

polynomial_eval_mem_maximalIdeal_of_reduced_eval_eq_zero_dvf

L124 ↗
RamificationTheory.HilbertRamification.Higher.polynomial_eval_mem_maximalIdeal_of_reduced_eval_eq_zero_dvf
Documentation

A reduced polynomial root is an actual value in the maximal ideal.

Source context 13 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
namespace Higher
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem polynomial_eval_mem_maximalIdeal_of_reduced_eval_eq_zero_dvf
    {P : Polynomial target.valuationSubring} {a : target.valuationSubring}
    (hroot : (P.map target.residueMap).eval (target.residueMap a) = 0) :
    P.eval a ∈ target.maximalIdeal
theorem

polynomial_derivative_eval_isUnit_of_reduced_ne_zero_dvf

L139 ↗
RamificationTheory.HilbertRamification.Higher.polynomial_derivative_eval_isUnit_of_reduced_ne_zero_dvf
Documentation

A nonzero reduced derivative lifts to a unit derivative.

Source context 13 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
namespace Higher
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem polynomial_derivative_eval_isUnit_of_reduced_ne_zero_dvf
    {P : Polynomial target.valuationSubring} {a : target.valuationSubring}
    (hsimple :
      ((P.map target.residueMap).derivative).eval
        (target.residueMap a) ≠ 0) :
    IsUnit (P.derivative.eval a)
theorem

polynomial_eval_add_uniformizer_isUniformizer_dvf

L162 ↗
RamificationTheory.HilbertRamification.Higher.polynomial_eval_add_uniformizer_isUniformizer_dvf
Documentation

If a polynomial value is already in the square of the maximal ideal and the derivative is a unit, adding a uniformizer to the argument makes the polynomial value a uniformizer.

Source context 13 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
namespace Higher
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem polynomial_eval_add_uniformizer_isUniformizer_dvf
    {P : Polynomial target.valuationSubring}
    {a pi : target.valuationSubring}
    (hpi : target.valuation.IsUniformizer (pi : L))
    (hdeep : P.eval a ∈ target.maximalIdeal ^ 2)
    (hderiv : IsUnit (P.derivative.eval a)) :
    target.valuation.IsUniformizer
      ((P.eval (a + pi) : target.valuationSubring) : L)
theorem

exists_residue_eq_polynomial_eval_isUniformizer_dvf

L242 ↗
RamificationTheory.HilbertRamification.Higher.exists_residue_eq_polynomial_eval_isUniformizer_dvf
Documentation

Representative adjustment from the proof of the monogenic integral-generator theorem.

Source context 13 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
namespace Higher
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem exists_residue_eq_polynomial_eval_isUniformizer_dvf
    {P : Polynomial target.valuationSubring}
    {a pi : target.valuationSubring}
    (hpi : target.valuation.IsUniformizer (pi : L))
    (hP : P.eval a ∈ target.maximalIdeal)
    (hderiv : IsUnit (P.derivative.eval a)) :
    ∃ y : target.valuationSubring,
      target.residueMap y = target.residueMap a ∧
        target.valuation.IsUniformizer ((P.eval y : target.valuationSubring) : L)
theorem

base_polynomial_aeval_residue_eq_dvf

L266 ↗
RamificationTheory.HilbertRamification.Higher.base_polynomial_aeval_residue_eq_dvf
Documentation

Reducing a base-polynomial evaluation agrees with evaluating the reduced polynomial at the reduced argument.

Source context 13 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
namespace Higher
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem base_polynomial_aeval_residue_eq_dvf
    (P : base.valuationSubring[X]) (a : target.valuationSubring) :
    target.residueMap (Polynomial.aeval a P) =
      ((P.map base.residueMap).map
        (algebraMap base.residueField target.residueField)).eval
          (target.residueMap a)
theorem

exists_mem_adjoin_residue_eq_dvf

L295 ↗
RamificationTheory.HilbertRamification.Higher.exists_mem_adjoin_residue_eq_dvf
Documentation

Every residue class is represented in the algebra generated by a lift of a primitive residue element.

Source context 13 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
namespace Higher
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem exists_mem_adjoin_residue_eq_dvf
    [Algebra.IsAlgebraic base.residueField target.residueField]
    {a : target.valuationSubring}
    (hprim :
      IntermediateField.adjoin base.residueField
          ({target.residueMap a} : Set target.residueField) =
        (⊤ : IntermediateField base.residueField target.residueField))
    (zbar : target.residueField) :
    ∃ z : target.valuationSubring,
      z ∈ Algebra.adjoin base.valuationSubring
          ({a} : Set target.valuationSubring) ∧
        target.residueMap z = zbar
theorem

exists_mem_adjoin_sub_mem_maximalIdeal_dvf

L334 ↗
RamificationTheory.HilbertRamification.Higher.exists_mem_adjoin_sub_mem_maximalIdeal_dvf
Documentation

First-order approximation by the algebra generated by a primitive residue lift.

Source context 13 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
namespace Higher
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem exists_mem_adjoin_sub_mem_maximalIdeal_dvf
    [Algebra.IsAlgebraic base.residueField target.residueField]
    {a : target.valuationSubring}
    (hprim :
      IntermediateField.adjoin base.residueField
          ({target.residueMap a} : Set target.residueField) =
        (⊤ : IntermediateField base.residueField target.residueField))
    (z : target.valuationSubring) :
    ∃ y : target.valuationSubring,
      y ∈ Algebra.adjoin base.valuationSubring
          ({a} : Set target.valuationSubring) ∧
        z - y ∈ target.maximalIdeal
theorem

exists_mem_adjoin_sub_mem_maximalIdeal_pow_dvf

L356 ↗
RamificationTheory.HilbertRamification.Higher.exists_mem_adjoin_sub_mem_maximalIdeal_pow_dvf
Documentation

Approximation to arbitrary maximal-ideal order, using the fact that the lifted minimal polynomial evaluates to a target uniformizer.

Source context 13 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
namespace Higher
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem exists_mem_adjoin_sub_mem_maximalIdeal_pow_dvf
    [Algebra.IsAlgebraic base.residueField target.residueField]
    {P : base.valuationSubring[X]} {a : target.valuationSubring}
    (hprim :
      IntermediateField.adjoin base.residueField
          ({target.residueMap a} : Set target.residueField) =
        (⊤ : IntermediateField base.residueField target.residueField))
    (hpi :
      target.valuation.IsUniformizer
        (Polynomial.aeval a P : L))
    (n : ℕ) (z : target.valuationSubring) :
    ∃ y : target.valuationSubring,
      y ∈ Algebra.adjoin base.valuationSubring
          ({a} : Set target.valuationSubring) ∧
        z - y ∈ target.maximalIdeal ^ n
theorem

exists_primitive_residue_lift_polynomial_uniformizer_dvf

L415 ↗
RamificationTheory.HilbertRamification.Higher.exists_primitive_residue_lift_polynomial_uniformizer_dvf
Documentation

A primitive residue lift can be adjusted so that its lifted minimal polynomial value is a target uniformizer.

Source context 13 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
namespace Higher
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem exists_primitive_residue_lift_polynomial_uniformizer_dvf
    [FiniteDimensional base.residueField target.residueField]
    [Algebra.IsSeparable base.residueField target.residueField] :
    ∃ P : base.valuationSubring[X], ∃ a : target.valuationSubring,
      IntermediateField.adjoin base.residueField
          ({target.residueMap a} : Set target.residueField) =
        (⊤ : IntermediateField base.residueField target.residueField) ∧
      target.valuation.IsUniformizer (Polynomial.aeval a P : L) ∧
      IsUnit
        ((P.map
          (algebraMap base.valuationSubring target.valuationSubring)).derivative.eval a)
theorem

exists_valuationSubring_generator_data_of_uniqueExtension

L499 ↗
RamificationTheory.HilbertRamification.Higher.exists_valuationSubring_generator_data_of_uniqueExtension
Documentation

The full noncomplete generator data used by the monogenic integral-generator theorem and the first ramification-quotient homomorphism: a primitive residue lift, a lifted polynomial whose value is a uniformizer, its unit derivative, and generation of the entire target valuation ring.

Source context 12 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
namespace Higher
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
Lean source · statement
theorem exists_valuationSubring_generator_data_of_uniqueExtension
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    [Algebra.IsSeparable base.residueField target.residueField] :
    ∃ P : base.valuationSubring[X], ∃ a : target.valuationSubring,
      IntermediateField.adjoin base.residueField
          ({target.residueMap a} : Set target.residueField) =
        (⊤ : IntermediateField base.residueField target.residueField) ∧
      target.valuation.IsUniformizer (Polynomial.aeval a P : L) ∧
      IsUnit
        ((P.map
          (algebraMap base.valuationSubring target.valuationSubring)).derivative.eval a) ∧
      Algebra.adjoin base.valuationSubring
          ({a} : Set target.valuationSubring) =
        (⊤ : Subalgebra base.valuationSubring target.valuationSubring)
theorem

exists_valuationSubring_adjoin_eq_top_of_uniqueExtension

L584 ↗
RamificationTheory.HilbertRamification.Higher.exists_valuationSubring_adjoin_eq_top_of_uniqueExtension
Documentation

A noncomplete monogeneity theorem for integral valuation rings.

Source context 12 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ResidueField
namespace Higher
open scoped Polynomial
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
Lean source · statement
theorem exists_valuationSubring_adjoin_eq_top_of_uniqueExtension
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    [Algebra.IsSeparable base.residueField target.residueField] :
    ∃ a : target.valuationSubring,
      Algebra.adjoin base.valuationSubring
          ({a} : Set target.valuationSubring) =
        (⊤ : Subalgebra base.valuationSubring target.valuationSubring)

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