NYLL
Module

RROpens_exists_injective_ell_sub_sum_single_eq_one_of_le_card.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.RROpens_exists_injective_ell_sub_sum_single_eq_one_of_le_card
11 declarations indexed from sourceView source ↗

Module documentation

Choose finitely many chart points whose subtraction decreases the Riemann--Roch dimension as prescribed.

Imports5
Imported by4

Declarations

theorem

one_le_deg

L43 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpens_exists_injective_ell_sub_sum_single_eq_one_of_le_card.AlgebraicCurve.RROpensFinPoolImpl.one_le_deg
Source context 11 commands

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

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

L47 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpens_exists_injective_ell_sub_sum_single_eq_one_of_le_card.AlgebraicCurve.RROpensFinPoolImpl.degree_eq_sum_support
Source context 11 commands

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

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

card_support_le_degree

L53 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpens_exists_injective_ell_sub_sum_single_eq_one_of_le_card.AlgebraicCurve.RROpensFinPoolImpl.card_support_le_degree
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs
namespace RROpens_exists_injective_ell_sub_sum_single_eq_one_of_le_card
universe u v
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensFinPoolImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem card_support_le_degree [IsCurveOver K F] {E : Divisor K F} (hE : ∀ v, 0 ≤ E v) :
    (E.support.card : ℤ) ≤ Divisor.degree E
theorem

sub_single_le

L65 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpens_exists_injective_ell_sub_sum_single_eq_one_of_le_card.AlgebraicCurve.RROpensFinPoolImpl.sub_single_le
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs
namespace RROpens_exists_injective_ell_sub_sum_single_eq_one_of_le_card
universe u v
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensFinPoolImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem sub_single_le (G : Divisor K F) (Q : Place K F) :
    G - Finsupp.single Q 1 ≤ G
theorem

degree_sub_sum_single

L73 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpens_exists_injective_ell_sub_sum_single_eq_one_of_le_card.AlgebraicCurve.RROpensFinPoolImpl.degree_sub_sum_single
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs
namespace RROpens_exists_injective_ell_sub_sum_single_eq_one_of_le_card
universe u v
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensFinPoolImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem degree_sub_sum_single (D : Divisor K F) {S T : Finset (Place K F)}
    (hS : ∀ v ∈ S, v.deg = 1) (hTS : T ⊆ S) :
    Divisor.degree (D - ∑ v ∈ T, Finsupp.single v 1) = Divisor.degree D - T.card
theorem

degree_add_one_sub_le_ell

L84 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpens_exists_injective_ell_sub_sum_single_eq_one_of_le_card.AlgebraicCurve.RROpensFinPoolImpl.degree_add_one_sub_le_ell
Source context 13 commands

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

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

L91 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpens_exists_injective_ell_sub_sum_single_eq_one_of_le_card.AlgebraicCurve.RROpensFinPoolImpl.finite_lSpace
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs
namespace RROpens_exists_injective_ell_sub_sum_single_eq_one_of_le_card
universe u v
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensFinPoolImpl
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_mem_ell_sub_single_lt

L117 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpens_exists_injective_ell_sub_sum_single_eq_one_of_le_card.AlgebraicCurve.RROpensFinPoolImpl.exists_mem_ell_sub_single_lt
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs
namespace RROpens_exists_injective_ell_sub_sum_single_eq_one_of_le_card
universe u v
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensFinPoolImpl
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_mem_ell_sub_single_lt [IsCurveOver K F]
    (hRR : ∀ D : Divisor K F, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g)
    {G : Divisor K F} (hG : 0 < ell G) (B T : Finset (Place K F))
    (hlt : Divisor.degree G + B.card < T.card) :
    ∃ Q ∈ T, Q ∉ B ∧ ell (G - Finsupp.single Q 1) < ell G
theorem

exists_subset_card_eq_ell_add_le

L160 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpens_exists_injective_ell_sub_sum_single_eq_one_of_le_card.AlgebraicCurve.RROpensFinPoolImpl.exists_subset_card_eq_ell_add_le
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs
namespace RROpens_exists_injective_ell_sub_sum_single_eq_one_of_le_card
universe u v
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensFinPoolImpl
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_subset_card_eq_ell_add_le [IsCurveOver K F]
    (hRR : ∀ D : Divisor K F, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g)
    (S : Finset (Place K F)) (hS : ∀ v ∈ S, v.deg = 1) (D : Divisor K F)
    (hDS : Divisor.degree D < S.card) :
    ∀ i : ℕ, (i : ℤ) + g ≤ Divisor.degree D + 1 →
      ∃ T : Finset (Place K F), T ⊆ S ∧ T.card = i ∧
        ell (D - ∑ v ∈ T, Finsupp.single v 1) + i ≤ ell D
theorem

exists_injective_ell_sub_sum_single_eq_one_of_le_card_impl

L193 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpens_exists_injective_ell_sub_sum_single_eq_one_of_le_card.AlgebraicCurve.RROpensFinPoolImpl.exists_injective_ell_sub_sum_single_eq_one_of_le_card_impl
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs
namespace RROpens_exists_injective_ell_sub_sum_single_eq_one_of_le_card
universe u v
noncomputable section
open Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensFinPoolImpl
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_injective_ell_sub_sum_single_eq_one_of_le_card_impl [IsCurveOver K F]
    (hRR : ∀ D : Divisor K F, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g)
    {r : ℕ} (hgr : 2 * g ≤ r + 1)
    (S : Finset (Place K F)) (hS : ∀ v ∈ S, v.deg = 1) (hcard : r + 1 ≤ S.card)
    (D : Divisor K F) (hdeg : Divisor.degree D = r) :
    ∃ f : Fin (r - g) → Place K F, Function.Injective f ∧ (∀ j, f j ∈ S) ∧
      ell (D - ∑ j : Fin (r - g), Finsupp.single (f j) 1) = 1
theorem

exists_injective_ell_sub_sum_single_eq_one_of_le_card

L247 ↗
AlgebraicCurve.RROpens.exists_injective_ell_sub_sum_single_eq_one_of_le_card
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs
namespace RROpens_exists_injective_ell_sub_sum_single_eq_one_of_le_card
universe u v
open _root_.AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.RROpens.exists_injective_ell_sub_sum_single_eq_one_of_le_card
    {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F] [IsCurveOver K F]
    {Kc : Divisor K F} {g : ℕ}
    (hRR : ∀ D : Divisor K F, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g)
    {r : ℕ} (hgr : 2 * g ≤ r + 1)
    (S : Finset (Place K F)) (hS : ∀ v ∈ S, v.deg = 1) (hcard : r + 1 ≤ S.card)
    (D : Divisor K F) (hdeg : Divisor.degree D = r) :
    ∃ f : Fin (r - g) → Place K F, Function.Injective f ∧ (∀ j, f j ∈ S) ∧
      ell (D - ∑ j : Fin (r - g), Finsupp.single (f j) 1) = 1

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