NYLL
Module

Existence.lean

Nyll.JacobianVarieties.Picard.Existence
2 declarations indexed from sourceView source ↗

Module documentation

Pointed Picard existence over reduced local rings and fields

Finite-map data on the original pointed curve produces finite etale chart sections. The resulting local representing scheme descends to the original curve. Over an arbitrary field the required finite-map data are constructed from the curve and its rational section.

No DVR thickening or comparison with a special fibre is used. These are pointed existence statements; unpointed existence, dimension and Albanese universality remain separate tasks.

Imports13
Imported by6

Declarations

theorem

exists_representsRelSubPic_of_local_finiteMapData

L49 ↗
AlgebraicGeometry.RelPicard.exists_representsRelSubPic_of_local_finiteMapData
Documentation

Finite-map data constructs a smooth proper representing Picard scheme over a reduced local noetherian ring, by finite etale chart construction and descent.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.SmoothProperCurve
  NeronModelInfra GoodReductionJacobian
namespace AlgebraicGeometry.RelPicard
Lean source · statement
theorem exists_representsRelSubPic_of_local_finiteMapData
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [_root_.IsReduced R]
    {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) [IsProper c]
    [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (h𝔉 : ∀ m₀ : ℕ, ∃ 𝔉 : FiniteMapData c ε, m₀ ≤ 𝔉.m ∧ 𝔉.LevelSetsGenericallyEtale) :
    ∃ D : RelativePic0Designation R c,
      Nonempty (RepresentsRelSubPic c ε (algEquivZeroCut c ε) D) ∧
        Smooth D.toBase ∧ IsProper D.toBase ∧ GeometricallyConnected D.toBase
theorem

exists_representsRelSubPic_of_field

L80 ↗
AlgebraicGeometry.RelPicard.exists_representsRelSubPic_of_field
Documentation

A pointed smooth proper geometrically integral curve over any field has a smooth proper geometrically connected scheme representing its rigidified degree-zero Picard functor.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.SmoothProperCurve
  NeronModelInfra GoodReductionJacobian
namespace AlgebraicGeometry.RelPicard
Lean source · statement
theorem exists_representsRelSubPic_of_field (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,
      Nonempty (RepresentsRelSubPic c ε (algEquivZeroCut c ε) D) ∧
        Smooth D.toBase ∧ IsProper D.toBase ∧ GeometricallyConnected D.toBase

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