Module

RelativeDimension.lean

Nyll.JacobianVarieties.Picard.RelativeDimension

2 declarations indexed from sourceView source ↗

Module documentation

Relative dimension of a pointed Picard scheme over a field

The represented group law and geometric connectedness give geometric integrality. The cotangent calculation at the rational zero section then determines the smooth relative dimension as the first-cohomology dimension on a two-affine cover.

This constructs a dimension witness for pointed curves over arbitrary fields. It does not assert unpointed existence or identify this dimension with a separate genus API.

Imports11

Imported by2

theorem

smoothOfRelativeDimension_finrank_H1

L41 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic.smoothOfRelativeDimension_finrank_H1

Documentation

The relative dimension of a smooth proper geometrically connected Picard representation is the dimension of first cohomology of the original curve on any two-affine cover.

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_finrank_H1
    {K : Type u} [Field K] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of K)}
    {ε : 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]
    (𝒱 : C.TwoAffineOpenCover) :
    SmoothOfRelativeDimension (Module.finrank K (𝒱.structureSheafSections c).H1)
      D.toBase

theorem

exists_representsRelSubPic_of_field_with_dimension

L66 ↗

AlgebraicGeometry.RelPicard.exists_representsRelSubPic_of_field_with_dimension