Module

GenusOneAbelJacobiIsomorphism.lean

Nyll.JacobianVarieties.Albanese.GenusOneAbelJacobiIsomorphism

1 declaration indexed from sourceView source ↗

Module documentation

The actual Abel--Jacobi isomorphism of a pointed genus-one curve

The Picard construction supplies one designation, one representing Poincaré family, and one Abel--Jacobi morphism. The point-difference theorem and that same family's point comparison make the actual morphism bijective on rational points. In characteristic zero, the proper smooth curve criterion makes it an isomorphism.

The imported Picard construction retains its Anthropic FLT provenance in its source.

Imports9

Imported by2

theorem

exists_abelJacobi_isIso_of_genus_one

L41 ↗

AlgebraicCurve.CurveModel.exists_abelJacobi_isIso_of_genus_one

Documentation

The constructed Abel--Jacobi map of a pointed genus-one curve is an isomorphism with its actual relative Picard scheme.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
namespace AlgebraicCurve.CurveModel
variable {K F : Type} [Field K] [IsAlgClosed K] [CharZero K]
  [Field F] [Algebra K F] [IsCurveOver K F]

Lean source · statement

theorem exists_abelJacobi_isIso_of_genus_one (M : CurveModel K F)
    (hg : genusFF K F = 1)
    (s : SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) M.toBase) :
    ∃ (D : RelativePic0Designation K M.toBase)
      (_ : RepresentsRelSubPic M.toBase s (algEquivZeroCut M.toBase s) D)
      (aj : SchemeHomOver M.toBase D.toBase),
      Smooth D.toBase ∧ IsProper D.toBase ∧ GeometricallyConnected D.toBase ∧
      s.1 ≫ aj.1 = D.zeroSection ∧ IsIso aj.1

Module documentation

The actual Abel--Jacobi isomorphism of a pointed genus-one curve

Declarations

exists_abelJacobi_isIso_of_genus_one