The Jacobian challenge (Christian Merten's AG version)

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremThe Riemann–Roch theorem#

On a proper integral curve over a field k whose codimension-one local rings are discrete valuation rings, with a k-rational point and with H¹(X, 𝒪_X) finite-dimensional, every Weil divisor D satisfies

χ(𝒪_X(D)) = deg D + 1 - g,

where χ(M) = dim H⁰(X, M) - dim H¹(X, M), deg D = Σ_y D(y) [κ(y) : k] and g is the genus.

TauCeti.AlgebraicGeometry.SchemeWeilDivisor.eulerCharBelow_sheaf_eq_relativeDegree_add_one_sub_genus.{u}
  {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X]
  [∀ (y : TauCeti.AlgebraicGeometry.CodimensionOnePoint X),
      IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)]
  (k : Type u) [Field k] [X.Over (AlgebraicGeometry.Spec ↧k)]
  [AlgebraicGeometry.IsProper (X ↘ AlgebraicGeometry.Spec ↧k)]
  [FiniteDimensional k
      (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology
        (TauCeti.AlgebraicGeometry.InvertibleSheaf.trivial X).obj 1)]
  (hX : ∀ (y : ↥X), Order.coheight y ≤ 1) {s : AlgebraicGeometry.Spec ↧k ⟶ X}
  (hs :
    CategoryTheory.CategoryStruct.comp s (X ↘ AlgebraicGeometry.Spec ↧k) =
      CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧k))
  (D : TauCeti.AlgebraicGeometry.SchemeWeilDivisor X) :
  AlgebraicGeometry.Scheme.Modules.eulerCharBelow k X D.sheaf 2 =
    (TauCeti.AlgebraicGeometry.SchemeWeilDivisor.relativeDegree (X ↘ AlgebraicGeometry.Spec ↧k)) D +
        1 -
      ↑(AlgebraicGeometry.Scheme.genus k X)
Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.SchemeWeilDivisor.eulerCharBelow_sheaf_eq_relativeDegree_add_one_sub_genus.

Other forms

Riemann–Roch on a curve of genus one. Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.SchemeWeilDivisor.finrank_cohomology_zero_sheaf_eq_relativeDegree_of_genus_eq_one.

TauCeti.AlgebraicGeometry.SchemeWeilDivisor.finrank_cohomology_zero_sheaf_eq_relativeDegree_of_genus_eq_one.{u}
  (k : Type u) [Field k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X]
  [AlgebraicGeometry.IsNoetherian X]
  [∀ (y : TauCeti.AlgebraicGeometry.CodimensionOnePoint X),
      IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)]
  [hX : Fact (∀ (y : ↥X), Order.coheight y ≤ 1)] [X.Over (AlgebraicGeometry.Spec ↧k)]
  [AlgebraicGeometry.IsProper (X ↘ AlgebraicGeometry.Spec ↧k)]
  [FiniteDimensional k
      (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology
        (TauCeti.AlgebraicGeometry.InvertibleSheaf.trivial X).obj 1)]
  (hk : IsIntegrallyClosedIn k ↑X.functionField) (hg : AlgebraicGeometry.Scheme.genus k X = 1)
  {D : TauCeti.AlgebraicGeometry.SchemeWeilDivisor X}
  (hD :
    0 <
      (TauCeti.AlgebraicGeometry.SchemeWeilDivisor.relativeDegree (X ↘ AlgebraicGeometry.Spec ↧k))
        D) :
  ↑(Module.finrank k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology D.sheaf 0)) =
    (TauCeti.AlgebraicGeometry.SchemeWeilDivisor.relativeDegree (X ↘ AlgebraicGeometry.Spec ↧k)) D

The Riemann–Roch theorem for a line bundle. Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.InvertibleSheaf.eulerCharBelow_eq_relativeDegree_add_one_sub_genus.

TauCeti.AlgebraicGeometry.InvertibleSheaf.eulerCharBelow_eq_relativeDegree_add_one_sub_genus.{u}
  {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X]
  [AlgebraicGeometry.IsLocallyNoetherian X]
  [∀ (y : TauCeti.AlgebraicGeometry.CodimensionOnePoint X),
      IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)]
  (k : Type u) [Field k] [X.Over (AlgebraicGeometry.Spec ↧k)]
  [AlgebraicGeometry.IsProper (X ↘ AlgebraicGeometry.Spec ↧k)]
  [FiniteDimensional k
      (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology
        (TauCeti.AlgebraicGeometry.InvertibleSheaf.trivial X).obj 1)]
  (hX : ∀ (y : ↥X), Order.coheight y ≤ 1) {s : AlgebraicGeometry.Spec ↧k ⟶ X}
  (hs :
    CategoryTheory.CategoryStruct.comp s (X ↘ AlgebraicGeometry.Spec ↧k) =
      CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧k))
  {L : TauCeti.AlgebraicGeometry.InvertibleSheaf X}
  {D : TauCeti.AlgebraicGeometry.SchemeWeilDivisor X} (e : L.obj ≅ D.sheaf) :
  AlgebraicGeometry.Scheme.Modules.eulerCharBelow k X L.obj 2 =
    (TauCeti.AlgebraicGeometry.SchemeWeilDivisor.relativeDegree (X ↘ AlgebraicGeometry.Spec ↧k)) D +
        1 -
      ↑(AlgebraicGeometry.Scheme.genus k X)

The Riemann–Roch theorem, in terms of the two cohomology dimensions. Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.SchemeWeilDivisor.finrank_cohomology_zero_sheaf_sub_finrank_cohomology_one_sheaf.

TauCeti.AlgebraicGeometry.SchemeWeilDivisor.finrank_cohomology_zero_sheaf_sub_finrank_cohomology_one_sheaf.{u}
  {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X]
  [∀ (y : TauCeti.AlgebraicGeometry.CodimensionOnePoint X),
      IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)]
  (k : Type u) [Field k] [X.Over (AlgebraicGeometry.Spec ↧k)]
  [AlgebraicGeometry.IsProper (X ↘ AlgebraicGeometry.Spec ↧k)]
  [FiniteDimensional k
      (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology
        (TauCeti.AlgebraicGeometry.InvertibleSheaf.trivial X).obj 1)]
  (hX : ∀ (y : ↥X), Order.coheight y ≤ 1) {s : AlgebraicGeometry.Spec ↧k ⟶ X}
  (hs :
    CategoryTheory.CategoryStruct.comp s (X ↘ AlgebraicGeometry.Spec ↧k) =
      CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧k))
  (D : TauCeti.AlgebraicGeometry.SchemeWeilDivisor X) :
  ↑(Module.finrank k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology D.sheaf 0)) -
      ↑(Module.finrank k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology D.sheaf 1)) =
    (TauCeti.AlgebraicGeometry.SchemeWeilDivisor.relativeDegree (X ↘ AlgebraicGeometry.Spec ↧k)) D +
        1 -
      ↑(AlgebraicGeometry.Scheme.genus k X)
Sources
LeanTauCeti.AlgebraicGeometry.SchemeWeilDivisor.eulerCharBelow_sheaf_eq_relativeDegree_add_one_sub_genus · TauCeti.AlgebraicGeometry.SchemeWeilDivisor.finrank_cohomology_zero_sheaf_eq_relativeDegree_of_genus_eq_one · TauCeti.AlgebraicGeometry.InvertibleSheaf.eulerCharBelow_eq_relativeDegree_add_one_sub_genus · TauCeti.AlgebraicGeometry.SchemeWeilDivisor.finrank_cohomology_zero_sheaf_sub_finrank_cohomology_one_sheaf
Uses 3
Proof usesRiemann's theorem · The Riemann–Roch theorem (Stichtenoth, Theorem 1.5.15), for the divisor (ω) itself · The weak approximation theorem

TheoremTauCeti.AlgebraicGeometry.nonempty_cohomologyOneDualEquivCohomologyZero_differentials_tensor_dual#

Over an exact constant field, the dual of H¹(X, L) is linearly equivalent to H⁰(X, Ω_{X/k} ⊗ L⁻¹), by the identification of the differential line bundle with the canonical bundle. This asserts only the existence of a noncanonical linear equivalence, not a natural duality pairing.

TauCeti.AlgebraicGeometry.nonempty_cohomologyOneDualEquivCohomologyZero_differentials_tensor_dual.{u}
  {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)]
  [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [X.IsSeparated]
  [∀ (y : TauCeti.AlgebraicGeometry.CodimensionOnePoint X),
      IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)]
  [TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X
      (AlgebraicGeometry.Scheme.relativeDifferentials k X)]
  (hF : TauCeti.IsFunctionField k ↑X.functionField) (hk : IsIntegrallyClosedIn k ↑X.functionField)
  (hdim : ∀ (y : ↥X), Order.coheight y ≤ 1)
  (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k))
  (L : TauCeti.AlgebraicGeometry.InvertibleSheaf X) :
  Nonempty
    (Module.Dual k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology L.obj 1) ≃ₗ[k]
      TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology
        (TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorProduct
            { obj := AlgebraicGeometry.Scheme.relativeDifferentials k X, property := ⋯ } L.dual).obj
        0)
Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.nonempty_cohomologyOneDualEquivCohomologyZero_differentials_tensor_dual.

Sources
LeanTauCeti.AlgebraicGeometry.nonempty_cohomologyOneDualEquivCohomologyZero_differentials_tensor_dual
Uses 8
Proof usesThe abstract residue theorem (Stichtenoth, (1.45)) · Dedekind's different theorem, first part (Stichtenoth, Theorem 3.5.1(a)) · The fundamental inequality (Stichtenoth, Theorem 3.1.11) · Riemann's theorem · The Riemann–Roch theorem (Stichtenoth, Theorem 1.5.15), for the divisor (ω) itself · Serre duality in degree zero · Stichtenoth's transformation formula · The weak approximation theorem

DefinitionThe Cartier–Picard dictionary#

On any integral scheme, Cartier divisors modulo principal divisors form the Picard group of line-bundle classes under tensor product.

TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.classGroupAddEquivLineBundleClass.{u}
  (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] :
  TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.ClassGroup X ≃+
    Additive (TauCeti.AlgebraicGeometry.LineBundleClass X)
Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.Scheme.CartierDivisor.classGroupAddEquivLineBundleClass.

Sources
LeanTauCeti.AlgebraicGeometry.Scheme.CartierDivisor.classGroupAddEquivLineBundleClass

DefinitionThe points of an elliptic curve form Pic⁰ of its projective model#

For an elliptic curve W over a field K, the group W.toAffine.Point of Mathlib, with its chord-and-tangent group law, is isomorphic to the group Pic⁰ (projModel W) of degree-zero line bundles on the projective model. The point at infinity goes to the trivial bundle, and an affine point P to the class of 𝒪(x_P - x_O) (coe_pointAddEquivPicZero_some).

WeierstrassCurve.pointAddEquivPicZero.{u} {K : Type u} [Field K] (W : WeierstrassCurve K)
  [W.IsElliptic] [DecidableEq K] :
  W.toAffine.Point ≃+ ↥(TauCeti.AlgebraicGeometry.LineBundleClass.picZero K W.projModel)
Lean

Formalized in Tau Ceti as WeierstrassCurve.pointAddEquivPicZero.

Sources
LeanWeierstrassCurve.pointAddEquivPicZero
Uses 3
Proof usesThe Jacobian criterion for étaleness · Riemann's theorem · The weak approximation theorem

TheoremThe Abel–Jacobi map of a curve of positive genus separates points over every field extension#

Let X be a smooth proper geometrically connected curve of genus g ≥ 1 over a field k, with a rational point x₀. For every field extension K / k, two K-points of X with the same class 𝒪(Γₓ - x₀) in Pic(X_K) / Pic(Spec K) are equal. Taking K algebraically closed, the Abel–Jacobi map is injective on geometric points.

TauCeti.AlgebraicGeometry.abelJacobiMap_app_injective_of_genus_pos.{u} {k : Type u} [Field k]
  {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)]
  [AlgebraicGeometry.IsProper (X ↘ AlgebraicGeometry.Spec ↧k)]
  [AlgebraicGeometry.SmoothOfRelativeDimension 1 (X ↘ AlgebraicGeometry.Spec ↧k)]
  [AlgebraicGeometry.GeometricallyConnected (X ↘ AlgebraicGeometry.Spec ↧k)]
  {x₀ : AlgebraicGeometry.Spec ↧k ⟶ X}
  (hx₀ :
    CategoryTheory.CategoryStruct.comp x₀ (X ↘ AlgebraicGeometry.Spec ↧k) =
      CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧k))
  (hg : 0 < AlgebraicGeometry.Scheme.genus k X) (K : Type u) [Field K] [Algebra k K] :
  Function.Injective
    ⇑(CategoryTheory.ConcreteCategory.hom
        ((TauCeti.AlgebraicGeometry.abelJacobiMap (X ↘ AlgebraicGeometry.Spec ↧k) hx₀).app
          (Opposite.op
            (CategoryTheory.Over.mk
              (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k K)))))))
Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.abelJacobiMap_app_injective_of_genus_pos.

Sources
LeanTauCeti.AlgebraicGeometry.abelJacobiMap_app_injective_of_genus_pos
Uses 8
Proof usesThe Jacobian criterion for étaleness · Krull–Akizuki for Mathlib's integralClosure · Riemann's theorem · The Riemann–Roch theorem (Stichtenoth, Theorem 1.5.15), for the divisor (ω) itself · Serre's vanishing theorem on affine opens · TauCeti.Ring.IsJapanese · The weak approximation theorem · Weierstrass gap theorem (Stichtenoth, Theorem 1.6.8)

DefinitionThe degree-zero Picard functor Pic⁰_{X/S}#

The degree-zero Picard functor Pic⁰_{X/S} of a smooth proper geometrically connected family of curves f : X ⟶ S, as a presheaf of commutative groups on schemes over S: it sends T to the subgroup relativePicardDegreeZeroSubgroup f T of Pic(X_T) / Pic(T), and a morphism over S to the restriction of the pullback map of the relative Picard presheaf.

TauCeti.AlgebraicGeometry.relativePicardDegreeZeroFunctor.{u} {S X : AlgebraicGeometry.Scheme}
  (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f]
  [AlgebraicGeometry.GeometricallyConnected f] :
  CategoryTheory.Functor (CategoryTheory.Over S)ᵒᵖ CommGrpCat
Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.relativePicardDegreeZeroFunctor.

Sources
LeanTauCeti.AlgebraicGeometry.relativePicardDegreeZeroFunctor
Uses 3 · Used by 1
Proof usesThe Jacobian criterion for étaleness · Riemann's theorem · The weak approximation theorem
Used byThe Abel–Jacobi map into the degree-zero Picard fppf sheaf

DefinitionTauCeti.AlgebraicGeometry.relativePicardFppfSheaf#

The relative Picard fppf sheaf of f : X ⟶ S, obtained by sheafifying the presheaf T ↦ Pic(X_T) / Pic(T) on the fppf site of schemes over S.

This definition does not assert that the resulting sheaf is representable.

TauCeti.AlgebraicGeometry.relativePicardFppfSheaf.{u} {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) :
  CategoryTheory.Sheaf (AlgebraicGeometry.Scheme.fppfTopology.over S) AddCommGrpCat
Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.relativePicardFppfSheaf.

Sources
LeanTauCeti.AlgebraicGeometry.relativePicardFppfSheaf

DefinitionThe Abel–Jacobi map into the degree-zero Picard fppf sheaf#

It sends an S-point x : T ⟶ X to the fppf-local class of 𝒪(Γₓ - x₀,T).

TauCeti.AlgebraicGeometry.abelJacobiMapToPicZeroFppf.{u} {S X : AlgebraicGeometry.Scheme}
  (f : X ⟶ S) [AlgebraicGeometry.IsProper f] [AlgebraicGeometry.SmoothOfRelativeDimension 1 f]
  [AlgebraicGeometry.GeometricallyConnected f] {x₀ : S ⟶ X}
  (hx₀ : CategoryTheory.CategoryStruct.comp x₀ f = CategoryTheory.CategoryStruct.id S) :
  (CategoryTheory.yoneda.obj (CategoryTheory.Over.mk f)).comp
      CategoryTheory.uliftFunctor.{u + 1, u} ⟶
    (TauCeti.AlgebraicGeometry.relativePicardDegreeZeroFppfSheaf f).obj.comp
      (CategoryTheory.forget AddCommGrpCat)
Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.abelJacobiMapToPicZeroFppf.

Sources
LeanTauCeti.AlgebraicGeometry.abelJacobiMapToPicZeroFppf
Uses 6
Statement usesThe degree-zero Picard functor Pic⁰_{X/S}
Proof usesThe Jacobian criterion for étaleness · Riemann's theorem · Serre's vanishing theorem on affine opens · TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf · The weak approximation theorem

StructureTauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese#

A pointed morphism a : X ⟶ J.toOver from a scheme X over K with a K-rational point x₀ to an abelian variety J has the Albanese property if every morphism f : X ⟶ A.toOver to an abelian variety sending x₀ to the identity factors as f = a ≫ φ through a unique homomorphism φ : J ⟶ A of abelian varieties.

TauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese.{u} {K : Type u} [Field K]
  {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)}
  (x₀ :
    CategoryTheory.MonoidalCategoryStruct.tensorUnit
        (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶
      X)
  {J : TauCeti.AlgebraicGeometry.AbelianVariety K} (a : X ⟶ J.toOver) : Prop
Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese.

Sources
LeanTauCeti.AlgebraicGeometry.AbelianVariety.IsAlbanese

TheoremRiemann's inequality#

On a proper integral curve over a field k whose codimension-one local rings are discrete valuation rings, with all global functions constant and with H¹(X, 𝒪_X) finite-dimensional, dim_k H⁰(X, 𝒪_X(D)) ≥ deg D + 1 - g.

TauCeti.AlgebraicGeometry.SchemeWeilDivisor.relativeDegree_add_one_sub_genus_le_finrank_cohomology_zero_sheaf.{u}
  {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X]
  [∀ (y : TauCeti.AlgebraicGeometry.CodimensionOnePoint X),
      IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)]
  (k : Type u) [Field k] [X.Over (AlgebraicGeometry.Spec ↧k)]
  [AlgebraicGeometry.IsProper (X ↘ AlgebraicGeometry.Spec ↧k)]
  [FiniteDimensional k
      (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology
        (TauCeti.AlgebraicGeometry.InvertibleSheaf.trivial X).obj 1)]
  (hX : ∀ (y : ↥X), Order.coheight y ≤ 1)
  (hφ : Function.Surjective ⇑(AlgebraicGeometry.Scheme.Modules.baseRingToGlobalSections k X))
  (D : TauCeti.AlgebraicGeometry.SchemeWeilDivisor X) :
  (TauCeti.AlgebraicGeometry.SchemeWeilDivisor.relativeDegree (X ↘ AlgebraicGeometry.Spec ↧k)) D +
        1 -
      ↑(AlgebraicGeometry.Scheme.genus k X) ≤
    ↑(Module.finrank k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology D.sheaf 0))
Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.SchemeWeilDivisor.relativeDegree_add_one_sub_genus_le_finrank_cohomology_zero_sheaf.

Sources
LeanTauCeti.AlgebraicGeometry.SchemeWeilDivisor.relativeDegree_add_one_sub_genus_le_finrank_cohomology_zero_sheaf

TheoremThe Riemann–Roch theorem with the sheaf of differentials#

Over an exact constant field, every line bundle L satisfies

dim H⁰(X, L) - dim H⁰(X, Ω_{X/k} ⊗ L⁻¹) = deg L + 1 - g,

where deg L = χ(L) - χ(𝒪_X) is the Euler-characteristic degree and g = dim H¹(X, 𝒪_X).

TauCeti.AlgebraicGeometry.finrank_cohomology_zero_sub_finrank_cohomology_zero_differentials_tensor_dual.{u}
  {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)]
  [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] [X.IsSeparated]
  [∀ (y : TauCeti.AlgebraicGeometry.CodimensionOnePoint X),
      IsDiscreteValuationRing ↑(X.presheaf.stalk ↑y)]
  [TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X
      (AlgebraicGeometry.Scheme.relativeDifferentials k X)]
  (hF : TauCeti.IsFunctionField k ↑X.functionField) (hk : IsIntegrallyClosedIn k ↑X.functionField)
  (hdim : ∀ (y : ↥X), Order.coheight y ≤ 1)
  (hex : AlgebraicGeometry.ValuativeCriterion.Existence (X ↘ AlgebraicGeometry.Spec ↧k))
  (L : TauCeti.AlgebraicGeometry.InvertibleSheaf X) :
  ↑(Module.finrank k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology L.obj 0)) -
      ↑(Module.finrank k
          (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology
            (TauCeti.AlgebraicGeometry.InvertibleSheaf.tensorProduct
                { obj := AlgebraicGeometry.Scheme.relativeDifferentials k X, property := ⋯ }
                L.dual).obj
            0)) =
    TauCeti.AlgebraicGeometry.InvertibleSheaf.eulerDegree k L + 1 -
      ↑(AlgebraicGeometry.Scheme.genus k X)
Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.finrank_cohomology_zero_sub_finrank_cohomology_zero_differentials_tensor_dual.

Sources
LeanTauCeti.AlgebraicGeometry.finrank_cohomology_zero_sub_finrank_cohomology_zero_differentials_tensor_dual
Uses 8
Proof usesThe abstract residue theorem (Stichtenoth, (1.45)) · Dedekind's different theorem, first part (Stichtenoth, Theorem 3.5.1(a)) · The fundamental inequality (Stichtenoth, Theorem 3.1.11) · Riemann's theorem · The Riemann–Roch theorem (Stichtenoth, Theorem 1.5.15), for the divisor (ω) itself · The Riemann–Roch theorem for line bundles, in Serre-duality form · Stichtenoth's transformation formula · The weak approximation theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.