Module

CechRiemannRoch_of_genusReached.lean

Nyll.AlgebraicCurves.Cohomology.CechRiemannRoch_of_genusReached

1 declaration indexed from sourceView source ↗

Module documentation

The Riemann--Roch dimension formula from a two-chart section system reaching the genus.

Imports12

Imported by6

theorem

cechRiemannRoch_of_genusReached

L35 ↗

AlgebraicCurve.cechRiemannRoch_of_genusReached

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.CechRiemannRoch_of_genusReached
open AlgebraicCurve in

Lean source · statement

theorem _root_.AlgebraicCurve.cechRiemannRoch_of_genusReached {K F : Type*} [Field K] [Field F]
    [Algebra K F] [IsCurveOver K F]
    [FiniteDimensional K ↥(LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀)
    {S₀ S₁ : Set (Place K F)} (hcover : S₀ ∪ S₁ = Set.univ) (h₀ : ∃ v, v ∉ S₀) (h₁ : ∃ v, v ∉ S₁)
    (D : Divisor K F) :
    FiniteDimensional K ↥(cechH0 S₀ S₁ D) ∧ Module.Finite K (cechH1 S₀ S₁ D) ∧
      Module.finrank K ↥(cechH0 S₀ S₁ D) = ell D ∧
      Module.finrank K (cechH1 S₀ S₁ D) = indexOfSpecialty D ∧
      (Module.finrank K ↥(cechH0 S₀ S₁ D) : ℤ) - Module.finrank K (cechH1 S₀ S₁ D)
        = Divisor.degree D + 1 - γ ∧
      (D₀ ≤ D → Subsingleton (cechH1 S₀ S₁ D))

Module documentation

Declarations

cechRiemannRoch_of_genusReached