Module

GenusDimension.lean

Nyll.JacobianVarieties.Picard.GenusDimension

2 declarations indexed from sourceView source ↗

Module documentation

The dimension of a represented Jacobian equals the geometric genus

The genus here is fixed by the original curve and its actual geometric function field, independently of the choice of point, affine cover, or Picard representation. No assumption on the characteristic or algebraic closedness is imposed.

Imports8

Imported by2

theorem

smoothOfRelativeDimension_geometricGenus

L35 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic.smoothOfRelativeDimension_geometricGenus

Documentation

The represented Jacobian has the geometric genus of the original curve as its smooth relative dimension. The affine cover is constructed from the given point.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry NeronModelInfra GoodReductionJacobian
namespace AlgebraicGeometry.RelPicard

Lean source · statement

theorem RepresentsRelSubPic.smoothOfRelativeDimension_geometricGenus
    {K : Type u} [Field K] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of K)}
    [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) c}
    {D : RelativePic0Designation K c}
    (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
    [Smooth D.toBase] [IsProper D.toBase] [GeometricallyConnected D.toBase] :
    SmoothOfRelativeDimension (SmoothProperCurve.geometricGenus K c) D.toBase

theorem

exists_representsRelSubPic_of_field_with_genus

L49 ↗

AlgebraicGeometry.RelPicard.exists_representsRelSubPic_of_field_with_genus