Module

IndexOfSpecialty_eq_ell_sub_of_rankOne_max.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.IndexOfSpecialty_eq_ell_sub_of_rankOne_max

78 declarations indexed from sourceView source ↗

Module documentation

Index Of Specialty eq ell sub of rank One max

Imports4

Imported by2

theorem

ord_nonneg_of_mem

L33 ↗

AlgebraicCurve.Place.ord_nonneg_of_mem

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [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

L49 ↗

AlgebraicCurve.Place.mem_of_ord_nonneg

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [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

mem_iff_ord_nonneg

L58 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.Place.mem_iff_ord_nonneg

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem mem_iff_ord_nonneg {f : F} (hf : f ≠ 0) :
    f ∈ v.toValuationSubring ↔ 0 ≤ v.ord f

theorem

degree_eq_sum_support

L72 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.Divisor.degree_eq_sum_support

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open scoped _root_.AlgebraicCurve.Divisor in

Lean source · statement

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

theorem

degree_nonneg_of_nonneg

L78 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.Divisor.degree_nonneg_of_nonneg

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D : Divisor K F}
open scoped _root_.AlgebraicCurve.Divisor in

Lean source · statement

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

theorem

lSpace_eq_bot_of_degree_neg

L82 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.lSpace_eq_bot_of_degree_neg

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D : Divisor K F}

Lean source · statement

theorem lSpace_eq_bot_of_degree_neg [IsCurveOver K F]
    (hD : Divisor.degree D < 0) : LSpace D = ⊥

theorem

ell_eq_zero_of_degree_neg

L98 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.ell_eq_zero_of_degree_neg

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D : Divisor K F}

Lean source · statement

theorem ell_eq_zero_of_degree_neg [IsCurveOver K F] (hD : Divisor.degree D < 0) :
    ell D = 0

theorem

mk_mem_maximalIdeal_iff

L122 ↗

AlgebraicCurve.Place.mk_mem_maximalIdeal_iff

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F)

Lean source · statement

theorem _root_.AlgebraicCurve.Place.mk_mem_maximalIdeal_iff {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

L152 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.ell_le_ell_sub_single_add_deg

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [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

L244 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.one_le_deg

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [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

ell_le_degree_add_ellZero

L248 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.ell_le_degree_add_ellZero

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ell_le_degree_add_ellZero [IsCurveOver K F] {D : Divisor K F}
    (hD : ∀ v, 0 ≤ D v) :
    (ell D : ℤ) ≤ Divisor.degree D + ell (0 : Divisor K F)

theorem

ell_le_degree_add_one_of_effective

L285 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.ell_le_degree_add_one_of_effective

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ell_le_degree_add_one_of_effective [IsCurveOver K F]
    (hC : ConstantsAreBase K F) {D : Divisor K F} (hD : ∀ v, 0 ≤ D v) :
    (ell D : ℤ) ≤ Divisor.degree D + 1

def

lSpaceShiftEquiv

L294 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.lSpaceShiftEquiv

Documentation

Multiplication by the inverse of g identifies the spaces for divisors differing by its divisor.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

def lSpaceShiftEquiv (D : Divisor K F) {g : F} (hg : g ≠ 0)
    {Dg : Divisor K F} (hDg : ∀ v, Dg v = v.ord g) :
    LSpace D ≃ₗ[K] LSpace (D + Dg) where
  toFun h := ⟨(h : F) * g⁻¹, by
    rw [mem_lSpace_iff_ord]
    rcases eq_or_ne (h : F) 0 with hh0 | hh0
    · left; rw [hh0, zero_mul]
    · right; intro v
      rw [Finsupp.add_apply, hDg, v.ord_mul hh0 (inv_ne_zero hg), v.ord_inv]
      have := (mem_lSpace_iff_ord.mp h.2).resolve_left hh0 v
      linarith⟩
  invFun k := ⟨(k : F) * g, by
    rw [mem_lSpace_iff_ord]
    rcases eq_or_ne (k : F) 0 with hk0 | hk0
    · left; rw [hk0, zero_mul]
    · right; intro v
      have := (mem_lSpace_iff_ord.mp k.2).resolve_left hk0 v
      rw [Finsupp.add_apply, hDg] at this
      rw [v.ord_mul hk0 hg]
      linarith⟩
  map_add' h₁ h₂ := by apply Subtype.ext; push_cast; ring
  map_smul' c h := by
    apply Subtype.ext
    simp only [RingHom.id_apply, SetLike.val_smul, Algebra.smul_def]
    ring
  left_inv h := by
    apply Subtype.ext
    change (h : F) * g⁻¹ * g = (h : F)
    rw [mul_assoc, inv_mul_cancel₀ hg, mul_one]
  right_inv k := by
    apply Subtype.ext
    change (k : F) * g * g⁻¹ = (k : F)
    rw [mul_assoc, mul_inv_cancel₀ hg, mul_one]

theorem

ell_le_degree_add_one

L328 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.ell_le_degree_add_one

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ell_le_degree_add_one [IsCurveOver K F] (hC : ConstantsAreBase K F)
    {D : Divisor K F} (hD : 0 ≤ Divisor.degree D) :
    (ell D : ℤ) ≤ Divisor.degree D + 1

def

nestedComapMapMkQEquiv

L366 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.Submodule.nestedComapMapMkQEquiv

Documentation

Identify the image of B in the quotient of C by A with the induced quotient of B.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace Submodule
open _root_.Submodule
open _root_.Submodule
variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]

Lean source · statement

def nestedComapMapMkQEquiv {A B C : Submodule K X} (_hAB : A ≤ B) (hBC : B ≤ C) :
    ((B.comap C.subtype).map (A.comap C.subtype).mkQ : Submodule K _)
      ≃ₗ[K] B ⧸ A.comap B.subtype

theorem

finrank_quotient_chain

L394 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.Submodule.finrank_quotient_chain

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace Submodule
open _root_.Submodule
open _root_.Submodule
variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]

Lean source · statement

theorem finrank_quotient_chain {A B C : Submodule K X} (hAB : A ≤ B) (hBC : B ≤ C)
    [hCB : Module.Finite K (C ⧸ B.comap C.subtype)]
    [hBA : Module.Finite K (B ⧸ A.comap B.subtype)] :
    Module.Finite K (C ⧸ A.comap C.subtype) ∧
      finrank K (C ⧸ A.comap C.subtype)
        = finrank K (C ⧸ B.comap C.subtype) + finrank K (B ⧸ A.comap B.subtype)

theorem

finrank_quotient_chain'

L413 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.Submodule.finrank_quotient_chain'

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace Submodule
open _root_.Submodule
open _root_.Submodule
variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]

Lean source · statement

theorem finrank_quotient_chain' {A B C : Submodule K X} (hAB : A ≤ B) (hBC : B ≤ C)
    [hCA : Module.Finite K (C ⧸ A.comap C.subtype)] :
    Module.Finite K (C ⧸ B.comap C.subtype) ∧
      finrank K (C ⧸ B.comap C.subtype)
        = finrank K (C ⧸ A.comap C.subtype) - finrank K (B ⧸ A.comap B.subtype)

def

adeleBddQuotSingleEquivResidueField

L439 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.adeleBddQuotSingleEquivResidueField

Documentation

The quotient obtained by lowering the bound at one place is linearly equivalent to its residue field.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def adeleBddQuotSingleEquivResidueField (D : Divisor K F) (P : Place K F) :
    (adeleBdd D ⧸ (adeleBdd (D - Finsupp.single P 1)).comap (adeleBdd D).subtype)
      ≃ₗ[K] P.ResidueField

theorem

finrank_adeleBdd_quotient_single

L550 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.finrank_adeleBdd_quotient_single

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem finrank_adeleBdd_quotient_single [IsCurveOver K F] (D : Divisor K F) (P : Place K F) :
    Module.Finite K
        (adeleBdd D ⧸ (adeleBdd (D - Finsupp.single P 1)).comap (adeleBdd D).subtype) ∧
      finrank K
          (adeleBdd D ⧸ (adeleBdd (D - Finsupp.single P 1)).comap (adeleBdd D).subtype)
        = P.deg

theorem

finrank_adeleBdd_quotient

L560 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.finrank_adeleBdd_quotient

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem finrank_adeleBdd_quotient [IsCurveOver K F] {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    Module.Finite K (adeleBdd D₂ ⧸ (adeleBdd D₁).comap (adeleBdd D₂).subtype) ∧
      (finrank K (adeleBdd D₂ ⧸ (adeleBdd D₁).comap (adeleBdd D₂).subtype) : ℤ)
        = Divisor.degree D₂ - Divisor.degree D₁

theorem

module_finite_adeleBdd_quotient

L621 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.module_finite_adeleBdd_quotient

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem module_finite_adeleBdd_quotient [IsCurveOver K F] {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    Module.Finite K (adeleBdd D₂ ⧸ (adeleBdd D₁).comap (adeleBdd D₂).subtype)

theorem

finrank_adeleBdd_quotient_eq

L625 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.finrank_adeleBdd_quotient_eq

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem finrank_adeleBdd_quotient_eq [IsCurveOver K F] {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    (finrank K (adeleBdd D₂ ⧸ (adeleBdd D₁).comap (adeleBdd D₂).subtype) : ℤ)
      = Divisor.degree D₂ - Divisor.degree D₁

def

lSpaceQuotientToAdeleBddQuotient

L631 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.lSpaceQuotientToAdeleBddQuotient

Documentation

The map between divisor-bounded quotients induced by the diagonal embedding into adeles.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def lSpaceQuotientToAdeleBddQuotient {D₁ D₂ : Divisor K F} (_hD : D₁ ≤ D₂) :
    (LSpace D₂ ⧸ (LSpace D₁).comap (LSpace D₂).subtype)
      →ₗ[K] (adeleBdd D₂ ⧸ (adeleBdd D₁).comap (adeleBdd D₂).subtype)

theorem

lSpaceQuotientToAdeleBddQuotient_injective

L642 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.lSpaceQuotientToAdeleBddQuotient_injective

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem lSpaceQuotientToAdeleBddQuotient_injective {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    Function.Injective (lSpaceQuotientToAdeleBddQuotient hD)

theorem

ell_sub_ell_le_degree_sub_degree

L655 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.ell_sub_ell_le_degree_sub_degree

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ell_sub_ell_le_degree_sub_degree [IsCurveOver K F] {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂)
    [FiniteDimensional K (LSpace D₂)] :
    (ell D₂ : ℤ) - (ell D₁ : ℤ) ≤ Divisor.degree D₂ - Divisor.degree D₁

theorem

adeleBdd_inf_sup_globalSub

L674 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.adeleBdd_inf_sup_globalSub

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem adeleBdd_inf_sup_globalSub {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    adeleBdd D₂ ⊓ (adeleBdd D₁ ⊔ globalSub K F)
      = adeleBdd D₁ ⊔ adeleBdd D₂ ⊓ globalSub K F

theorem

map_diagonal_lSpace_inf_adeleBdd

L679 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.map_diagonal_lSpace_inf_adeleBdd

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem map_diagonal_lSpace_inf_adeleBdd {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    (LSpace D₂).map (diagonalHom K F) ⊓ adeleBdd D₁ = (LSpace D₁).map (diagonalHom K F)

theorem

gate_finrank_adeleBdd_quotient_single_point

L684 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.gate_finrank_adeleBdd_quotient_single_point

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open _root_.Module
open _root_.IsLocalRing
open _root_.IsDedekindDomain
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem gate_finrank_adeleBdd_quotient_single_point [IsCurveOver K F] (P : Place K F) :
    (finrank K (adeleBdd (Finsupp.single P 1 : Divisor K F)
        ⧸ (adeleBdd (0 : Divisor K F)).comap (adeleBdd (Finsupp.single P 1)).subtype) : ℤ)
      = (P.deg : ℤ)

theorem

comap_subtype_sup_of_le_of_le

L708 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.Submodule.comap_subtype_sup_of_le_of_le

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace Submodule
open _root_.Submodule
open _root_.Submodule
variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]

Lean source · statement

theorem comap_subtype_sup_of_le_of_le {S T C : Submodule K X} (hS : S ≤ C) (hT : T ≤ C) :
    S.comap C.subtype ⊔ T.comap C.subtype = (S ⊔ T).comap C.subtype

theorem

finrank_quotient_chain_top

L715 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.Submodule.finrank_quotient_chain_top

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace Submodule
open _root_.Submodule
open _root_.Submodule
variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]

Lean source · statement

theorem finrank_quotient_chain_top {M : Type*} [AddCommGroup M] [Module K M]
    {A B : Submodule K M} (hAB : A ≤ B)
    [hMB : Module.Finite K (M ⧸ B)] [hBA : Module.Finite K (B ⧸ A.comap B.subtype)] :
    Module.Finite K (M ⧸ A) ∧
      finrank K (M ⧸ A) = finrank K (M ⧸ B) + finrank K (B ⧸ A.comap B.subtype)

theorem

globalSub_le_adeleSpace

L745 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.globalSub_le_adeleSpace

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem globalSub_le_adeleSpace [HasPrincipalDivisors K F] :
    globalSub K F ≤ adeleSpace K F

theorem

adeleBdd_sup_globalSub_le_adeleSpace

L750 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.adeleBdd_sup_globalSub_le_adeleSpace

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem adeleBdd_sup_globalSub_le_adeleSpace [HasPrincipalDivisors K F] (D : Divisor K F) :
    adeleBdd D ⊔ globalSub K F ≤ adeleSpace K F

theorem

adeleBddPrincipal_eq_comap

L754 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.adeleBddPrincipal_eq_comap

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem adeleBddPrincipal_eq_comap [HasPrincipalDivisors K F] (D : Divisor K F) :
    adeleBddPrincipal K F D = (adeleBdd D ⊔ globalSub K F).comap (adeleSpace K F).subtype

theorem

adeleBddPrincipal_mono

L758 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.adeleBddPrincipal_mono

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem adeleBddPrincipal_mono {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    adeleBddPrincipal K F D₁ ≤ adeleBddPrincipal K F D₂

theorem

finiteDimensional_lSpace

L767 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.finiteDimensional_lSpace

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section FiniteLSpace
variable [IsCurveOver K F] [Nonempty (Place K F)]
omit [Nonempty (Place K F)] in

Lean source · statement

theorem finiteDimensional_lSpace [hL0 : FiniteDimensional K (LSpace (0 : Divisor K F))]
    (D : Divisor K F) : FiniteDimensional K (LSpace D)

theorem

range_lSpaceQuotientToAdeleBddQuotient

L787 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.range_lSpaceQuotientToAdeleBddQuotient

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem range_lSpaceQuotientToAdeleBddQuotient {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) :
    LinearMap.range (lSpaceQuotientToAdeleBddQuotient hD)
      = ((adeleBdd D₁ ⊔ globalSub K F).comap (adeleBdd D₂).subtype).map
          ((adeleBdd D₁).comap (adeleBdd D₂).subtype).mkQ

theorem

finrank_adeleBddSup_quotient

L828 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.finrank_adeleBddSup_quotient

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem finrank_adeleBddSup_quotient [IsCurveOver K F] [Nonempty (Place K F)]
    {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂) [hL : FiniteDimensional K (LSpace D₂)] :
    Module.Finite K (↥(adeleBdd D₂ ⊔ globalSub K F)
        ⧸ (adeleBdd D₁ ⊔ globalSub K F).comap (adeleBdd D₂ ⊔ globalSub K F).subtype) ∧
      (finrank K (↥(adeleBdd D₂ ⊔ globalSub K F)
          ⧸ (adeleBdd D₁ ⊔ globalSub K F).comap (adeleBdd D₂ ⊔ globalSub K F).subtype) : ℤ)
        = (Divisor.degree D₂ - ell D₂) - (Divisor.degree D₁ - ell D₁)

theorem

adeleBddSup_eq_of_degree_sub_ell_eq

L899 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.adeleBddSup_eq_of_degree_sub_ell_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Index
variable [IsCurveOver K F] [Nonempty (Place K F)]

Lean source · statement

theorem adeleBddSup_eq_of_degree_sub_ell_eq {D₁ D₂ : Divisor K F} (hD : D₁ ≤ D₂)
    [FiniteDimensional K (LSpace D₂)]
    (heq : Divisor.degree D₂ - ell D₂ = Divisor.degree D₁ - ell D₁) :
    adeleBdd D₂ ⊔ globalSub K F = adeleBdd D₁ ⊔ globalSub K F

theorem

eq_of_ge

L927 ↗

AlgebraicCurve.RiemannGenusReachedAt.eq_of_ge

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace RiemannGenusReachedAt
open scoped _root_.AlgebraicCurve.RiemannGenusReachedAt in

Lean source · statement

theorem _root_.AlgebraicCurve.RiemannGenusReachedAt.eq_of_ge [IsCurveOver K F] [Nonempty
  (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀)
    {D : Divisor K F} (hD : D₀ ≤ D) :
    Divisor.degree D - ell D = γ - 1

theorem

adeleSpace_eq_of_genusReached

L942 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.adeleSpace_eq_of_genusReached

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve

Lean source · statement

theorem adeleSpace_eq_of_genusReached [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    adeleSpace K F = adeleBdd D₀ ⊔ globalSub K F

theorem

indexOfSpecialty_eq_zero_of_genusReached

L958 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.indexOfSpecialty_eq_zero_of_genusReached

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve

Lean source · statement

theorem indexOfSpecialty_eq_zero_of_genusReached [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    indexOfSpecialty D₀ = 0

theorem

indexOfSpecialty_eq_of_genusReached

L969 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.indexOfSpecialty_eq_of_genusReached

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve

Lean source · statement

theorem indexOfSpecialty_eq_of_genusReached [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) (D : Divisor K F) :
    Module.Finite K (adeleSpace K F ⧸ adeleBddPrincipal K F D) ∧
      (indexOfSpecialty D : ℤ) = (ell D : ℤ) - (Divisor.degree D + 1 - γ)

theorem

gate_indexOfSpecialty_at_witness

L1016 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.gate_indexOfSpecialty_at_witness

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve

Lean source · statement

theorem gate_indexOfSpecialty_at_witness [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    (indexOfSpecialty D₀ : ℤ) = 0

theorem

gate_riemannInequality_of_genusReached

L1025 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.gate_riemannInequality_of_genusReached

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve

Lean source · statement

theorem gate_riemannInequality_of_genusReached [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) (D : Divisor K F) :
    Divisor.degree D + 1 - γ ≤ (ell D : ℤ)

theorem

adeleSpaceMul_add

L1047 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.adeleSpaceMul_add

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem adeleSpaceMul_add [HasPrincipalDivisors K F] (f g : F) :
    adeleSpaceMul K F (f + g) = adeleSpaceMul K F f + adeleSpaceMul K F g

theorem

adeleSpaceMul_zero

L1053 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.adeleSpaceMul_zero

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem adeleSpaceMul_zero [HasPrincipalDivisors K F] :
    adeleSpaceMul K F (0 : F) = 0

theorem

weilSmul_add_left

L1059 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.weilSmul_add_left

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem weilSmul_add_left [HasPrincipalDivisors K F] (f g : F)
    (φ : Module.Dual K (adeleSpace K F)) :
    weilSmul K F (f + g) φ = weilSmul K F f φ + weilSmul K F g φ

theorem

weilSmul_zero_left

L1065 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.weilSmul_zero_left

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem weilSmul_zero_left [HasPrincipalDivisors K F]
    (φ : Module.Dual K (adeleSpace K F)) :
    weilSmul K F (0 : F) φ = 0

theorem

weilSmul_neg_left

L1071 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.weilSmul_neg_left

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem weilSmul_neg_left [HasPrincipalDivisors K F] (f : F)
    (φ : Module.Dual K (adeleSpace K F)) :
    weilSmul K F (-f) φ = -weilSmul K F f φ

theorem

weilSmul_sub_left

L1078 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.weilSmul_sub_left

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem weilSmul_sub_left [HasPrincipalDivisors K F] (f g : F)
    (φ : Module.Dual K (adeleSpace K F)) :
    weilSmul K F (f - g) φ = weilSmul K F f φ - weilSmul K F g φ

theorem

weilSmul_eq_zero_iff_left

L1083 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.weilSmul_eq_zero_iff_left

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem weilSmul_eq_zero_iff_left [HasPrincipalDivisors K F]
    {f : F} {φ : Module.Dual K (adeleSpace K F)} (hφ : φ ≠ 0) :
    weilSmul K F f φ = 0 ↔ f = 0

theorem

weilSmul_left_injective

L1090 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.weilSmul_left_injective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

theorem weilSmul_left_injective [HasPrincipalDivisors K F]
    {φ : Module.Dual K (adeleSpace K F)} (hφ : φ ≠ 0) :
    Function.Injective (fun f : F => weilSmul K F f φ) := by
  intro f g hfg
  have hsub : weilSmul K F (f - g) φ = 0 := by
    rw [weilSmul_sub_left, sub_eq_zero]; exact hfg
  exact sub_eq_zero.mp ((weilSmul_eq_zero_iff_left hφ).mp hsub)

def

doubleResiduePairing

L1100 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.doubleResiduePairing

Documentation

The sum of the two residue pairings on the product of their spaces of sections.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in

Lean source · statement

def doubleResiduePairing [HasPrincipalDivisors K F] (W D : Divisor K F)
    {φ μ : Module.Dual K (adeleSpace K F)}
    (hφ : φ ∈ omegaSpace W) (hμ : μ ∈ omegaSpace W) :
    LSpace (W - D) × LSpace (W - D) →ₗ[K] omegaSpace D

theorem

doubleResiduePairing_apply_coe

L1106 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.doubleResiduePairing_apply_coe

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in

Lean source · statement

theorem doubleResiduePairing_apply_coe [HasPrincipalDivisors K F] (W D : Divisor K F)
    {φ μ : Module.Dual K (adeleSpace K F)}
    (hφ : φ ∈ omegaSpace W) (hμ : μ ∈ omegaSpace W) (g h : LSpace (W - D)) :
    (doubleResiduePairing K F W D hφ hμ (g, h) : Module.Dual K (adeleSpace K F))
      = weilSmul K F (g : F) φ + weilSmul K F (h : F) μ

theorem

doubleResiduePairing_injective

L1114 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.doubleResiduePairing_injective

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in

Lean source · statement

theorem doubleResiduePairing_injective [HasPrincipalDivisors K F] (W D : Divisor K F)
    {φ μ : Module.Dual K (adeleSpace K F)}
    (hφ : φ ∈ omegaSpace W) (hμ : μ ∈ omegaSpace W)
    (hφ0 : φ ≠ 0) (hindep : ∀ f : F, μ ≠ weilSmul K F f φ) :
    Function.Injective (doubleResiduePairing K F W D hφ hμ)

theorem

two_mul_ell_le_indexOfSpecialty

L1141 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.two_mul_ell_le_indexOfSpecialty

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in

Lean source · statement

theorem two_mul_ell_le_indexOfSpecialty [HasPrincipalDivisors K F] (W D : Divisor K F)
    {φ μ : Module.Dual K (adeleSpace K F)}
    (hφ : φ ∈ omegaSpace W) (hμ : μ ∈ omegaSpace W)
    (hφ0 : φ ≠ 0) (hindep : ∀ f : F, μ ≠ weilSmul K F f φ)
    [Module.Finite K (omegaSpace (K := K) (F := F) D)]
    [Module.Finite K (LSpace (K := K) (F := F) (W - D))] :
    2 * ell (W - D) ≤ indexOfSpecialty D

theorem

omegaSpace_finite_of_genusReached

L1173 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.omegaSpace_finite_of_genusReached

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Finiteness
variable [IsCurveOver K F] [Nonempty (Place K F)]
  [FiniteDimensional K (LSpace (0 : Divisor K F))]

Lean source · statement

theorem omegaSpace_finite_of_genusReached
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) (D : Divisor K F) :
    Module.Finite K (omegaSpace (K := K) (F := F) D)

theorem

exists_weilSmul_eq_of_genusReached

L1187 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.exists_weilSmul_eq_of_genusReached

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ParametricRankOne
variable [IsCurveOver K F] [Nonempty (Place K F)]
  [FiniteDimensional K (LSpace (0 : Divisor K F))]

Lean source · statement

theorem exists_weilSmul_eq_of_genusReached
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀)
    {φ μ : Module.Dual K (adeleSpace K F)} {W : Divisor K F}
    (hφ : φ ∈ omegaSpace W) (hμ : μ ∈ omegaSpace W) (hφ0 : φ ≠ 0) :
    ∃ f : F, μ = weilSmul K F f φ

theorem

weilDifferentialRankOne_of_genusReached

L1223 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.weilDifferentialRankOne_of_genusReached

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ParametricRankOne
variable [IsCurveOver K F] [Nonempty (Place K F)]
  [FiniteDimensional K (LSpace (0 : Divisor K F))]

Lean source · statement

theorem weilDifferentialRankOne_of_genusReached
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    WeilDifferentialRankOne K F

theorem

residuePairing_surjective_of_rankOne_max

L1236 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.residuePairing_surjective_of_rankOne_max

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem residuePairing_surjective_of_rankOne_max [HasPrincipalDivisors K F]
    (hRankOne : WeilDifferentialRankOne K F)
    {W : Divisor K F} {φ : Module.Dual K (adeleSpace K F)}
    (hφ : φ ∈ omegaSpace W) (hφ0 : φ ≠ 0)
    (hWmax : ∀ E : Divisor K F, φ ∈ omegaSpace E → E ≤ W) (D : Divisor K F) :
    Function.Surjective (residuePairing K F W D hφ)

theorem

exists_riemannGenusReachedAt_of_bounded

L1280 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.exists_riemannGenusReachedAt_of_bounded

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem exists_riemannGenusReachedAt_of_bounded
    [IsCurveOver K F] [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (hbdd : RiemannGenusBounded K F) :
    ∃ (γ : ℤ) (D₀ : Divisor K F), RiemannGenusReachedAt γ D₀

theorem

stichtenothGenusExists_of_bounded

L1297 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.stichtenothGenusExists_of_bounded

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem stichtenothGenusExists_of_bounded
    [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (hbdd : RiemannGenusBounded K F) :
    StichtenothGenusExists K F

theorem

mul_mem_lSpace_add

L1318 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.mul_mem_lSpace_add

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mul_mem_lSpace_add {D E : Divisor K F} {f g : F}
    (hf : f ∈ LSpace D) (hg : g ∈ LSpace E) :
    f * g ∈ LSpace (D + E)

theorem

pow_mem_lSpace_nsmul

L1331 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.pow_mem_lSpace_nsmul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem pow_mem_lSpace_nsmul {B : Divisor K F} {f : F} (hf : f ∈ LSpace B) (j : ℕ) :
    f ^ j ∈ LSpace (j • B)

structure

PoleDivisorPackage

L1340 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.PoleDivisorPackage

Documentation

A function and effective divisor equipped with degree and linear-independence data.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

structure PoleDivisorPackage (K F : Type*) [Field K] [Field F] [Algebra K F] where
  /-- The function whose powers are used in the independent family. -/
  x : F
  /-- The effective divisor bounding the poles of the function. -/
  B : Divisor K F
  /-- The divisor is effective. -/
  hB_eff : 0 ≤ B
  /-- The function belongs to the Riemann-Roch space of the divisor. -/
  hx_mem : x ∈ LSpace B
  /-- The positive degree of the divisor. -/
  n : ℕ
  /-- The specified degree is positive. -/
  hn_pos : 0 < n
  /-- The divisor has the specified degree. -/
  degB_eq : Divisor.degree B = n
  /-- The multiple of the divisor bounding the auxiliary functions. -/
  c : ℕ
  /-- The auxiliary family of functions. -/
  u : Fin n → F
  /-- Each auxiliary function belongs to the specified Riemann-Roch space. -/
  hu_mem : ∀ i, u i ∈ LSpace (c • B)
  /-- Products of powers of the chosen function with the auxiliary family are independent. -/
  lin_indep : LinearIndependent K (fun p : ℕ × Fin n => x ^ p.1 * u p.2)

def

HasPoleDivisorPackage

L1366 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.HasPoleDivisorPackage

Documentation

The function field admits the specified effective-divisor and independent-family data.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in

Lean source · statement

def HasPoleDivisorPackage : Prop

theorem

pow_mul_u_mem_lSpace

L1372 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.PoleDivisorPackage.pow_mul_u_mem_lSpace

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
namespace PoleDivisorPackage
variable (P : PoleDivisorPackage K F)

Lean source · statement

theorem pow_mul_u_mem_lSpace (j : ℕ) (i : Fin P.n) :
    P.x ^ j * P.u i ∈ LSpace ((j + P.c) • P.B)

theorem

pow_mul_u_mem_lSpace_of_le

L1377 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.PoleDivisorPackage.pow_mul_u_mem_lSpace_of_le

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
namespace PoleDivisorPackage
variable (P : PoleDivisorPackage K F)

Lean source · statement

theorem pow_mul_u_mem_lSpace_of_le {j m : ℕ} (hjm : j + P.c ≤ m) (i : Fin P.n) :
    P.x ^ j * P.u i ∈ LSpace (m • P.B)

theorem

ell_nsmul_poleDivisor_ge

L1387 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.PoleDivisorPackage.ell_nsmul_poleDivisor_ge

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
namespace PoleDivisorPackage
variable (P : PoleDivisorPackage K F)

Lean source · statement

theorem ell_nsmul_poleDivisor_ge [IsCurveOver K F]
    [FiniteDimensional K (LSpace (0 : Divisor K F))] {m : ℕ} (hm : P.c ≤ m) :
    (P.n : ℤ) * (m - P.c + 1) ≤ ell (m • P.B)

theorem

degree_nsmul_sub_ell_le

L1413 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.PoleDivisorPackage.degree_nsmul_sub_ell_le

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
namespace PoleDivisorPackage
variable (P : PoleDivisorPackage K F)

Lean source · statement

theorem degree_nsmul_sub_ell_le [IsCurveOver K F]
    [FiniteDimensional K (LSpace (0 : Divisor K F))] {m : ℕ} (hm : P.c ≤ m) :
    Divisor.degree (m • P.B) - ell (m • P.B) ≤ (P.n : ℤ) * (P.c - 1)

theorem

ell_nsmul_sub_pos

L1424 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.PoleDivisorPackage.ell_nsmul_sub_pos

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in

Lean source · statement

theorem PoleDivisorPackage.ell_nsmul_sub_pos [IsCurveOver K F]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (P : PoleDivisorPackage K F) {A : Divisor K F} (hA : 0 ≤ A) {m : ℕ} (hm : P.c ≤ m)
    (hbig : Divisor.degree A < (P.n : ℤ) * (m - P.c + 1)) :
    0 < ell (m • P.B - A)

theorem

degree_sub_ell_le

L1442 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.PoleDivisorPackage.degree_sub_ell_le

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in

Lean source · statement

theorem PoleDivisorPackage.degree_sub_ell_le [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (P : PoleDivisorPackage K F) (D : Divisor K F) :
    Divisor.degree D - ell D ≤ (P.n : ℤ) * (P.c - 1)

theorem

riemannGenusBounded_of_poleDivisorPackage

L1487 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.riemannGenusBounded_of_poleDivisorPackage

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in

Lean source · statement

theorem riemannGenusBounded_of_poleDivisorPackage [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (P : PoleDivisorPackage K F) :
    RiemannGenusBounded K F

theorem

stichtenothGenusExists_of_poleDivisorPackage

L1493 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.stichtenothGenusExists_of_poleDivisorPackage

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
noncomputable section
open Module IsDedekindDomain WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in

Lean source · statement

theorem stichtenothGenusExists_of_poleDivisorPackage [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (P : PoleDivisorPackage K F) :
    StichtenothGenusExists K F

theorem

weilDifferentialRankOne_of_stichtenothGenusExists

L1508 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.weilDifferentialRankOne_of_stichtenothGenusExists

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem weilDifferentialRankOne_of_stichtenothGenusExists [IsCurveOver K F]
    (h : StichtenothGenusExists K F) : WeilDifferentialRankOne K F

theorem

indexOfSpecialty_eq_ell_sub_of_rankOne_max_port

L1515 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.indexOfSpecialty_eq_ell_sub_of_rankOne_max_port

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem indexOfSpecialty_eq_ell_sub_of_rankOne_max_port [HasPrincipalDivisors K F]
    (hRankOne : WeilDifferentialRankOne K F)
    {W : Divisor K F} {φ : Module.Dual K (adeleSpace K F)}
    (hφ : φ ∈ omegaSpace W) (hφ0 : φ ≠ 0)
    (hWmax : ∀ E : Divisor K F, φ ∈ omegaSpace E → E ≤ W) (D : Divisor K F) :
    indexOfSpecialty D = ell (W - D)

theorem

exists_genus_riemannIndex_of_stichtenothGenusExists

L1526 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax.AlgebraicCurve.exists_genus_riemannIndex_of_stichtenothGenusExists

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem exists_genus_riemannIndex_of_stichtenothGenusExists [IsCurveOver K F]
    (h : StichtenothGenusExists K F) :
    ∃ γ : ℤ, ∀ D : Divisor K F,
      Module.Finite K (↥(adeleSpace K F) ⧸ adeleBddPrincipal K F D) ∧
        (indexOfSpecialty D : ℤ) = (ell D : ℤ) - (Divisor.degree D + 1 - γ)

theorem

indexOfSpecialty_eq_ell_sub_of_rankOne_max

L1537 ↗

AlgebraicCurve.indexOfSpecialty_eq_ell_sub_of_rankOne_max

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IndexOfSpecialtyEllSubRankOneMax
open _root_.AlgebraicCurve AlgebraicCurve in

Lean source · statement

theorem _root_.AlgebraicCurve.indexOfSpecialty_eq_ell_sub_of_rankOne_max {K F : Type*} [Field K]
  [Field F] [Algebra K F] [HasPrincipalDivisors K F]
    (hRankOne : WeilDifferentialRankOne K F)
    {W : Divisor K F} {φ : Module.Dual K ↥(adeleSpace K F)}
    (hφ : φ ∈ omegaSpace W) (hφ0 : φ ≠ 0)
    (hWmax : ∀ E : Divisor K F, φ ∈ omegaSpace E → E ≤ W) (D : Divisor K F) :
    indexOfSpecialty D = ell (W - D)

Module documentation

Index Of Specialty eq ell sub of rank One max

Declarations