NYLL
Module

JacobianChallenge.lean

Nyll.JacobianVarieties.JacobianChallenge
10 declarations indexed from sourceView source ↗

Module documentation

Jacobians of smooth proper curves in the over category

The Jacobian, its group object, and every Abel--Jacobi map use the same scheme constructed by finite faithfully flat descent without a rational basepoint. The genus is the geometric function-field genus, also identified with actual structure-sheaf cohomology. These declarations implement all nine statements of the algebraic-geometric Jacobian challenge.

Imports9
Imported by1

Declarations

instance

curveIntegral

L47 ↗
AlgebraicGeometry.JacobianChallenge.curveIntegral
Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open NeronModelInfra GoodReductionJacobian
open scoped CategoryTheory.MonObj
namespace AlgebraicGeometry.JacobianChallenge
variable {k : Type u} [Field k] {C : Over (Spec (CommRingCat.of k))}
  [SmoothOfRelativeDimension 1 C.hom] [IsProper C.hom] [GeometricallyIrreducible C.hom]
Lean source · statement
instance curveIntegral : GeometricallyIntegral C.hom
def

genus

L53 ↗
AlgebraicGeometry.JacobianChallenge.genus
Documentation

The geometric genus of a smooth proper curve.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open NeronModelInfra GoodReductionJacobian
open scoped CategoryTheory.MonObj
namespace AlgebraicGeometry.JacobianChallenge
variable {k : Type u} [Field k] {C : Over (Spec (CommRingCat.of k))}
  [SmoothOfRelativeDimension 1 C.hom] [IsProper C.hom] [GeometricallyIrreducible C.hom]
local instance curveIntegral : GeometricallyIntegral C.hom := by
  have _ : GeometricallyConnected C.hom :=
    GeometricallyIrreducible.geometricallyConnected C.hom
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected C.hom
Lean source · statement
def genus (C : Over (Spec (CommRingCat.of k))) [IsProper C.hom]
    [SmoothOfRelativeDimension 1 C.hom] [GeometricallyIrreducible C.hom] : ℕ
def

Jacobian

L58 ↗
AlgebraicGeometry.JacobianChallenge.Jacobian
Documentation

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

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open NeronModelInfra GoodReductionJacobian
open scoped CategoryTheory.MonObj
namespace AlgebraicGeometry.JacobianChallenge
variable {k : Type u} [Field k] {C : Over (Spec (CommRingCat.of k))}
  [SmoothOfRelativeDimension 1 C.hom] [IsProper C.hom] [GeometricallyIrreducible C.hom]
local instance curveIntegral : GeometricallyIntegral C.hom := by
  have _ : GeometricallyConnected C.hom :=
    GeometricallyIrreducible.geometricallyConnected C.hom
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected C.hom
Lean source · statement
def Jacobian (C : Over (Spec (CommRingCat.of k))) [IsProper C.hom]
    [SmoothOfRelativeDimension 1 C.hom] [GeometricallyIrreducible C.hom] :
    Over (Spec (CommRingCat.of k))
instance

instGrpObj

L66 ↗
AlgebraicGeometry.JacobianChallenge.Jacobian.instGrpObj
Documentation

The group object induced by tensor product on the fixed descended Jacobian.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open NeronModelInfra GoodReductionJacobian
open scoped CategoryTheory.MonObj
namespace AlgebraicGeometry.JacobianChallenge
variable {k : Type u} [Field k] {C : Over (Spec (CommRingCat.of k))}
  [SmoothOfRelativeDimension 1 C.hom] [IsProper C.hom] [GeometricallyIrreducible C.hom]
local instance curveIntegral : GeometricallyIntegral C.hom := by
  have _ : GeometricallyConnected C.hom :=
    GeometricallyIrreducible.geometricallyConnected C.hom
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected C.hom
namespace Jacobian
Lean source · statement
instance instGrpObj : GrpObj (Jacobian C)
instance

smoothOfRelativeDimension_genus

L70 ↗
AlgebraicGeometry.JacobianChallenge.Jacobian.smoothOfRelativeDimension_genus
Documentation

The Jacobian has smooth relative dimension equal to the geometric genus.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open NeronModelInfra GoodReductionJacobian
open scoped CategoryTheory.MonObj
namespace AlgebraicGeometry.JacobianChallenge
variable {k : Type u} [Field k] {C : Over (Spec (CommRingCat.of k))}
  [SmoothOfRelativeDimension 1 C.hom] [IsProper C.hom] [GeometricallyIrreducible C.hom]
local instance curveIntegral : GeometricallyIntegral C.hom := by
  have _ : GeometricallyConnected C.hom :=
    GeometricallyIrreducible.geometricallyConnected C.hom
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected C.hom
namespace Jacobian
Lean source · statement
instance smoothOfRelativeDimension_genus :
    SmoothOfRelativeDimension (genus C) (Jacobian C).hom
instance

instIsProper

L75 ↗
AlgebraicGeometry.JacobianChallenge.Jacobian.instIsProper
Documentation

Properness of the fixed Jacobian over the original field.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open NeronModelInfra GoodReductionJacobian
open scoped CategoryTheory.MonObj
namespace AlgebraicGeometry.JacobianChallenge
variable {k : Type u} [Field k] {C : Over (Spec (CommRingCat.of k))}
  [SmoothOfRelativeDimension 1 C.hom] [IsProper C.hom] [GeometricallyIrreducible C.hom]
local instance curveIntegral : GeometricallyIntegral C.hom := by
  have _ : GeometricallyConnected C.hom :=
    GeometricallyIrreducible.geometricallyConnected C.hom
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected C.hom
namespace Jacobian
Lean source · statement
instance instIsProper : IsProper (Jacobian C).hom
instance

instGeometricallyIrreducible

L79 ↗
AlgebraicGeometry.JacobianChallenge.Jacobian.instGeometricallyIrreducible
Documentation

Geometric irreducibility of the fixed Jacobian over the original field.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open NeronModelInfra GoodReductionJacobian
open scoped CategoryTheory.MonObj
namespace AlgebraicGeometry.JacobianChallenge
variable {k : Type u} [Field k] {C : Over (Spec (CommRingCat.of k))}
  [SmoothOfRelativeDimension 1 C.hom] [IsProper C.hom] [GeometricallyIrreducible C.hom]
local instance curveIntegral : GeometricallyIntegral C.hom := by
  have _ : GeometricallyConnected C.hom :=
    GeometricallyIrreducible.geometricallyConnected C.hom
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected C.hom
namespace Jacobian
Lean source · statement
instance instGeometricallyIrreducible : GeometricallyIrreducible (Jacobian C).hom
def

ofCurve

L85 ↗
AlgebraicGeometry.JacobianChallenge.Jacobian.ofCurve
Documentation

The actual point-minus-basepoint Abel--Jacobi morphism in the over category.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open NeronModelInfra GoodReductionJacobian
open scoped CategoryTheory.MonObj
namespace AlgebraicGeometry.JacobianChallenge
variable {k : Type u} [Field k] {C : Over (Spec (CommRingCat.of k))}
  [SmoothOfRelativeDimension 1 C.hom] [IsProper C.hom] [GeometricallyIrreducible C.hom]
local instance curveIntegral : GeometricallyIntegral C.hom := by
  have _ : GeometricallyConnected C.hom :=
    GeometricallyIrreducible.geometricallyConnected C.hom
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected C.hom
namespace Jacobian
Lean source · statement
def ofCurve (P : 𝟙_ (Over (Spec (CommRingCat.of k))) ⟶ C) : C ⟶ Jacobian C
theorem

comp_ofCurve

L92 ↗
AlgebraicGeometry.JacobianChallenge.Jacobian.comp_ofCurve
Documentation

The specified rational basepoint maps to the identity of the same group object.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open NeronModelInfra GoodReductionJacobian
open scoped CategoryTheory.MonObj
namespace AlgebraicGeometry.JacobianChallenge
variable {k : Type u} [Field k] {C : Over (Spec (CommRingCat.of k))}
  [SmoothOfRelativeDimension 1 C.hom] [IsProper C.hom] [GeometricallyIrreducible C.hom]
local instance curveIntegral : GeometricallyIntegral C.hom := by
  have _ : GeometricallyConnected C.hom :=
    GeometricallyIrreducible.geometricallyConnected C.hom
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected C.hom
namespace Jacobian
Lean source · statement
theorem comp_ofCurve (C : Over (Spec (CommRingCat.of k))) [IsProper C.hom]
    [SmoothOfRelativeDimension 1 C.hom] [GeometricallyIrreducible C.hom]
    (P : 𝟙_ (Over (Spec (CommRingCat.of k))) ⟶ C) :
    P ≫ ofCurve P = η[Jacobian C]
theorem

exists_unique_ofCurve_comp

L104 ↗
AlgebraicGeometry.JacobianChallenge.Jacobian.exists_unique_ofCurve_comp
Documentation

Every pointed morphism to an abelian variety factors uniquely through the same Abel--Jacobi morphism and the fixed Jacobian, over the original field.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open NeronModelInfra GoodReductionJacobian
open scoped CategoryTheory.MonObj
namespace AlgebraicGeometry.JacobianChallenge
variable {k : Type u} [Field k] {C : Over (Spec (CommRingCat.of k))}
  [SmoothOfRelativeDimension 1 C.hom] [IsProper C.hom] [GeometricallyIrreducible C.hom]
local instance curveIntegral : GeometricallyIntegral C.hom := by
  have _ : GeometricallyConnected C.hom :=
    GeometricallyIrreducible.geometricallyConnected C.hom
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected C.hom
namespace Jacobian
Lean source · statement
theorem exists_unique_ofCurve_comp
    {k : Type u} [Field k]
    (C : Over (Spec (.of k))) [IsProper C.hom]
    [SmoothOfRelativeDimension 1 C.hom] [GeometricallyIrreducible C.hom]
    (P : 𝟙_ (Over (Spec (.of k))) ⟶ C)
    {A : Over (Spec (.of k))} [Smooth A.hom] [IsProper A.hom] [GrpObj A]
    [GeometricallyIrreducible A.hom] (f : C ⟶ A) (hf : P ≫ f = η[A]) :
    ∃! (g : Jacobian C ⟶ A), f = ofCurve P ≫ g

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