Module

UnpointedJacobian.lean

Nyll.JacobianVarieties.Picard.UnpointedJacobian

15 declarations indexed from sourceView source ↗

Module documentation

A Jacobian over an arbitrary field without a rational basepoint

A single effective descent presentation is chosen from the proved existence theorem. Its carrier and structure map are retained by all public constructions. The relative group law is constructed from tensor product, and its dimension is the geometric genus of the original curve.

Imports6

Imported by3

structure

Presentation

L36 ↗

JacobianVarieties.Picard.Unpointed.Presentation

Documentation

The actual finite-extension presentation retained by the Jacobian construction. All of these data are supplied by the proved existence theorem below.

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 (K : Type u) [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))

Lean source · full declaration

structure Presentation where
  /-- A finite extension on which the curve has a section. -/
  extension : Type u
  /-- The field structure of the chosen extension. -/
  extensionField : Field extension
  /-- The specified ground-field algebra structure. -/
  extensionAlgebra : Algebra K extension
  /-- Finiteness of the actual extension. -/
  extensionFinite : Module.Finite K extension
  /-- The section constructed after extending the ground field. -/
  localSection : SchemeHomOver (𝟙 (Spec (CommRingCat.of extension))) (baseChange K c extension)
  /-- The actual pointed Picard representative after extension. -/
  localPicard : RelativePic0Designation extension (baseChange K c extension)
  /-- Its universal line-bundle classification. -/
  localRepresentation : RepresentsRelSubPic (baseChange K c extension) localSection
    (algEquivZeroCut (baseChange K c extension) localSection) localPicard
  /-- The effective descent carrier over the ground field. -/
  carrier : Scheme.{u}
  /-- Its structure morphism. -/
  toBase : carrier ⟶ Spec (CommRingCat.of K)
  /-- Smoothness supplied by faithfully flat descent. -/
  smooth : Smooth toBase
  /-- Properness supplied by faithfully flat descent. -/
  proper : IsProper toBase
  /-- Geometric connectedness supplied by faithfully flat descent. -/
  geometricallyConnected : GeometricallyConnected toBase
  /-- The effective-descent comparison with the local Picard representative. -/
  comparison : pullback toBase (specMap K extension) ≅ localPicard.P
  /-- The comparison lies over the extension field. -/
  comparison_over : comparison.hom ≫ localPicard.toBase = pullback.snd toBase (specMap K extension)
  /-- The actual canonical descent action is respected by the comparison. -/
  comparison_action :
    DescentAction.eRel (specMap K extension) localPicard.toBase toBase comparison comparison_over ≫
        (descentAction c extension localSection localRepresentation).act =
      (DescentAction.canonical (specMap K extension) toBase).act ≫ comparison.hom

instance

curveGeometricallyIntegral

L74 ↗

JacobianVarieties.Picard.Unpointed.curveGeometricallyIntegral

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
noncomputable section
namespace JacobianVarieties.Picard.Unpointed
variable (K : Type u) [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
variable [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]

Lean source · statement

instance curveGeometricallyIntegral : GeometricallyIntegral c

theorem

nonempty_presentation

L79 ↗

JacobianVarieties.Picard.Unpointed.nonempty_presentation

Documentation

Construct the entire presentation using a closed point and effective descent.

Source context 8 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 (K : Type u) [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
variable [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
local instance curveGeometricallyIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c

Lean source · statement

theorem nonempty_presentation : Nonempty (Presentation K c)

def

presentation

L85 ↗

JacobianVarieties.Picard.Unpointed.presentation

Documentation

One fixed effective-descent presentation; all later definitions share this value.

Source context 8 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 (K : Type u) [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
variable [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
local instance curveGeometricallyIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c

Lean source · statement

def presentation : Presentation K c

def

Jacobian

L88 ↗

JacobianVarieties.Picard.Unpointed.Jacobian

Documentation

The Jacobian scheme over the original field, with no rational point required.

Source context 8 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 (K : Type u) [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
variable [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
local instance curveGeometricallyIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c

Lean source · statement

def Jacobian : Scheme.{u}

def

toBase

L91 ↗

JacobianVarieties.Picard.Unpointed.toBase

Documentation

The structure morphism of the same chosen Jacobian.

Source context 8 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 (K : Type u) [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
variable [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
local instance curveGeometricallyIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c

Lean source · statement

def toBase : Jacobian K c ⟶ Spec (CommRingCat.of K)

def

groupLaw

L94 ↗

JacobianVarieties.Picard.Unpointed.groupLaw

Documentation

The tensor-product relative group law on the chosen Jacobian.

Source context 8 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 (K : Type u) [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
variable [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
local instance curveGeometricallyIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c

Lean source · statement

def groupLaw : RelativeGroupLaw K (toBase K c)

theorem

groupLaw_commutative

L101 ↗

JacobianVarieties.Picard.Unpointed.groupLaw_commutative

Source context 8 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 (K : Type u) [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
variable [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
local instance curveGeometricallyIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c

Lean source · statement

theorem groupLaw_commutative : (groupLaw K c).IsCommutative

theorem

smooth

L109 ↗

JacobianVarieties.Picard.Unpointed.smooth

Source context 8 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 (K : Type u) [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
variable [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
local instance curveGeometricallyIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c

Lean source · statement

theorem smooth : Smooth (toBase K c)

theorem

proper

L111 ↗

JacobianVarieties.Picard.Unpointed.proper

Source context 8 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 (K : Type u) [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
variable [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
local instance curveGeometricallyIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c

Lean source · statement

theorem proper : IsProper (toBase K c)

theorem

geometricallyConnected

L113 ↗

JacobianVarieties.Picard.Unpointed.geometricallyConnected

Source context 8 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 (K : Type u) [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
variable [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
local instance curveGeometricallyIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c

Lean source · statement

theorem geometricallyConnected : GeometricallyConnected (toBase K c)

theorem

dimension_and_geometricallyIntegral

L117 ↗

JacobianVarieties.Picard.Unpointed.dimension_and_geometricallyIntegral

Documentation

Smooth relative dimension and geometric integrality concern the same chosen carrier.

Source context 8 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 (K : Type u) [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
variable [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
local instance curveGeometricallyIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c

Lean source · statement

theorem dimension_and_geometricallyIntegral :
    SmoothOfRelativeDimension (geometricGenus K c) (toBase K c) ∧
      GeometricallyIntegral (toBase K c)

theorem

smoothOfRelativeDimension

L130 ↗

JacobianVarieties.Picard.Unpointed.smoothOfRelativeDimension

Source context 8 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 (K : Type u) [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
variable [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
local instance curveGeometricallyIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c

Lean source · statement

theorem smoothOfRelativeDimension :
    SmoothOfRelativeDimension (geometricGenus K c) (toBase K c)

theorem

geometricallyIntegral

L134 ↗

JacobianVarieties.Picard.Unpointed.geometricallyIntegral

Source context 8 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 (K : Type u) [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
variable [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
local instance curveGeometricallyIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c

Lean source · statement

theorem geometricallyIntegral : GeometricallyIntegral (toBase K c)

theorem

abelianSchemePropertyBundle

L138 ↗

JacobianVarieties.Picard.Unpointed.abelianSchemePropertyBundle

Documentation

The constructed Jacobian is an abelian variety over the original arbitrary field.

Source context 8 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 (K : Type u) [Field K] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of K))
variable [IsProper c] [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
local instance curveGeometricallyIntegral : GeometricallyIntegral c := by
  have _ : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected c

Lean source · statement

theorem abelianSchemePropertyBundle : AbelianSchemePropertyBundle K (toBase K c)

Module documentation

A Jacobian over an arbitrary field without a rational basepoint

Declarations