Nyll.JacobianVarieties.Picard.UnpointedExistence

Module documentation

Existence of a smooth proper unpointed Picard descent

A closed point supplies a finite residue extension and an actual section of the extended curve. Pointed Picard existence and its affine-neighborhood theorem apply there. The unrigidified quotient presheaf supplies the descent action, and its effective quotient gives a smooth proper geometrically connected scheme over the original field.

This statement retains the local representation and the actual descent compatibility. Identifying the result with an fppf sheafification and descending its group law are separate constructions.

theorem

exists_smooth_proper_picardDescent_of_field

L40 ↗

JacobianVarieties.Picard.Unpointed.exists_smooth_proper_picardDescent_of_field

Documentation

Every smooth proper geometrically integral curve over an arbitrary field has a smooth proper geometrically connected descent of a pointed Picard representation. The point and local representation are constructed, including in positive characteristic.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian
namespace JacobianVarieties.Picard.Unpointed

Lean source · statement

theorem exists_smooth_proper_picardDescent_of_field
    (K : Type u) [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
    [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c] :
    ∃ (L : Type u) (_ : Field L) (_ : Algebra K L) (_ : Module.Finite K L)
      (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of L))) (baseChange K c L))
      (D : RelativePic0Designation L (baseChange K c L))
      (h : RepresentsRelSubPic (baseChange K c L) ε (algEquivZeroCut (baseChange K c L) ε) D)
      (P : Scheme.{u}) (p : P ⟶ Spec (CommRingCat.of K)),
      Smooth p ∧ IsProper p ∧ GeometricallyConnected p ∧
      ∃ (e : pullback p (specMap K L) ≅ D.P)
        (he : e.hom ≫ D.toBase = pullback.snd p (specMap K L)),
        DescentAction.eRel (specMap K L) D.toBase p e he ≫ (descentAction c L ε h).act =
          (DescentAction.canonical (specMap K L) p).act ≫ e.hom

Module documentation

Existence of a smooth proper unpointed Picard descent

Declarations

exists_smooth_proper_picardDescent_of_field