NYLL
Module

UnpointedPointedComparison.lean

Nyll.JacobianVarieties.Picard.UnpointedPointedComparison
7 declarations indexed from sourceView source ↗

Module documentation

Comparison of the unpointed Jacobian with a pointed Picard representative

When an actual rational point and a pointed representation are provided, the same chosen unpointed Jacobian represents the unrigidified presheaf. Descending the local universal element fixes its comparison with the pointed representative.

Imports4
Imported by2

Declarations

def

pointedUnrigidifiedRepresentation

L35 ↗
JacobianVarieties.Picard.Unpointed.pointedUnrigidifiedRepresentation
Documentation

The pointed Picard representative also represents the actual unrigidified classes.

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 Opposite
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {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)
Lean source · statement
def pointedUnrigidifiedRepresentation :
    (Unrigidified.zeroPresheaf c).RepresentableBy (Over.mk D.toBase)
def

pointedRepresentation

L41 ↗
JacobianVarieties.Picard.Unpointed.Presentation.pointedRepresentation
Documentation

A pointed curve makes its actual quotient presheaf a sheaf on the finite faithfully flat cover, so the descended universal element represents it globally.

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 Opposite
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {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)
Lean source · statement
def Presentation.pointedRepresentation (M : Presentation K c) :
    (Unrigidified.zeroPresheaf c).RepresentableBy (Over.mk M.toBase)
def

pointedComparisonOver

L56 ↗
JacobianVarieties.Picard.Unpointed.Presentation.pointedComparisonOver
Documentation

The over-scheme isomorphism fixed by the actual two Picard classifications.

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 Opposite
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {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)
Lean source · statement
def Presentation.pointedComparisonOver (M : Presentation K c) :
    Over.mk M.toBase ≅ Over.mk D.toBase
def

pointedComparison

L61 ↗
JacobianVarieties.Picard.Unpointed.Presentation.pointedComparison
Documentation

The actual scheme comparison with any pointed Picard representative.

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 Opposite
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {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)
Lean source · statement
def Presentation.pointedComparison (M : Presentation K c) : M.carrier ≅ D.P
theorem

pointedComparison_over

L64 ↗
JacobianVarieties.Picard.Unpointed.Presentation.pointedComparison_over
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 Opposite
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {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)
Lean source · statement
theorem Presentation.pointedComparison_over (M : Presentation K c) :
    (M.pointedComparison ε h).hom ≫ D.toBase = M.toBase
def

pointedComparison

L72 ↗
JacobianVarieties.Picard.Unpointed.pointedComparison
Documentation

An actual section identifies the fixed unpointed Jacobian with a pointed Picard representative over the original field.

Source context 7 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 Opposite
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {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)
variable (c) [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
Lean source · statement
def pointedComparison : Jacobian K c ≅ D.P
theorem

pointedComparison_over

L75 ↗
JacobianVarieties.Picard.Unpointed.pointedComparison_over
Source context 7 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 Opposite
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable {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)
variable (c) [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
Lean source · statement
theorem pointedComparison_over :
    (pointedComparison c ε h).hom ≫ D.toBase = toBase K c

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