Module

Place_sum_fiber_ord_eq_finrank.lean

Nyll.AlgebraicCurves.Places.Place_sum_fiber_ord_eq_finrank

49 declarations indexed from sourceView source ↗

Module documentation

Place sum fiber ord eq finrank

Imports12

Imported by1

Nyll.AlgebraicCurves.Places.All

def

fib

L51 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.fib

Documentation

The set of places at which the selected function is regular and takes the prescribed value.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

def fib (b : ℂ) : Set (Place ℂ F)

def

poles

L54 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.poles

Documentation

The set of poles of the selected function.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

def poles : Set (Place ℂ F)

def

eFin

L57 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.eFin

Documentation

The nonnegative multiplicity of the selected function minus the prescribed finite value.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

def eFin (w : Place ℂ F) (b : ℂ) : ℕ

def

eInf

L60 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.eInf

Documentation

The nonnegative order of the inverse function at a place.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

def eInf (w : Place ℂ F) : ℕ

abbrev

deg

L64 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.deg

Documentation

The degree of the function-field extension over the field generated by the selected function.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

abbrev deg : ℕ

theorem

mem_fib_iff

L66 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.mem_fib_iff

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem mem_fib_iff {w : Place ℂ F} {b : ℂ} :
    w ∈ fib x b ↔ x ∈ w.toValuationSubring ∧ Place.evalAt w x = b

theorem

mem_poles_iff

L69 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.mem_poles_iff

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem mem_poles_iff {w : Place ℂ F} : w ∈ poles x ↔ x ∉ w.toValuationSubring

theorem

evalAt_sub_algebraMap

L71 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.evalAt_sub_algebraMap

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem evalAt_sub_algebraMap (v : Place ℂ F) (hv : v.IsRational) {f : F}
    (hf : f ∈ v.toValuationSubring) (c : ℂ) :
    v.evalAt (f - algebraMap ℂ F c) = v.evalAt f - c

theorem

evalAt_eq_zero_of_ord_pos

L83 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.evalAt_eq_zero_of_ord_pos

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem evalAt_eq_zero_of_ord_pos (v : Place ℂ F) {g : F} (hg : g ≠ 0)
    (h : 0 < v.ord g) : v.evalAt g = 0

theorem

ord_eq_zero_of_evalAt_ne_zero

L99 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.ord_eq_zero_of_evalAt_ne_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem ord_eq_zero_of_evalAt_ne_zero (v : Place ℂ F) {g : F} (hg : g ≠ 0)
    (hmem : g ∈ v.toValuationSubring) (hne : v.evalAt g ≠ 0) : v.ord g = 0

theorem

ord_pos_of_evalAt_eq_zero

L106 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.ord_pos_of_evalAt_eq_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem ord_pos_of_evalAt_eq_zero (v : Place ℂ F) (hv : v.IsRational) {g : F} (hg : g ≠ 0)
    (hmem : g ∈ v.toValuationSubring) (hz : v.evalAt g = 0) : 0 < v.ord g

theorem

ord_multiset_prod

L113 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.ord_multiset_prod

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem ord_multiset_prod (v : Place ℂ F) (s : Multiset F) (hs : ∀ y ∈ s, y ≠ 0) :
    v.ord s.prod = (s.map v.ord).sum

theorem

ord_algebraMap_eq_zero

L124 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.ord_algebraMap_eq_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem ord_algebraMap_eq_zero (v : Place ℂ F) {c : ℂ} (hc : c ≠ 0) :
    v.ord (algebraMap ℂ F c) = 0

theorem

sum_map_ite_count

L139 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.sum_map_ite_count

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · full declaration

theorem sum_map_ite_count (t : ℂ) (e : ℤ) (s : Multiset ℂ) :
    (s.map (fun r => if r = t then e else 0)).sum = (s.count t : ℤ) * e := by
  classical
  induction s using Multiset.induction_on with
  | empty => simp
  | cons a s ih =>
    rw [Multiset.map_cons, Multiset.sum_cons, ih, Multiset.count_cons]
    by_cases h : a = t
    · rw [ite_eq_left h, ite_eq_left h.symm]
      push_cast
      ring
    · rw [ite_eq_right h, ite_eq_right (fun hh => h hh.symm)]
      push_cast
      ring

theorem

ord_aeval

L154 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.ord_aeval

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem ord_aeval (v : Place ℂ F) (hv : v.IsRational) {g : F} (htg : Transcendental ℂ g)
    (hmem : g ∈ v.toValuationSubring) {p : ℂ[X]} (hp : p ≠ 0) :
    v.ord (Polynomial.aeval g p)
      = v.ord (g - algebraMap ℂ F (v.evalAt g)) * p.rootMultiplicity (v.evalAt g)

theorem

isRational_of_finite

L199 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.isRational_of_finite

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem isRational_of_finite {L : Type*} [Field L] [Algebra ℂ L] (v : Place ℂ L)
    (hfin : Module.Finite ℂ v.ResidueField) : v.IsRational

theorem

nonneg_mul_of_nonneg_mul

L205 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.nonneg_mul_of_nonneg_mul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem nonneg_mul_of_nonneg_mul {e e' d : ℤ} (he : 0 < e) (he' : 0 < e')
    (h : 0 ≤ e * d) : 0 ≤ e' * d

theorem

pos_of_mul_pos_of_pos

L214 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.pos_of_mul_pos_of_pos

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem pos_of_mul_pos_of_pos {e k : ℤ} (he : 0 < e) (h : 0 < e * k) : 0 < k

theorem

neg_of_mul_neg_of_pos

L219 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.neg_of_mul_neg_of_pos

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem neg_of_mul_neg_of_pos {e k : ℤ} (he : 0 < e) (h : e * k < 0) : k < 0

theorem

ne_zero_of_transcendental

L224 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.ne_zero_of_transcendental

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem ne_zero_of_transcendental {g : F} (hg : Transcendental ℂ g) : g ≠ 0

theorem

transcendental_inv

L230 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.transcendental_inv

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem transcendental_inv {g : F} (hg : Transcendental ℂ g) : Transcendental ℂ g⁻¹

theorem

adjoin_le_adjoin_inv

L233 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.adjoin_le_adjoin_inv

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem adjoin_le_adjoin_inv (g : F) :
    IntermediateField.adjoin ℂ ({g} : Set F) ≤ IntermediateField.adjoin ℂ ({g⁻¹} : Set F)

theorem

sub_ne_zero

L239 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.sub_ne_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem sub_ne_zero (htr : Transcendental ℂ x) (b : ℂ) : x - algebraMap ℂ F b ≠ 0

theorem

transcendental_sub_algebraMap

L242 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.transcendental_sub_algebraMap

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem transcendental_sub_algebraMap (htr : Transcendental ℂ x) (c : ℂ) :
    Transcendental ℂ (x - algebraMap ℂ F c)

theorem

adjoin_inv_sub_eq

L249 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.adjoin_inv_sub_eq

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem adjoin_inv_sub_eq (c : ℂ) :
    IntermediateField.adjoin ℂ ({(x - algebraMap ℂ F c)⁻¹} : Set F)
      = IntermediateField.adjoin ℂ ({x} : Set F)

theorem

sub_mem_of_mem_fib

L263 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.sub_mem_of_mem_fib

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem sub_mem_of_mem_fib {w : Place ℂ F} {b : ℂ} (hw : w ∈ fib x b) :
    x - algebraMap ℂ F b ∈ w.toValuationSubring

theorem

inv_mem_of_mem_poles

L267 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.inv_mem_of_mem_poles

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem inv_mem_of_mem_poles {w : Place ℂ F} (hw : w ∈ poles x) : x⁻¹ ∈ w.toValuationSubring

theorem

ne_zero_of_mem_poles

L270 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.ne_zero_of_mem_poles

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem ne_zero_of_mem_poles {w : Place ℂ F} (hw : w ∈ poles x) : x ≠ 0

theorem

ord_neg_of_mem_poles

L276 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.ord_neg_of_mem_poles

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem ord_neg_of_mem_poles {w : Place ℂ F} (hw : w ∈ poles x) : w.ord x < 0

theorem

ord_inv_pos_of_mem_poles

L281 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.ord_inv_pos_of_mem_poles

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem ord_inv_pos_of_mem_poles {w : Place ℂ F} (hw : w ∈ poles x) : 0 < w.ord x⁻¹

theorem

evalAt_inv_of_mem_poles

L286 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.evalAt_inv_of_mem_poles

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem evalAt_inv_of_mem_poles {w : Place ℂ F} (hw : w ∈ poles x) : Place.evalAt w x⁻¹ = 0

theorem

exists_mem_poles

L290 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.exists_mem_poles

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem exists_mem_poles (htr : Transcendental ℂ x)
    [FiniteDimensional (IntermediateField.adjoin ℂ ({x} : Set F)) F] :
    ∃ w : Place ℂ F, w ∈ poles x

theorem

mem_poles_of_restrict_eq

L298 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.mem_poles_of_restrict_eq

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)

Lean source · statement

theorem mem_poles_of_restrict_eq
    [FiniteDimensional (IntermediateField.adjoin ℂ ({x} : Set F)) F] {w₀ w : Place ℂ F}
    (hw₀ : w₀ ∈ poles x)
    (hre : w.restrict (IntermediateField.adjoin ℂ ({x} : Set F))
      = w₀.restrict (IntermediateField.adjoin ℂ ({x} : Set F))) : w ∈ poles x

theorem

place_isRational

L330 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.place_isRational

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)
variable [IsCurveOver ℂ F]

Lean source · statement

theorem place_isRational (w : Place ℂ F) : w.IsRational

theorem

restrict_isRational

L333 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.restrict_isRational

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)
variable [IsCurveOver ℂ F]

Lean source · statement

theorem restrict_isRational
    [FiniteDimensional (IntermediateField.adjoin ℂ ({x} : Set F)) F] (w : Place ℂ F) :
    (w.restrict (IntermediateField.adjoin ℂ ({x} : Set F))).IsRational

theorem

evalAt_sub_of_mem_fib

L343 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.evalAt_sub_of_mem_fib

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)
variable [IsCurveOver ℂ F]

Lean source · statement

theorem evalAt_sub_of_mem_fib {w : Place ℂ F} {b : ℂ} (hw : w ∈ fib x b) :
    Place.evalAt w (x - algebraMap ℂ F b) = 0

theorem

exists_mem_fib

L348 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.exists_mem_fib

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)
variable [IsCurveOver ℂ F]

Lean source · statement

theorem exists_mem_fib (htr : Transcendental ℂ x)
    [FiniteDimensional (IntermediateField.adjoin ℂ ({x} : Set F)) F] (b : ℂ) :
    ∃ w : Place ℂ F, w ∈ fib x b

theorem

exists_ord_coe_eq

L370 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.exists_ord_coe_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)
variable [IsCurveOver ℂ F]

Lean source · statement

theorem exists_ord_coe_eq {g : F} (htg : Transcendental ℂ g)
    (hle : IntermediateField.adjoin ℂ ({x} : Set F) ≤ IntermediateField.adjoin ℂ ({g} : Set F))
    (c : ℂ) (y : ↥(IntermediateField.adjoin ℂ ({x} : Set F))) (hy : y ≠ 0) :
    ∃ k : ℤ, ∀ w : Place ℂ F, g ∈ w.toValuationSubring → w.evalAt g = c →
      w.ord (y : F) = w.ord (g - algebraMap ℂ F c) * k

theorem

restrict_eq_of_forall

L400 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.restrict_eq_of_forall

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)
variable [IsCurveOver ℂ F]

Lean source · statement

theorem restrict_eq_of_forall
    [FiniteDimensional (IntermediateField.adjoin ℂ ({x} : Set F)) F]
    {g : F} (htg : Transcendental ℂ g)
    (hle : IntermediateField.adjoin ℂ ({x} : Set F) ≤ IntermediateField.adjoin ℂ ({g} : Set F))
    (c : ℂ) {w w' : Place ℂ F}
    (hw : g ∈ w.toValuationSubring ∧ w.evalAt g = c)
    (hw' : g ∈ w'.toValuationSubring ∧ w'.evalAt g = c) :
    w.restrict (IntermediateField.adjoin ℂ ({x} : Set F))
      = w'.restrict (IntermediateField.adjoin ℂ ({x} : Set F))

theorem

ramificationIndex_eq_ord

L428 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.ramificationIndex_eq_ord

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)
variable [IsCurveOver ℂ F]

Lean source · statement

theorem ramificationIndex_eq_ord
    [FiniteDimensional (IntermediateField.adjoin ℂ ({x} : Set F)) F]
    {g : F} (htg : Transcendental ℂ g)
    (hle : IntermediateField.adjoin ℂ ({x} : Set F) ≤ IntermediateField.adjoin ℂ ({g} : Set F))
    (hgE : g ∈ IntermediateField.adjoin ℂ ({x} : Set F)) (c : ℂ) (w : Place ℂ F)
    (hgm : g ∈ w.toValuationSubring) (hgc : w.evalAt g = c) :
    (w.ramificationIndex (↥(IntermediateField.adjoin ℂ ({x} : Set F))) : ℤ)
      = w.ord (g - algebraMap ℂ F c)

theorem

mem_fib_of_restrict_eq

L464 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.mem_fib_of_restrict_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)
variable [IsCurveOver ℂ F]

Lean source · statement

theorem mem_fib_of_restrict_eq (htr : Transcendental ℂ x)
    [FiniteDimensional (IntermediateField.adjoin ℂ ({x} : Set F)) F] {b : ℂ} {w₀ w : Place ℂ F}
    (hw₀ : w₀ ∈ fib x b)
    (hre : w.restrict (IntermediateField.adjoin ℂ ({x} : Set F))
      = w₀.restrict (IntermediateField.adjoin ℂ ({x} : Set F))) : w ∈ fib x b

theorem

fib_iff_restrict_eq

L507 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.fib_iff_restrict_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)
variable [IsCurveOver ℂ F]

Lean source · statement

theorem fib_iff_restrict_eq (htr : Transcendental ℂ x)
    [FiniteDimensional (IntermediateField.adjoin ℂ ({x} : Set F)) F] {b : ℂ} {w₀ : Place ℂ F}
    (hw₀ : w₀ ∈ fib x b) (w : Place ℂ F) :
    w ∈ fib x b ↔ w.restrict (IntermediateField.adjoin ℂ ({x} : Set F))
      = w₀.restrict (IntermediateField.adjoin ℂ ({x} : Set F))

theorem

poles_iff_restrict_eq

L515 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.poles_iff_restrict_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)
variable [IsCurveOver ℂ F]

Lean source · statement

theorem poles_iff_restrict_eq (htr : Transcendental ℂ x)
    [FiniteDimensional (IntermediateField.adjoin ℂ ({x} : Set F)) F] {w₀ : Place ℂ F}
    (hw₀ : w₀ ∈ poles x) (w : Place ℂ F) :
    w ∈ poles x ↔ w.restrict (IntermediateField.adjoin ℂ ({x} : Set F))
      = w₀.restrict (IntermediateField.adjoin ℂ ({x} : Set F))

theorem

eFin_eq_ramificationIndex

L525 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.eFin_eq_ramificationIndex

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)
variable [IsCurveOver ℂ F]

Lean source · statement

theorem eFin_eq_ramificationIndex (htr : Transcendental ℂ x)
    [FiniteDimensional (IntermediateField.adjoin ℂ ({x} : Set F)) F] {w : Place ℂ F} {b : ℂ}
    (hw : w ∈ fib x b) :
    (eFin x w b : ℤ) = (w.ramificationIndex (↥(IntermediateField.adjoin ℂ ({x} : Set F))) : ℤ)

theorem

eInf_eq_ramificationIndex

L538 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.eInf_eq_ramificationIndex

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)
variable [IsCurveOver ℂ F]

Lean source · statement

theorem eInf_eq_ramificationIndex (htr : Transcendental ℂ x)
    [FiniteDimensional (IntermediateField.adjoin ℂ ({x} : Set F)) F] {w : Place ℂ F}
    (hw : w ∈ poles x) :
    (eInf x w : ℤ) = (w.ramificationIndex (↥(IntermediateField.adjoin ℂ ({x} : Set F))) : ℤ)

theorem

sum_eFin

L552 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.sum_eFin

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)
variable [IsCurveOver ℂ F]

Lean source · statement

theorem sum_eFin (htr : Transcendental ℂ x)
    [FiniteDimensional (IntermediateField.adjoin ℂ ({x} : Set F)) F] (b : ℂ)
    (s : Finset (Place ℂ F))
    (hs : ∀ w, w ∈ s ↔ w ∈ fib x b) : ∑ w ∈ s, eFin x w b = deg x

theorem

sum_eInf

L580 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreOrderCount.sum_eInf

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
noncomputable section
namespace FibreOrderCount
open AlgebraicCurve Polynomial
variable {F : Type*} [Field F] [Algebra ℂ F]
variable (x : F)
variable [IsCurveOver ℂ F]

Lean source · statement

theorem sum_eInf (htr : Transcendental ℂ x)
    [FiniteDimensional (IntermediateField.adjoin ℂ ({x} : Set F)) F] (s : Finset (Place ℂ F))
    (hs : ∀ w, w ∈ s ↔ w ∈ poles x) : ∑ w ∈ s, eInf x w = deg x

theorem

sum_fiber_ord_eq_finrank

L617 ↗

AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank.FibreIdentity.sum_fiber_ord_eq_finrank

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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
section MainStatement
open AlgebraicCurve IntermediateField
namespace FibreIdentity

Lean source · statement

theorem sum_fiber_ord_eq_finrank {F : Type*} [Field F] [Algebra ℂ F] [IsCurveOver ℂ F]
    {x : F} (htr : Transcendental ℂ x) [FiniteDimensional (↥(adjoin ℂ ({x} : Set F))) F] :
    (∀ (b : ℂ) (s : Finset (Place ℂ F)),
      (∀ w : Place ℂ F, w ∈ s ↔ x ∈ w.toValuationSubring ∧ Place.evalAt w x = b) →
      ∑ w ∈ s, (w.ord (x - algebraMap ℂ F b)).toNat = Module.finrank (↥(adjoin ℂ ({x} : Set F))) F)
        ∧
    (∀ s : Finset (Place ℂ F), (∀ w : Place ℂ F, w ∈ s ↔ x ∉ w.toValuationSubring) →
      ∑ w ∈ s, (w.ord x⁻¹).toNat = Module.finrank (↥(adjoin ℂ ({x} : Set F))) F)

theorem

sum_fiber_ord_eq_finrank

L634 ↗

AlgebraicCurve.Place.sum_fiber_ord_eq_finrank

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_sum_fiber_ord_eq_finrank
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 IntermediateField

Lean source · statement

theorem _root_.AlgebraicCurve.Place.sum_fiber_ord_eq_finrank {F : Type*} [Field F] [Algebra ℂ F]
  [IsCurveOver ℂ F]
    {x : F} (htr : Transcendental ℂ x) [FiniteDimensional (↥(adjoin ℂ ({x} : Set F))) F] :
    (∀ (b : ℂ) (s : Finset (Place ℂ F)),
      (∀ w : Place ℂ F, w ∈ s ↔ x ∈ w.toValuationSubring ∧ Place.evalAt w x = b) →
      ∑ w ∈ s, (w.ord (x - algebraMap ℂ F b)).toNat = Module.finrank (↥(adjoin ℂ ({x} : Set F))) F)
        ∧
    (∀ s : Finset (Place ℂ F), (∀ w : Place ℂ F, w ∈ s ↔ x ∉ w.toValuationSubring) →
      ∑ w ∈ s, (w.ord x⁻¹).toNat = Module.finrank (↥(adjoin ℂ ({x} : Set F))) F)

Module documentation

Place sum fiber ord eq finrank

Declarations