Module

Mul_mem_lSpace_add.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Mul_mem_lSpace_add

90 declarations indexed from sourceView source ↗

Module documentation

Mul mem l Space add

Imports6

Imported by3

theorem

ord_nonneg_of_mem

L35 ↗

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.MulMemLSpaceAdd
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

L51 ↗

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.MulMemLSpaceAdd
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

L60 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L74 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L80 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L84 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L100 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L124 ↗

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.MulMemLSpaceAdd
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

L154 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L246 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L250 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L287 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L296 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L330 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L368 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L396 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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'

L415 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L441 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L552 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L562 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L623 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L627 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L633 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L644 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.lSpaceQuotientToAdeleBddQuotient_injective

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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

L657 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L676 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L681 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L686 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L710 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L717 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L747 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L752 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L756 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L760 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.adeleBddPrincipal_mono

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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

L769 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.finiteDimensional_lSpace

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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

L789 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.range_lSpaceQuotientToAdeleBddQuotient

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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

L830 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L901 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L929 ↗

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.MulMemLSpaceAdd
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

L944 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L960 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L971 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L1018 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L1027 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L1049 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.adeleSpaceMul_add

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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

L1055 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.adeleSpaceMul_zero

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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

L1061 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L1067 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L1073 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L1080 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L1085 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L1092 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L1102 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L1108 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L1116 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.doubleResiduePairing_injective

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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

L1143 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L1175 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L1189 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L1225 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L1238 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L1282 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

L1299 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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

indexOfSpecialty_sub_of_ge

L1307 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.indexOfSpecialty_sub_of_ge

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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 indexOfSpecialty_sub_of_ge [IsCurveOver K F] [Nonempty (Place K F)]
    {D₀ D : Divisor K F} (hD : D₀ ≤ D)
    [FiniteDimensional K (LSpace D)]
    [hfin : Module.Finite K (adeleSpace K F ⧸ adeleBddPrincipal K F D₀)] :
    Module.Finite K (adeleSpace K F ⧸ adeleBddPrincipal K F D) ∧
      (Divisor.degree D - ell D) - (Divisor.degree D₀ - ell D₀)
        = (indexOfSpecialty D₀ : ℤ) - (indexOfSpecialty D : ℤ)

theorem

degreeSub_ell_le_of_indexFinite

L1351 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.degreeSub_ell_le_of_indexFinite

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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 degreeSub_ell_le_of_indexFinite [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {D₀ : Divisor K F}
    (hfin : Module.Finite K (adeleSpace K F ⧸ adeleBddPrincipal K F D₀))
    (D : Divisor K F) :
    Divisor.degree D - ell D ≤ (Divisor.degree D₀ - ell D₀) + indexOfSpecialty D₀

theorem

riemannGenusBounded_of_indexFinite

L1368 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.riemannGenusBounded_of_indexFinite

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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 riemannGenusBounded_of_indexFinite [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (hfin : IndexOfSpecialtyFinite K F) :
    RiemannGenusBounded K F

theorem

stichtenothGenusExists_of_indexFinite

L1376 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.stichtenothGenusExists_of_indexFinite

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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_indexFinite
    [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (hfin : IndexOfSpecialtyFinite K F) :
    StichtenothGenusExists K F

theorem

indexOfSpecialtyFinite_of_stichtenothGenusExists

L1383 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.indexOfSpecialtyFinite_of_stichtenothGenusExists

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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 indexOfSpecialtyFinite_of_stichtenothGenusExists
    [IsCurveOver K F] (hSG : StichtenothGenusExists K F) :
    IndexOfSpecialtyFinite K F

theorem

stichtenothGenusExists_iff_indexFinite

L1397 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.stichtenothGenusExists_iff_indexFinite

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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_iff_indexFinite
    [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))] :
    StichtenothGenusExists K F ↔ IndexOfSpecialtyFinite K F

theorem

gate_indexOfSpecialty_engine_at_witness

L1404 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.gate_indexOfSpecialty_engine_at_witness

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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 gate_indexOfSpecialty_engine_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_stichtenothGenus_le_of_indexFinite

L1410 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.gate_stichtenothGenus_le_of_indexFinite

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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 gate_stichtenothGenus_le_of_indexFinite [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {D₀ : Divisor K F}
    (hfin : Module.Finite K (adeleSpace K F ⧸ adeleBddPrincipal K F D₀))
    {γ : ℤ} {D₁ : Divisor K F} (h : RiemannGenusReachedAt γ D₁) :
    γ - 1 ≤ (Divisor.degree D₀ - ell D₀) + indexOfSpecialty D₀

theorem

gate_riemannGenusBounded_of_reachedAt

L1419 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.gate_riemannGenusBounded_of_reachedAt

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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 gate_riemannGenusBounded_of_reachedAt
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    RiemannGenusBounded K F

theorem

gate_indexOfSpecialtyFinite_at_zero

L1424 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.gate_indexOfSpecialtyFinite_at_zero

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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 gate_indexOfSpecialtyFinite_at_zero [IsCurveOver K F] [Nonempty (Place K F)]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    Module.Finite K (adeleSpace K F ⧸ adeleBddPrincipal K F (0 : Divisor K F))

theorem

mul_mem_lSpace_add_port

L1444 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.mul_mem_lSpace_add_port

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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_port {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

L1457 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.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.MulMemLSpaceAdd
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)

theorem

pow_mul_u_mem_lSpace

L1471 ↗

AlgebraicCurve.PoleDivisorPackage.pow_mul_u_mem_lSpace

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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 PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
variable (P : PoleDivisorPackage K F)

Lean source · statement

theorem _root_.AlgebraicCurve.PoleDivisorPackage.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

L1479 ↗

AlgebraicCurve.PoleDivisorPackage.pow_mul_u_mem_lSpace_of_le

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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 PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
variable (P : PoleDivisorPackage K F)
open _root_.AlgebraicCurve.PoleDivisorPackage

Lean source · statement

theorem _root_.AlgebraicCurve.PoleDivisorPackage.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

L1491 ↗

AlgebraicCurve.PoleDivisorPackage.ell_nsmul_poleDivisor_ge

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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 PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
variable (P : PoleDivisorPackage K F)
open _root_.AlgebraicCurve.PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage

Lean source · statement

theorem _root_.AlgebraicCurve.PoleDivisorPackage.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

L1519 ↗

AlgebraicCurve.PoleDivisorPackage.degree_nsmul_sub_ell_le

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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 PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
variable (P : PoleDivisorPackage K F)
open _root_.AlgebraicCurve.PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage
open _root_.AlgebraicCurve.PoleDivisorPackage

Lean source · statement

theorem _root_.AlgebraicCurve.PoleDivisorPackage.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

L1536 ↗

AlgebraicCurve.PoleDivisorPackage.ell_nsmul_sub_pos

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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 PoleDivisorPackage
open scoped _root_.AlgebraicCurve.PoleDivisorPackage in

Lean source · statement

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

L1557 ↗

AlgebraicCurve.PoleDivisorPackage.degree_sub_ell_le

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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
namespace PoleDivisorPackage
open scoped _root_.AlgebraicCurve.PoleDivisorPackage in

Lean source · statement

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

L1606 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.riemannGenusBounded_of_poleDivisorPackage

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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
open _root_.AlgebraicCurve

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

L1612 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.stichtenothGenusExists_of_poleDivisorPackage

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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
open _root_.AlgebraicCurve

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

indexOfSpecialtyFinite_of_poleDivisorPackage

L1618 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.indexOfSpecialtyFinite_of_poleDivisorPackage

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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
open _root_.AlgebraicCurve

Lean source · statement

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

theorem

indexOfSpecialtyFinite_of_hasPoleDivisorPackage

L1625 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.indexOfSpecialtyFinite_of_hasPoleDivisorPackage

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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
open _root_.AlgebraicCurve

Lean source · statement

theorem indexOfSpecialtyFinite_of_hasPoleDivisorPackage [IsCurveOver K F]
    [Nonempty (Place K F)] [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (h : HasPoleDivisorPackage K F) :
    IndexOfSpecialtyFinite K F

theorem

stichtenothGenusExists_of_hasPoleDivisorPackage

L1631 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.stichtenothGenusExists_of_hasPoleDivisorPackage

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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
open _root_.AlgebraicCurve

Lean source · statement

theorem stichtenothGenusExists_of_hasPoleDivisorPackage [IsCurveOver K F]
    [Nonempty (Place K F)] [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (h : HasPoleDivisorPackage K F) :
    StichtenothGenusExists K F

theorem

gate_stichtenothGenus_le_of_poleDivisorPackage

L1637 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.gate_stichtenothGenus_le_of_poleDivisorPackage

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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
open _root_.AlgebraicCurve

Lean source · statement

theorem gate_stichtenothGenus_le_of_poleDivisorPackage [IsCurveOver K F]
    [Nonempty (Place K F)] [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (P : PoleDivisorPackage K F)
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀) :
    γ ≤ (P.n : ℤ) * (P.c - 1) + 1

theorem

gate_ell_c_nsmul_ge

L1645 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.gate_ell_c_nsmul_ge

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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
open _root_.AlgebraicCurve

Lean source · statement

theorem gate_ell_c_nsmul_ge [IsCurveOver K F]
    [FiniteDimensional K (LSpace (0 : Divisor K F))]
    (P : PoleDivisorPackage K F) :
    (P.n : ℤ) ≤ ell (P.c • P.B)

theorem

gate_x_transcendental_of_poleDivisorPackage

L1653 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.gate_x_transcendental_of_poleDivisorPackage

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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
open _root_.AlgebraicCurve

Lean source · full declaration

theorem gate_x_transcendental_of_poleDivisorPackage (P : PoleDivisorPackage K F) :
    LinearIndependent K (fun j : ℕ => P.x ^ j * P.u ⟨0, P.hn_pos⟩) := by
  refine P.lin_indep.comp (fun j => (j, ⟨0, P.hn_pos⟩)) ?_
  intro a b hab
  exact (Prod.mk.injEq .. ▸ hab).1

theorem

gate_u_linearIndependent_of_poleDivisorPackage

L1659 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd.AlgebraicCurve.gate_u_linearIndependent_of_poleDivisorPackage

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.MulMemLSpaceAdd
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
open _root_.AlgebraicCurve

Lean source · statement

theorem gate_u_linearIndependent_of_poleDivisorPackage (P : PoleDivisorPackage K F) :
    LinearIndependent K P.u

theorem

mul_mem_lSpace_add

L1673 ↗

AlgebraicCurve.mul_mem_lSpace_add

Source context 3 commands

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

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

Lean source · statement

theorem _root_.AlgebraicCurve.mul_mem_lSpace_add {K : Type*} {F : Type*} [Field K] [Field F]
  [Algebra K F] {D E : Divisor K F} {f g : F}
    (hf : f ∈ LSpace D) (hg : g ∈ LSpace E) :
    f * g ∈ LSpace (D + E)

Module documentation

Mul mem l Space add

Declarations