AlgebraicCurve.Pic0.exists_relativeGroupLaw_equiv_of_curveModel
The represented Picard group carries the relative group law and Abel–Jacobi normalization.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurve.Pic0
open _root_.JacobianVarieties.Pic0.Proofs.CurveModelGroup
open _root_.CategoryTheory _root_.CategoryTheory.Limits _root_.AlgebraicGeometry
_root_.AlgebraicGeometry.RelPicard
_root_.NeronModelInfra _root_.GoodReductionJacobian _root_.AlgebraicCurve
universe u vLean source · statement
theorem exists_relativeGroupLaw_equiv_of_curveModel
(K : Type u) [Field K] [IsAlgClosed K] (F : Type v) [Field F] [Algebra K F] [IsCurveOver K F]
(M : CurveModel K F)
(s : {q : Spec (CommRingCat.of K) ⟶ M.C // q ≫ M.toBase = 𝟙 _}) :
∃ (J : Scheme.{u}) (f : J ⟶ Spec (CommRingCat.of K)) (L : RelativeGroupLaw K f)
(aj : SchemeHomOver M.toBase f)
(pts : Pic0 K F ≃ SchemeHomOver (𝟙 (Spec (CommRingCat.of K))) f),
AbelianSchemePropertyBundle K f ∧
(∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of K)) (x y : SchemeHomOver t f),
L.mul t x y = L.mul t y x) ∧
s.1 ≫ aj.1 = (L.one (𝟙 (Spec (CommRingCat.of K)))).1 ∧
(∀ x y : Pic0 K F, pts (x + y) = L.mul (𝟙 (Spec (CommRingCat.of K))) (pts x) (pts y)) ∧
∀ x : {q : Spec (CommRingCat.of K) ⟶ M.C // q ≫ M.toBase = 𝟙 _},
∃ Dv : Divisor.degZero (K := K) (F := F),
(Dv : Divisor K F) =
Finsupp.single (M.pointEquivPlace x) 1 - Finsupp.single (M.pointEquivPlace s) 1 ∧
(pts (Pic0.mk Dv)).1 = x.1 ≫ aj.1