structure CechCohomologyCurves.CechDataTwoOpen (k : Type u_1) [Field k] : Type (max (max (max u_1 (u_2 + 1)) (u_3 + 1)) (u_4 + 1))

Čech data for a sheaf relative to a cover by two open sets U₁, U₂: the k-vector spaces of sections on U₁, U₂, U₁ ∩ U₂, together with the two restriction maps.

• sectionsU1 : Type u_2
• sectionsU2 : Type u_3
• sectionsU12 : Type u_4
• addCommGroupU1 : AddCommGroup self.sectionsU1
• moduleU1 : Module k self.sectionsU1
• addCommGroupU2 : AddCommGroup self.sectionsU2
• moduleU2 : Module k self.sectionsU2
• addCommGroupU12 : AddCommGroup self.sectionsU12
• moduleU12 : Module k self.sectionsU12
• restriction1 : self.sectionsU1 →ₗ[k] self.sectionsU12
• restriction2 : self.sectionsU2 →ₗ[k] self.sectionsU12

def CechCohomologyCurves.cechDifferential {k : Type u_1} [Field k] (D : CechDataTwoOpen k) : D.sectionsU1 × D.sectionsU2 →ₗ[k] D.sectionsU12

The Čech differential (s₁, s₂) ↦ s₁|_{U₁₂} - s₂|_{U₁₂} on a two-open cover.

def CechCohomologyCurves.cechH0 {k : Type u_1} [Field k] (D : CechDataTwoOpen k) : Submodule k (D.sectionsU1 × D.sectionsU2)

The 0-th Čech cohomology of a two-open cover, computed as the kernel of the Čech differential.

def CechCohomologyCurves.cechH1 {k : Type u_1} [Field k] (D : CechDataTwoOpen k) : Type u_4

The 1-st Čech cohomology of a two-open cover, computed as the cokernel of the Čech differential.

@[implicit_reducible]

instance CechCohomologyCurves.cechH1.addCommGroup {k : Type u_1} [Field k] (D : CechDataTwoOpen k) : AddCommGroup (cechH1 D)

The first Čech cohomology inherits an additive commutative group structure from the quotient.

@[implicit_reducible]

instance CechCohomologyCurves.cechH1.module {k : Type u_1} [Field k] (D : CechDataTwoOpen k) : Module k (cechH1 D)

The first Čech cohomology is a k-module via the quotient structure.

noncomputable def CechCohomologyCurves.h0 {k : Type u_1} [Field k] (D : CechDataTwoOpen k) : ℕ

The dimension h⁰ of the 0-th Čech cohomology.

noncomputable def CechCohomologyCurves.h1 {k : Type u_1} [Field k] (D : CechDataTwoOpen k) : ℕ

The dimension h¹ of the first Čech cohomology.

noncomputable def CechCohomologyCurves.eulerCharacteristic {k : Type u_1} [Field k] (D : CechDataTwoOpen k) : ℤ

The Euler characteristic χ = h⁰ - h¹ of a two-open Čech datum.

structure CechCohomologyCurves.LineBundleCurveData (k : Type u_2) [Field k] extends CechCohomologyCurves.CechDataTwoOpen k : Type (max (max (max u_2 (u_3 + 1)) (u_4 + 1)) (u_5 + 1))

Čech data for a line bundle on a curve, packaged with the degree of the line bundle and the genus of the curve.

• sectionsU1 : Type u_5
• sectionsU2 : Type u_4
• sectionsU12 : Type u_3
• addCommGroupU1 : AddCommGroup self.sectionsU1
• moduleU1 : Module k self.sectionsU1
• addCommGroupU2 : AddCommGroup self.sectionsU2
• moduleU2 : Module k self.sectionsU2
• addCommGroupU12 : AddCommGroup self.sectionsU12
• moduleU12 : Module k self.sectionsU12
• restriction1 : self.sectionsU1 →ₗ[k] self.sectionsU12
• restriction2 : self.sectionsU2 →ₗ[k] self.sectionsU12
• deg : ℤ
• genus : ℕ

theorem CechCohomologyCurves.riemann_roch {k : Type u_1} [Field k] (D : LineBundleCurveData k) : eulerCharacteristic D.toCechDataTwoOpen = D.deg + 1 - ↑D.genus

Riemann–Roch for a line bundle on a curve, expressed via Čech cohomology: χ(L) = deg L + 1 - g.