NYLL
Module

Genus_eq_genusFF.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Genus_eq_genusFF
1 declaration indexed from sourceView source ↗

Module documentation

Genus eq genus FF

Imports4
Imported by12

Declarations

theorem

genus_eq_genusFF

L28 ↗
AlgebraicCurve.genus_eq_genusFF
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Genus_eq_genusFF
open AlgebraicCurve KaehlerDifferential
Lean source · statement
theorem _root_.AlgebraicCurve.genus_eq_genusFF
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    [AlgebraicCurve.IsCurveOver K F] [AlgebraicCurve.HasCanonicalDivisor (K := K) (F := F)]
    [∀ v : AlgebraicCurve.Place K F, v.DCoordGenerates]
    (hRR : AlgebraicCurve.FunctionFieldRiemannRoch K F) (hWDA : AlgebraicCurve.WeilDualityAdelic K
      F)
    (hC : AlgebraicCurve.ConstantsAreBase K F) :
    AlgebraicCurve.genus K F = AlgebraicCurve.genusFF K F

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