NYLL
Module

OrbitPolynomialIdeal.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.OrbitPolynomialIdeal
14 declarations indexed from sourceView source ↗

Module documentation

Quotient-depth identity over a general DVF

This file proves the orbit-polynomial ideal identity before normalization of the fixed-field valuation. It uses the literal fixed field and its literal restricted valuation ring; no completeness or Henselian hypothesis occurs.

Imports3
Imported by2

Declarations

theorem

prod_X_sub_C_dvd_of_eval_eq_zero_dvf

L32 ↗
RamificationTheory.HilbertRamification.Higher.prod_X_sub_C_dvd_of_eval_eq_zero_dvf
Documentation

A polynomial vanishing at every point of a finite set is divisible by the product of the corresponding distinct linear factors.

Source context 5 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open scoped Polynomial
Lean source · statement
theorem prod_X_sub_C_dvd_of_eval_eq_zero_dvf
    {R : Type*} [CommRing R] [IsDomain R]
    (s : Finset R) (p : Polynomial R)
    (hp : ∀ a ∈ s, p.eval a = 0) :
    (∏ a ∈ s, (Polynomial.X - Polynomial.C a)) ∣ p
theorem

fintype_prod_X_sub_C_dvd_of_eval_eq_zero_of_injective_dvf

L60 ↗
RamificationTheory.HilbertRamification.Higher.fintype_prod_X_sub_C_dvd_of_eval_eq_zero_of_injective_dvf
Documentation

States the theorem fintype_prod_X_sub_C_dvd_of_eval_eq_zero_of_injective_dvf.

Source context 5 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open scoped Polynomial
Lean source · statement
theorem fintype_prod_X_sub_C_dvd_of_eval_eq_zero_of_injective_dvf
    {R ι : Type*} [CommRing R] [IsDomain R] [Fintype ι]
    (r : ι → R) (hr : Function.Injective r) (p : Polynomial R)
    (hp : ∀ i, p.eval (r i) = 0) :
    (∏ i, (Polynomial.X - Polynomial.C (r i))) ∣ p
theorem

polynomial_eval_mem_ideal_of_coeff_mem_dvf

L80 ↗
RamificationTheory.HilbertRamification.Higher.polynomial_eval_mem_ideal_of_coeff_mem_dvf
Documentation

States the theorem polynomial_eval_mem_ideal_of_coeff_mem_dvf.

Source context 5 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open scoped Polynomial
Lean source · statement
theorem polynomial_eval_mem_ideal_of_coeff_mem_dvf
    {R : Type*} [CommRing R] (I : Ideal R) (p : Polynomial R) (z : R)
    (hp : ∀ n, p.coeff n ∈ I) : p.eval z ∈ I
theorem

valuationSubringAutOfUniqueExtension_generator_injective

L94 ↗
RamificationTheory.HilbertRamification.Higher.valuationSubringAutOfUniqueExtension_generator_injective
Documentation

A generator of the top valuation ring has a faithful Galois orbit.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · full declaration
theorem valuationSubringAutOfUniqueExtension_generator_injective
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    {z : target.valuationSubring}
    (hz : Algebra.adjoin base.valuationSubring
      ({z} : Set target.valuationSubring) = ⊤) :
    Function.Injective
      (fun sigma : Gal(L/K) =>
        valuationSubringAutOfUniqueExtension
          (base := base) (target := target) huniq sigma z) := by
  intro sigma tau hst
  have hring :
      (valuationSubringAlgEquivOfUniqueExtension
        (base := base) (target := target) huniq sigma).toAlgHom =
      (valuationSubringAlgEquivOfUniqueExtension
        (base := base) (target := target) huniq tau).toAlgHom := by
    apply AlgHom.ext_of_adjoin_eq_top hz
    intro a ha
    rw [Set.mem_singleton_iff] at ha
    subst a
    exact hst
  have hfix (a : target.valuationSubring) :
      sigma (algebraMap target.valuationSubring L a) =
        tau (algebraMap target.valuationSubring L a) := by
    change sigma (a : L) = tau (a : L)
    have ha := congrArg Subtype.val (DFunLike.congr_fun hring a)
    change sigma (a : L) = tau (a : L) at ha
    exact ha
  apply AlgEquiv.ext
  intro a
  let : IsFractionRing target.valuationSubring L :=
    target.valuationSubring_isFractionRing
  obtain ⟨b, c, _hc, ha⟩ :=
    IsFractionRing.div_surjective (A := target.valuationSubring) a
  rw [← ha, map_div₀, map_div₀, hfix b, hfix c]
def

subgroupOrbitPolynomialDVF

L132 ↗
RamificationTheory.HilbertRamification.Higher.subgroupOrbitPolynomialDVF
Documentation

The polynomial whose roots are the H-orbit of the top generator.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def subgroupOrbitPolynomialDVF
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) (z : target.valuationSubring) :
    Polynomial target.valuationSubring
theorem

subgroupOrbitPolynomialDVF_map_aut

L147 ↗
RamificationTheory.HilbertRamification.Higher.subgroupOrbitPolynomialDVF_map_aut
Documentation

States the theorem subgroupOrbitPolynomialDVF_map_aut.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in
Lean source · statement
theorem subgroupOrbitPolynomialDVF_map_aut
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) (z : target.valuationSubring) (rho : H) :
    (subgroupOrbitPolynomialDVF
        (base := base) (target := target) huniq H z).map
      (valuationSubringAutOfUniqueExtension
        (base := base) (target := target) huniq rho).toRingHom =
      subgroupOrbitPolynomialDVF
        (base := base) (target := target) huniq H z
def

subgroupOrbitPolynomialCoeffFixedFieldDVF

L184 ↗
RamificationTheory.HilbertRamification.Higher.subgroupOrbitPolynomialCoeffFixedFieldDVF
Documentation

Every orbit-polynomial coefficient, packaged in the literal restricted valuation ring of the actual fixed field.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def subgroupOrbitPolynomialCoeffFixedFieldDVF
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) (z : target.valuationSubring) (n : ℕ) :
    fixedFieldValuationSubringDVF (K := K) (target := target) H
def

cosetGeneratorDisplacementProductDVF

L201 ↗
RamificationTheory.HilbertRamification.Higher.cosetGeneratorDisplacementProductDVF
Documentation

Product of generator displacements over the right coset sigma H.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def cosetGeneratorDisplacementProductDVF
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) (sigma : Gal(L/K))
    (z : target.valuationSubring) : target.valuationSubring
theorem

subgroupOrbitPolynomialDVF_eval_self

L215 ↗
RamificationTheory.HilbertRamification.Higher.subgroupOrbitPolynomialDVF_eval_self
Documentation

States the theorem subgroupOrbitPolynomialDVF_eval_self.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in
Lean source · statement
theorem subgroupOrbitPolynomialDVF_eval_self
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) (z : target.valuationSubring) :
    (subgroupOrbitPolynomialDVF
      (base := base) (target := target) huniq H z).eval z = 0
theorem

subgroupOrbitPolynomialDVF_map_eval_eq_sign_mul_cosetProduct

L231 ↗
RamificationTheory.HilbertRamification.Higher.subgroupOrbitPolynomialDVF_map_eval_eq_sign_mul_cosetProduct
Documentation

States the theorem subgroupOrbitPolynomialDVF_map_eval_eq_sign_mul_cosetProduct.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in
Lean source · statement
theorem subgroupOrbitPolynomialDVF_map_eval_eq_sign_mul_cosetProduct
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) (sigma : Gal(L/K))
    (z : target.valuationSubring) :
    ((subgroupOrbitPolynomialDVF
        (base := base) (target := target) huniq H z).map
      (valuationSubringAutOfUniqueExtension
        (base := base) (target := target) huniq sigma).toRingHom).eval z =
      (-1) ^ Nat.card H * cosetGeneratorDisplacementProductDVF
        (base := base) (target := target) huniq H sigma z
theorem

fixedFieldToTarget_quotientAut_apply_dvf

L283 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldToTarget_quotientAut_apply_dvf
Documentation

Inclusion into O_L intertwines the quotient automorphism with any chosen top lift.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem fixedFieldToTarget_quotientAut_apply_dvf
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal]
    (sigma : Gal(L/K))
    (a : fixedFieldValuationSubringDVF (K := K) (target := target) H) :
    fixedFieldValuationSubringDVFToTarget
        (K := K) (target := target) H
        (fixedFieldValuationSubringAutDVF
          (base := base) (target := target) huniq H
          (IsGalois.normalAutEquivQuotient H sigma) a) =
      valuationSubringAutOfUniqueExtension
        (base := base) (target := target) huniq sigma
        (fixedFieldValuationSubringDVFToTarget
          (K := K) (target := target) H a)
theorem

cosetGeneratorDisplacementProductDVF_dvd_fixed_displacement

L306 ↗
RamificationTheory.HilbertRamification.Higher.cosetGeneratorDisplacementProductDVF_dvd_fixed_displacement
Documentation

The coset product divides every top displacement coming from the actual fixed valuation ring.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L] [IsGalois K L]
omit [IsGalois K L] in
Lean source · statement
theorem cosetGeneratorDisplacementProductDVF_dvd_fixed_displacement
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) (sigma : Gal(L/K))
    {z : target.valuationSubring}
    (hz : Algebra.adjoin base.valuationSubring
      ({z} : Set target.valuationSubring) = ⊤)
    (a : fixedFieldValuationSubringDVF (K := K) (target := target) H) :
    cosetGeneratorDisplacementProductDVF
        (base := base) (target := target) huniq H sigma z ∣
      valuationSubringAutOfUniqueExtension
          (base := base) (target := target) huniq sigma
          (fixedFieldValuationSubringDVFToTarget
            (K := K) (target := target) H a) -
        fixedFieldValuationSubringDVFToTarget
          (K := K) (target := target) H a
theorem

cosetGeneratorDisplacementProductDVF_mem_map_fixedFieldDisplacementIdeal

L419 ↗
RamificationTheory.HilbertRamification.Higher.cosetGeneratorDisplacementProductDVF_mem_map_fixedFieldDisplacementIdeal
Documentation

The coset product belongs to the image of the actual fixed-field displacement ideal.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem cosetGeneratorDisplacementProductDVF_mem_map_fixedFieldDisplacementIdeal
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal]
    (sigma : Gal(L/K)) (z : target.valuationSubring) :
    cosetGeneratorDisplacementProductDVF
        (base := base) (target := target) huniq H sigma z ∈
      Ideal.map (fixedFieldValuationSubringDVFToTarget
        (K := K) (target := target) H)
        (fixedFieldDisplacementIdealDVF
          (base := base) (target := target) huniq H
          (IsGalois.normalAutEquivQuotient H sigma))
theorem

span_cosetGeneratorDisplacementProduct_eq_map_fixedFieldDisplacementIdeal

L502 ↗
RamificationTheory.HilbertRamification.Higher.span_cosetGeneratorDisplacementProduct_eq_map_fixedFieldDisplacementIdeal
Documentation

The quotient-depth identity, ideal-level form.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
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 [base.valuation.HasExtension target.valuation]
variable [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem span_cosetGeneratorDisplacementProduct_eq_map_fixedFieldDisplacementIdeal
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal]
    (sigma : Gal(L/K)) {z : target.valuationSubring}
    (hz : Algebra.adjoin base.valuationSubring
      ({z} : Set target.valuationSubring) = ⊤) :
    Ideal.span (Set.singleton (cosetGeneratorDisplacementProductDVF
        (base := base) (target := target) huniq H sigma z) :
      Set target.valuationSubring) =
      Ideal.map (fixedFieldValuationSubringDVFToTarget
        (K := K) (target := target) H)
        (fixedFieldDisplacementIdealDVF
          (base := base) (target := target) huniq H
          (IsGalois.normalAutEquivQuotient H sigma))

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