NYLL
Module

Exists_place_over_of_simple_root_along.lean

Nyll.AlgebraicCurves.Places.Exists_place_over_of_simple_root_along
12 declarations indexed from sourceView source ↗

Module documentation

Exists place over of simple root along

Imports7
Imported by1

Declarations

theorem

eq_singleton_of_sum_eq_one

L41 ↗
AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along.S09SR.eq_singleton_of_sum_eq_one
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace S09SR
Lean source · statement
theorem eq_singleton_of_sum_eq_one {ι : Type*} (S : Finset ι) (g : ι → ℕ) (hg : ∀ x ∈ S, 1 ≤ g x)
    (h : ∑ x ∈ S, g x = 1) : ∃ a, S = {a} ∧ g a = 1
theorem

ord_coe_eq_zero_of_isUnit

L59 ↗
AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along.S09SR.ord_coe_eq_zero_of_isUnit
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace S09SR
section OnePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_coe_eq_zero_of_isUnit (v : Place K F) {u : v.toValuationSubring} (hu : IsUnit u) :
    ((u : F) ≠ 0) ∧ v.ord (u : F) = 0
theorem

ord_add_eq_zero

L74 ↗
AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along.S09SR.ord_add_eq_zero
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace S09SR
section OnePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_add_eq_zero (w : Place K F) {u z : F} (hu0 : u ≠ 0) (hu : w.ord u = 0)
    (humem : u ∈ w.toValuationSubring) (hz : z ∈ w.toValuationSubring) (hzpos : z = 0 ∨ 0 < w.ord
      z) :
    u + z ≠ 0 ∧ w.ord (u + z) = 0
theorem

exists_taylor

L104 ↗
AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along.S09SR.exists_taylor
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace S09SR
section OnePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_taylor (v : Place K F) (Q : Polynomial v.toValuationSubring) (b :
  v.toValuationSubring) :
    ∃ S : Polynomial v.toValuationSubring,
      Q - C (Q.eval b) = (X - C b) * S ∧ S.eval b = Q.derivative.eval b
theorem

aeval_taylor

L125 ↗
AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along.S09SR.aeval_taylor
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace S09SR
section Engine
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
  [Algebra F F'] [IsScalarTower K F F']
omit [Algebra K F'] [IsScalarTower K F F'] in
Lean source · statement
theorem aeval_taylor (v : Place K F) {Q S : Polynomial v.toValuationSubring} {b :
  v.toValuationSubring}
    (hS : Q - C (Q.eval b) = (X - C b) * S) (x : F') :
    aeval x (Q.map (algebraMap v.toValuationSubring F)) - algebraMap F F' ((Q.eval b :
      v.toValuationSubring) : F)
      = (x - algebraMap F F' (b : F)) * aeval x (S.map (algebraMap v.toValuationSubring F))
theorem

algebraMap_mem_of_restrict_eq

L138 ↗
AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along.S09SR.algebraMap_mem_of_restrict_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace S09SR
section Engine
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
  [Algebra F F'] [IsScalarTower K F F']
variable [Algebra.IsIntegral F F']
Lean source · statement
theorem algebraMap_mem_of_restrict_eq {w : Place K F'} {v : Place K F} (hw : w.restrict F = v)
    (r : v.toValuationSubring) : algebraMap F F' (r : F) ∈ w.toValuationSubring
theorem

aeval_mem_of_restrict_eq

L143 ↗
AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along.S09SR.aeval_mem_of_restrict_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace S09SR
section Engine
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
  [Algebra F F'] [IsScalarTower K F F']
variable [Algebra.IsIntegral F F']
Lean source · statement
theorem aeval_mem_of_restrict_eq {w : Place K F'} {v : Place K F} (hw : w.restrict F = v)
    (S : Polynomial v.toValuationSubring) {x : F'} (hxmem : x ∈ w.toValuationSubring) :
    aeval x (S.map (algebraMap v.toValuationSubring F)) ∈ w.toValuationSubring
theorem

root_mem_of_restrict_eq

L151 ↗
AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along.S09SR.root_mem_of_restrict_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace S09SR
section Engine
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
  [Algebra F F'] [IsScalarTower K F F']
variable [Algebra.IsIntegral F F']
Lean source · statement
theorem root_mem_of_restrict_eq {w : Place K F'} {v : Place K F} (hw : w.restrict F = v)
    {Q : Polynomial v.toValuationSubring} (hQ : Q.Monic) {x : F'}
    (hx : aeval x (Q.map (algebraMap v.toValuationSubring F)) = 0) : x ∈ w.toValuationSubring
theorem

ord_sub_eq_ramificationIndex_mul

L162 ↗
AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along.S09SR.ord_sub_eq_ramificationIndex_mul
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace S09SR
section Engine
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
  [Algebra F F'] [IsScalarTower K F F']
variable [Algebra.IsIntegral F F']
Lean source · statement
theorem ord_sub_eq_ramificationIndex_mul (v : Place K F) (Q : Polynomial v.toValuationSubring)
    {x : F'} (hx : aeval x (Q.map (algebraMap v.toValuationSubring F)) = 0)
    (b : v.toValuationSubring) (hsimple : IsUnit (Q.derivative.eval b))
    {w : Place K F'} (hw : w.restrict F = v) (hxb : 0 < w.ord (x - algebraMap F F' (b : F))) :
    w.ord (x - algebraMap F F' (b : F))
      = Place.ramificationIndex (F := F) w * v.ord ((Q.eval b : v.toValuationSubring) : F)
theorem

exists_place_of_simple_root

L213 ↗
AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along.S09SR.exists_place_of_simple_root
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace S09SR
section Engine
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
  [Algebra F F'] [IsScalarTower K F F']
variable [Algebra.IsIntegral F F']
variable [Module.Finite F F'] [HasPrincipalDivisors K F']
Lean source · statement
theorem exists_place_of_simple_root (H : Divisor.PushforwardNormFormula K F F') (v : Place K F)
    {Q : Polynomial v.toValuationSubring} (hQ : Q.Monic) {x : F'}
    (hx : aeval x (Q.map (algebraMap v.toValuationSubring F)) = 0)
    (b : v.toValuationSubring) (hroot : 0 < v.ord ((Q.eval b : v.toValuationSubring) : F))
    (hsimple : IsUnit (Q.derivative.eval b))
    (hnorm : v.ord (Algebra.norm F (x - algebraMap F F' (b : F))) = v.ord ((Q.eval b :
      v.toValuationSubring) : F)) :
    ∃ w₀ : Place K F', w₀.restrict F = v ∧ 0 < w₀.ord (x - algebraMap F F' (b : F)) ∧
      Place.ramificationIndex (F := F) w₀ = 1 ∧ w₀.inertiaDeg F = 1 ∧
      ∀ w : Place K F', w.restrict F = v → 0 < w.ord (x - algebraMap F F' (b : F)) → w = w₀
theorem

exists_place_of_simple_root_along

L284 ↗
AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along.S09SR.exists_place_of_simple_root_along
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
namespace S09SR
section Along
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] [CharZero F]
  [HasPrincipalDivisors K F']
Lean source · full declaration
theorem exists_place_of_simple_root_along (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hfin :
  FiniteAlong K φ)
    (v : Place K F) {Q : Polynomial v.toValuationSubring} (hQ : Q.Monic) {x : F'}
    (hx : (Q.map (algebraMap v.toValuationSubring F)).eval₂ φ.toRingHom x = 0)
    (b : v.toValuationSubring) (hroot : 0 < v.ord ((Q.eval b : v.toValuationSubring) : F))
    (hsimple : IsUnit (Q.derivative.eval b))
    (hnorm :
      let _ : Algebra F F' := algebraAlong φ
      v.ord (Algebra.norm F (x - φ (b : F))) =
        v.ord ((Q.eval b : v.toValuationSubring) : F)) :
    ∃ w₀ : Place K F', w₀.restrictAlong φ hφ = v ∧ 0 < w₀.ord (x - φ (b : F)) ∧
      w₀.ramificationIndexAlong φ = 1 ∧ w₀.inertiaDegAlong φ hφ = 1 ∧
      ∀ w : Place K F', w.restrictAlong φ hφ = v → 0 < w.ord (x - φ (b : F)) → w = w₀ := by
  let : Algebra F F' := algebraAlong φ
  have := isScalarTower_along φ
  have := isIntegral_along φ hφ
  have : Module.Finite F F' := hfin
  have H : Divisor.PushforwardNormFormula K F F' := normFormulaAlong φ hfin
    (separableAlong_of_charZero φ hφ)
  have hx' : aeval x (Q.map (algebraMap v.toValuationSubring F)) = 0 := by
    rw [aeval_def]; exact hx
  exact exists_place_of_simple_root H v hQ hx' b hroot hsimple hnorm
theorem

exists_place_over_of_simple_root_along

L311 ↗
AlgebraicCurve.exists_place_over_of_simple_root_along
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_place_over_of_simple_root_along
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurve Polynomial
Lean source · full declaration
theorem _root_.AlgebraicCurve.exists_place_over_of_simple_root_along {K F F' : Type*} [Field K]
  [Field F] [Field F'] [Algebra K F] [Algebra K F'] [CharZero F] [HasPrincipalDivisors K F'] (φ : F
  →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hfin : FiniteAlong K φ) (v : Place K F) {Q : Polynomial
  v.toValuationSubring} (hQ : Q.Monic) {x : F'} (hx : (Q.map (algebraMap v.toValuationSubring
  F)).eval₂ φ.toRingHom x = 0) (b : v.toValuationSubring) (hroot : 0 < v.ord ((Q.eval b :
  v.toValuationSubring) : F)) (hsimple : IsUnit ((Polynomial.derivative Q).eval b))
  (hnorm :
    let _ : Algebra F F' := algebraAlong φ
    v.ord (Algebra.norm F (x - φ (b : F))) =
      v.ord ((Q.eval b : v.toValuationSubring) : F)) :
    ∃ w₀ : Place K F', w₀.restrictAlong φ hφ = v ∧ 0 < w₀.ord (x - φ (b : F)) ∧
      w₀.ramificationIndexAlong φ = 1 ∧ w₀.inertiaDegAlong φ hφ = 1 ∧
      ∀ w : Place K F', w.restrictAlong φ hφ = v → 0 < w.ord (x - φ (b : F)) → w = w₀ := by
  exact S09SR.exists_place_of_simple_root_along φ hφ hfin v hQ hx b hroot hsimple hnorm

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