NYLL
Module

RROpens_exists_finset_subset_ell_sub_sum_single_eq_zero.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.RROpens_exists_finset_subset_ell_sub_sum_single_eq_zero
16 declarations indexed from sourceView source ↗

Module documentation

RROpens exists finset subset ell sub sum single eq zero

Imports4
Imported by2

Declarations

theorem

ord_nonneg_of_mem

L38 ↗
AlgebraicCurve.Place.ord_nonneg_of_mem
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.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

L55 ↗
AlgebraicCurve.Place.mem_of_ord_nonneg
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub
universe u v
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.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

L81 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub.AlgebraicCurve.RROpensImpl.mk_mem_maximalIdeal_iff
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.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

L107 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub.AlgebraicCurve.RROpensImpl.ell_le_ell_sub_single_add_deg
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.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

L199 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub.AlgebraicCurve.RROpensImpl.one_le_deg
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.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

L203 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub.AlgebraicCurve.RROpensImpl.degree_eq_sum_support
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.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

L213 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub.AlgebraicCurve.RROpensImpl.ell_canonical_eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.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

L221 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub.AlgebraicCurve.RROpensImpl.degree_add_one_sub_le_ell
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.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

L228 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub.AlgebraicCurve.RROpensImpl.finite_lSpace
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.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

L257 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub.AlgebraicCurve.RROpensImpl.exists_ord_pos_of_ord_neg
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.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

L278 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub.AlgebraicCurve.RROpensImpl.infinite_place_of_pole
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.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

L318 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub.AlgebraicCurve.RROpensImpl.infinite_place
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.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

L329 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub.AlgebraicCurve.RROpensImpl.ell_sub_single_add_one_eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.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

L355 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub.AlgebraicCurve.RROpensImpl.exists_finset_forall_ell_sub_single_add_one_eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.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

exists_finset_subset_ell_sub_sum_single_eq_zero_impl

L379 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub.AlgebraicCurve.RROpensSubsetImpl.exists_finset_subset_ell_sub_sum_single_eq_zero_impl
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub
universe u v
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensSubsetImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_finset_subset_ell_sub_sum_single_eq_zero_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)
    (G : Divisor K F) (S : Set (Place K F)) (hS : S.Infinite) :
    ∃ T : Finset (Place K F), (↑T : Set (Place K F)) ⊆ S ∧ T.card = ell G ∧
      ell (G - ∑ v ∈ T, Finsupp.single v 1) = 0
theorem

exists_finset_subset_ell_sub_sum_single_eq_zero

L426 ↗
AlgebraicCurve.RROpens.exists_finset_subset_ell_sub_sum_single_eq_zero
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsFinsetSubsetEllSub
universe u v
open _root_.AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.RROpens.exists_finset_subset_ell_sub_sum_single_eq_zero
    {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F] [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)
    (G : Divisor K F) (S : Set (Place K F)) (hS : S.Infinite) :
    ∃ T : Finset (Place K F), (↑T : Set (Place K F)) ⊆ S ∧ T.card = ell G ∧
      ell (G - ∑ v ∈ T, Finsupp.single v 1) = 0

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