Module

FiniteDimensional_lSpace.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.FiniteDimensional_lSpace

45 declarations indexed from sourceView source ↗

Module documentation

Finite-dimensional Riemann–Roch spaces

Bounded adelic quotients and the diagonal embedding establish finite dimensionality of each Riemann–Roch space from finite dimensionality of the space for the zero divisor.

Imports5

Nyll.AlgebraicCurves.Divisors.ClassGroup
Nyll.AlgebraicCurves.Cohomology.Adelic.Repartitions
Nyll.AlgebraicCurves.FunctionFields.CurveOver
Nyll.AlgebraicCurves.Cohomology.Adelic.Index
Mathlib.Util.WithWeakNamespace

Imported by17

theorem

ord_nonneg_of_mem

L36 ↗

AlgebraicCurve.Place.ord_nonneg_of_mem

Source context 8 commands

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

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

L52 ↗

AlgebraicCurve.Place.mem_of_ord_nonneg

Source context 9 commands

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

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

L61 ↗

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

Source context 10 commands

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

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

L75 ↗

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

L81 ↗

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

L85 ↗

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

L101 ↗

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

L125 ↗

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

L155 ↗

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

L247 ↗

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

L251 ↗

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

L288 ↗

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

L297 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FiniteDimensional_lSpace.AlgebraicCurve.lSpaceShiftEquiv

Documentation

Multiplication by the inverse of a nonzero function identifies the Riemann–Roch space for D with the space for D + Dg, where Dg records the orders of that function.

Source context 11 commands

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

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

L331 ↗

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

L370 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FiniteDimensional_lSpace.Submodule.nestedComapMapMkQEquiv

Documentation

For nested submodules, identify the image of B in the quotient of C by A with the quotient of B by the induced submodule from A.

Source context 11 commands

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

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

L398 ↗

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

L417 ↗

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

L443 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FiniteDimensional_lSpace.AlgebraicCurve.adeleBddQuotSingleEquivResidueField

Documentation

Identify the quotient of bounded adeles obtained by lowering the divisor coefficient at one place by one with that place's residue field.

Source context 11 commands

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

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

L554 ↗

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

L564 ↗

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

L625 ↗

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

L629 ↗

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

L636 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FiniteDimensional_lSpace.AlgebraicCurve.lSpaceQuotientToAdeleBddQuotient

Documentation

The diagonal embedding induces a map from a quotient of Riemann–Roch spaces to the corresponding quotient of bounded adelic spaces.

Source context 11 commands

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

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

L647 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FiniteDimensional_lSpace.AlgebraicCurve.lSpaceQuotientToAdeleBddQuotient_injective

Source context 11 commands

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

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

L660 ↗

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

L679 ↗

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

L684 ↗

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

L689 ↗

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

L713 ↗

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

L720 ↗

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

L750 ↗

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

L755 ↗

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

L759 ↗

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

L763 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FiniteDimensional_lSpace.AlgebraicCurve.adeleBddPrincipal_mono

Source context 8 commands

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

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

L772 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FiniteDimensional_lSpace.AlgebraicCurve.finiteDimensional_lSpace_port

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FiniteDimensional_lSpace
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_port [hL0 : FiniteDimensional K (LSpace (0 : Divisor K F))]
    (D : Divisor K F) : FiniteDimensional K (LSpace D)

theorem

range_lSpaceQuotientToAdeleBddQuotient

L792 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FiniteDimensional_lSpace.AlgebraicCurve.range_lSpaceQuotientToAdeleBddQuotient

Source context 8 commands

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

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

L833 ↗

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

L904 ↗

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

L932 ↗

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

L947 ↗

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

L963 ↗

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

L974 ↗

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

L1021 ↗

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

L1030 ↗

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