NYLL
Module

OmegaSpace_finite_of_genusReached.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.OmegaSpace_finite_of_genusReached
61 declarations indexed from sourceView source ↗

Module documentation

Finiteness of differential-dual spaces from a place where the genus is reached. Adelic quotient and residue-pairing comparisons give the dimension bounds.

Imports4
Imported by2

Declarations

theorem

ord_nonneg_of_mem

L34 ↗
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.OmegaSpace_finite_of_genusReached
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

L50 ↗
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.OmegaSpace_finite_of_genusReached
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

L59 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L73 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L79 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L83 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L99 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L123 ↗
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.OmegaSpace_finite_of_genusReached
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

L153 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L245 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L249 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L286 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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.OmegaSpace_finite_of_genusReached.AlgebraicCurve.lSpaceShiftEquiv
Documentation

Identify divisor-bounded spaces after translating by the divisor of the nonzero function.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached
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.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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.OmegaSpace_finite_of_genusReached.Submodule.nestedComapMapMkQEquiv
Documentation

Identify a nested submodule image in a quotient with its quotient by the smaller submodule.

Source context 11 commands

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

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

L438 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.AlgebraicCurve.adeleBddQuotSingleEquivResidueField
Documentation

Identify the single-place bounded adelic quotient with the residue field at that place.

Source context 11 commands

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

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

L549 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L559 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L620 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L624 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L632 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.AlgebraicCurve.lSpaceQuotientToAdeleBddQuotient
Documentation

Map the quotient of divisor-bounded function spaces to the corresponding bounded adelic quotient.

Source context 11 commands

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

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

L643 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.AlgebraicCurve.lSpaceQuotientToAdeleBddQuotient_injective
Source context 11 commands

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

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

L656 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L675 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L680 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L685 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L709 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L716 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L746 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L751 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L755 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L759 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.AlgebraicCurve.adeleBddPrincipal_mono
Source context 8 commands

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

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

L768 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.AlgebraicCurve.finiteDimensional_lSpace
Source context 11 commands

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

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

L788 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.AlgebraicCurve.range_lSpaceQuotientToAdeleBddQuotient
Source context 8 commands

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

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

L829 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L900 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L928 ↗
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.OmegaSpace_finite_of_genusReached
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

L943 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L959 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L970 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L1017 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L1026 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L1048 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.AlgebraicCurve.adeleSpaceMul_add
Source context 8 commands

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

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

L1054 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.AlgebraicCurve.adeleSpaceMul_zero
Source context 8 commands

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

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

L1060 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L1066 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L1072 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L1079 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L1084 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L1091 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L1101 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.AlgebraicCurve.doubleResiduePairing
Documentation

Combine two residue pairings by adding the two Weil scalar multiples.

Source context 9 commands

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

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

L1107 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L1115 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.AlgebraicCurve.doubleResiduePairing_injective
Source context 9 commands

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

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

L1142 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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_port

L1174 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.AlgebraicCurve.omegaSpace_finite_of_genusReached_port
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached
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_port
    {γ : ℤ} {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

L1188 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L1224 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

L1237 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached.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.OmegaSpace_finite_of_genusReached
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

omegaSpace_finite_of_genusReached

L1273 ↗
AlgebraicCurve.omegaSpace_finite_of_genusReached
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpace_finite_of_genusReached
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs in
open _root_.AlgebraicCurve OmegaSpace_finite_of_genusReached.AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.omegaSpace_finite_of_genusReached {K F : Type*} [Field K] [Field F]
    [Algebra K F] [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 ↥(omegaSpace (K := K) (F := F) D)

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