Module

Finite_H1_of_genusReached.lean

Nyll.AlgebraicCurves.Cohomology.Finite_H1_of_genusReached

1 declaration indexed from sourceView source ↗

Module documentation

Finite adelic first cohomology from a two-chart Cech system reaching the genus.

Imports7

Imported by2

theorem

finite_H1_of_genusReached

AlgebraicCurve.finite_H1_of_genusReached

Source context 3 commands

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

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

Lean source · statement

theorem _root_.AlgebraicCurve.finite_H1_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 (H1 D)