Module

UnpointedDescent.lean

Nyll.JacobianVarieties.Picard.UnpointedDescent

4 declarations indexed from sourceView source ↗

Module documentation

Canonical descent of a Picard scheme without a rational basepoint

A point is required only after the finite field extension. Normalization there and the unrigidified base-change comparison make the actual Picard representation a representation of a restricted presheaf. Its canonical descent action consequently has proved unit and cocycle laws, and finite faithfully flat descent is effective.

Imports7

Imported by3

def

representableByRestrict

L44 ↗

JacobianVarieties.Picard.Unpointed.representableByRestrict

Documentation

The local pointed representation represents the restriction of the actual unrigidified presheaf on the original curve.

Source context 6 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
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R']
  (ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R'))) (baseChange R c R'))
  {D' : RelativePic0Designation R' (baseChange R c R')}
  (h' : RepresentsRelSubPic (baseChange R c R') ε'
    (algEquivZeroCut (baseChange R c R') ε') D')

Lean source · statement

def representableByRestrict :
    ((Over.map (specMap R R')).op ⋙ Unrigidified.zeroPresheaf c).RepresentableBy
      (Over.mk D'.toBase)

def

descentAction

L51 ↗

JacobianVarieties.Picard.Unpointed.descentAction

Documentation

The canonical action induced by the actual quotient presheaf and its representation.

Source context 6 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
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R']
  (ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R'))) (baseChange R c R'))
  {D' : RelativePic0Designation R' (baseChange R c R')}
  (h' : RepresentsRelSubPic (baseChange R c R') ε'
    (algEquivZeroCut (baseChange R c R') ε') D')

Lean source · statement

def descentAction : DescentAction (specMap R R') D'.toBase

theorem

descentAction_effective

L57 ↗

JacobianVarieties.Picard.Unpointed.descentAction_effective

Documentation

The unpointed Picard descent datum is effective along a finite faithfully flat finitely presented algebra, under the affine-neighborhood criterion.

Source context 6 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
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R']
  (ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R'))) (baseChange R c R'))
  {D' : RelativePic0Designation R' (baseChange R c R')}
  (h' : RepresentsRelSubPic (baseChange R c R') ε'
    (algEquivZeroCut (baseChange R c R') ε') D')

Lean source · statement

theorem descentAction_effective
    [Module.Finite R R'] [Algebra.FinitePresentation R R'] [Module.FaithfullyFlat R R']
    (haff : ∀ S : Finset D'.P, ∃ U : D'.P.Opens, IsAffineOpen U ∧ ∀ x ∈ S, x ∈ U) :
    (descentAction c R' ε' h').Effective

theorem

descentAction_effective_of_finite_fieldExtension

L65 ↗

JacobianVarieties.Picard.Unpointed.descentAction_effective_of_finite_fieldExtension

Documentation

In particular any finite field extension suffices; no separability or characteristic restriction is imposed and no point over the ground field is required.

Source context 6 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
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  (c : C ⟶ Spec (CommRingCat.of R))
  (R' : Type u) [CommRing R'] [Algebra R R']
  (ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R'))) (baseChange R c R'))
  {D' : RelativePic0Designation R' (baseChange R c R')}
  (h' : RepresentsRelSubPic (baseChange R c R') ε'
    (algEquivZeroCut (baseChange R c R') ε') D')

Lean source · statement

theorem descentAction_effective_of_finite_fieldExtension
    {K : Type u} [Field K] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of K))
    (L : Type u) [Field L] [Algebra K L] [Module.Finite K L]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of L))) (baseChange K f L))
    {D : RelativePic0Designation L (baseChange K f L)}
    (h : RepresentsRelSubPic (baseChange K f L) ε (algEquivZeroCut (baseChange K f L) ε) D)
    (haff : ∀ S : Finset D.P, ∃ U : D.P.Opens, IsAffineOpen U ∧ ∀ x ∈ S, x ∈ U) :
    (descentAction f L ε h).Effective

Module documentation

Canonical descent of a Picard scheme without a rational basepoint

Declarations

representableByRestrict

descentAction

descentAction_effective

descentAction_effective_of_finite_fieldExtension