NYLL
Module

UnpointedDimension.lean

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

Module documentation

Dimension and geometric integrality of the descended Jacobian

The same descended scheme is used throughout. Its locally constant smooth dimension is compared, after the actual finite extension, with the dimension of the represented Picard scheme. Comparison of affine smooth charts determines the integer dimension, including over imperfect fields.

Imports5
Imported by2

Declarations

theorem

relativeDimension_eq_of_point

L32 ↗
JacobianVarieties.Picard.Unpointed.relativeDimension_eq_of_point
Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian
namespace JacobianVarieties.Picard.Unpointed
Lean source · statement
theorem relativeDimension_eq_of_point
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsAffine Y] (x : X) (n m : ℕ)
    [SmoothOfRelativeDimension n f] [SmoothOfRelativeDimension m f] : n = m
theorem

smoothOfRelativeDimension_geometricGenus_of_picardDescent

L43 ↗
JacobianVarieties.Picard.Unpointed.smoothOfRelativeDimension_geometricGenus_of_picardDescent
Documentation

The actual descent of a local Picard representative has the original curve's geometric genus as its smooth dimension and is geometrically integral.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open AlgebraicGeometry.SmoothProperCurve NeronModelInfra GoodReductionJacobian
namespace JacobianVarieties.Picard.Unpointed
Lean source · statement
theorem smoothOfRelativeDimension_geometricGenus_of_picardDescent
    (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 = baseChange K p L) :
    SmoothOfRelativeDimension (geometricGenus K c) p ∧ GeometricallyIntegral p

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