Module

Divisor_mem_principal_of_forall_ell_pos_add.lean

Nyll.AlgebraicCurves.Divisors.Divisor_mem_principal_of_forall_ell_pos_add

19 declarations indexed from sourceView source ↗

Module documentation

Divisor mem principal of forall ell pos add

Imports4

Imported by2

theorem

ord_nonneg_of_mem

L36 ↗

AlgebraicCurve.Place.ord_nonneg_of_mem

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section SinglePlacePriv
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_nonneg_of_mem {f : F} (hf : f ∈
  v.toValuationSubring) : 0 ≤ v.ord f

theorem

mem_of_ord_nonneg

L53 ↗

AlgebraicCurve.Place.mem_of_ord_nonneg

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section SinglePlacePriv
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem _root_.AlgebraicCurve.Place.mem_of_ord_nonneg {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord
  f) :
    f ∈ v.toValuationSubring

theorem

mk_mem_maximalIdeal_iff

L78 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add.AlgebraicCurve.RROpensImpl.mk_mem_maximalIdeal_iff

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mk_mem_maximalIdeal_iff (v : Place K F) {f : F} (hf : f ∈ v.toValuationSubring) :
    (⟨f, hf⟩ : v.toValuationSubring) ∈ IsLocalRing.maximalIdeal v.toValuationSubring
      ↔ f = 0 ∨ 0 < v.ord f

theorem

ell_le_ell_sub_single_add_deg

L104 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add.AlgebraicCurve.RROpensImpl.ell_le_ell_sub_single_add_deg

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ell_le_ell_sub_single_add_deg [IsCurveOver K F] (D : Divisor K F)
    (P : Place K F) : ell D ≤ ell (D - Finsupp.single P 1) + P.deg

theorem

one_le_deg

L196 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add.AlgebraicCurve.RROpensImpl.one_le_deg

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem one_le_deg [IsCurveOver K F] (P : Place K F) : 1 ≤ P.deg

theorem

degree_eq_sum_support

L200 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add.AlgebraicCurve.RROpensImpl.degree_eq_sum_support

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem degree_eq_sum_support (D : Divisor K F) :
    Divisor.degree D = ∑ v ∈ D.support, D v * (v.deg : ℤ)

theorem

ell_canonical_eq

L210 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add.AlgebraicCurve.RROpensImpl.ell_canonical_eq

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section WithPack
variable {Kc : Divisor K F} {g : ℕ}

Lean source · statement

theorem ell_canonical_eq
    (hRR : ∀ D : Divisor K F, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g)
    (hC : ConstantsAreBase K F) : ell Kc = g

theorem

degree_add_one_sub_le_ell

L218 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add.AlgebraicCurve.RROpensImpl.degree_add_one_sub_le_ell

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section WithPack
variable {Kc : Divisor K F} {g : ℕ}

Lean source · statement

theorem degree_add_one_sub_le_ell
    (hRR : ∀ D : Divisor K F, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g)
    (E : Divisor K F) : Divisor.degree E + 1 - (g : ℤ) ≤ (ell E : ℤ)

theorem

finite_lSpace

L225 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add.AlgebraicCurve.RROpensImpl.finite_lSpace

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section WithPack
variable {Kc : Divisor K F} {g : ℕ}

Lean source · statement

theorem finite_lSpace [IsCurveOver K F]
    (hRR : ∀ D : Divisor K F, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g)
    (P : Place K F) (D : Divisor K F) : Module.Finite K (LSpace D)

theorem

exists_ord_pos_of_ord_neg

L254 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add.AlgebraicCurve.RROpensImpl.exists_ord_pos_of_ord_neg

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem exists_ord_pos_of_ord_neg [IsCurveOver K F] {x : F} (hx : x ≠ 0)
    (v₀ : Place K F) (hpole : v₀.ord x < 0) : ∃ P : Place K F, 0 < P.ord x

theorem

infinite_place_of_pole

L275 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add.AlgebraicCurve.RROpensImpl.infinite_place_of_pole

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem infinite_place_of_pole [IsCurveOver K F] [Infinite K] {x : F}
    (v₀ : Place K F) (hpole : v₀.ord x < 0) : Infinite (Place K F)

theorem

infinite_place

L315 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add.AlgebraicCurve.RROpensImpl.infinite_place

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem infinite_place [IsAlgClosed K] [IsCurveOver K F] (P : Place K F) :
    Infinite (Place K F)

theorem

ell_sub_single_add_one_eq

L326 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add.AlgebraicCurve.RROpensImpl.ell_sub_single_add_one_eq

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section WithPack
variable {Kc : Divisor K F} {g : ℕ}

Lean source · statement

theorem ell_sub_single_add_one_eq [IsCurveOver K F]
    (hRR : ∀ D : Divisor K F, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g)
    (P : Place K F) {G : Divisor K F} {f : F} (hfG : f ∈ LSpace G)
    (hf0 : f ≠ 0) {Q : Place K F} (hQ : Q.deg = 1) (hGQ : G Q = 0) (hfQ : Q.ord f = 0) :
    ell (G - Finsupp.single Q 1) + 1 = ell G

theorem

exists_finset_forall_ell_sub_single_add_one_eq

L352 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add.AlgebraicCurve.RROpensImpl.exists_finset_forall_ell_sub_single_add_one_eq

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section WithPack
variable {Kc : Divisor K F} {g : ℕ}

Lean source · statement

theorem exists_finset_forall_ell_sub_single_add_one_eq [IsAlgClosed K] [IsCurveOver K F]
    (hRR : ∀ D : Divisor K F, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g)
    (P : Place K F) {G : Divisor K F} (hG : 0 < ell G) :
    ∃ S : Finset (Place K F), ∀ Q ∉ S, ell (G - Finsupp.single Q 1) + 1 = ell G

theorem

eq_zero_of_effective_of_degree_eq_zero

L376 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add.AlgebraicCurve.WStabImpl.eq_zero_of_effective_of_degree_eq_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WStabImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem eq_zero_of_effective_of_degree_eq_zero [IsCurveOver K F] {D : Divisor K F}
    (hD : ∀ v, 0 ≤ D v) (hdeg : Divisor.degree D = 0) : D = 0

theorem

ell_pos_of_effective

L391 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add.AlgebraicCurve.WStabImpl.ell_pos_of_effective

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WStabImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ell_pos_of_effective [IsCurveOver K F] {Kc : Divisor K F} {g : ℕ}
    (hRR : ∀ D : Divisor K F, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g)
    (P : Place K F) {E : Divisor K F} (hE : ∀ v, 0 ≤ E v) : 0 < ell E

theorem

mem_principal_of_ell_pos

L399 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add.AlgebraicCurve.WStabImpl.mem_principal_of_ell_pos

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WStabImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mem_principal_of_ell_pos [IsCurveOver K F] {ξ : Divisor K F}
    (hξ : Divisor.degree ξ = 0) (hpos : 0 < ell ξ) :
    ξ ∈ Divisor.principal (K := K) (F := F)

theorem

mem_principal_of_forall_ell_pos_add_impl

L416 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add.AlgebraicCurve.WStabImpl.mem_principal_of_forall_ell_pos_add_impl

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace WStabImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mem_principal_of_forall_ell_pos_add_impl [IsAlgClosed K] [IsCurveOver K F]
    (Kc : Divisor K F) (g : ℕ)
    (hRR : ∀ D : Divisor K F, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g)
    (ξ : Divisor K F) (hξ : Divisor.degree ξ = 0)
    (h : ∀ D : Divisor K F, Divisor.degree D = (g : ℤ) - 1 → 0 < ell D → 0 < ell (D + ξ)) :
    ξ ∈ Divisor.principal (K := K) (F := F)

theorem

mem_principal_of_forall_ell_pos_add

L490 ↗

AlgebraicCurve.Divisor.mem_principal_of_forall_ell_pos_add

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_mem_principal_of_forall_ell_pos_add
universe u v
open _root_.AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.Divisor.mem_principal_of_forall_ell_pos_add
    {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F] [IsAlgClosed K]
    [IsCurveOver K F] [Algebra.EssFiniteType K F] (Kc : Divisor K F) (g : ℕ)
    (hRR : ∀ D : Divisor K F, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g)
    (ξ : Divisor K F) (hξ : Divisor.degree ξ = 0)
    (h : ∀ D : Divisor K F, Divisor.degree D = (g : ℤ) - 1 → 0 < ell D → 0 < ell (D + ξ)) :
    ξ ∈ Divisor.principal (K := K) (F := F)

Module documentation

Divisor mem principal of forall ell pos add

Declarations