AlgebraicCurve.Pic0.exists_jacobianPack_of_isAlgClosed
The curve has a smooth proper connected Jacobian with the specified addition law.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurve.Pic0
open _root_.JacobianVarieties.Pic0.Proofs.Pic0_exists_jacobianPack_of_isAlgClosed
open _root_.CategoryTheory _root_.CategoryTheory.Limits _root_.AlgebraicGeometry
_root_.AlgebraicCurve _root_.NeronModelInfra
_root_.GoodReductionJacobian _root_.AlgebraicGeometry.RelPicardLean source · statement
theorem exists_jacobianPack_of_isAlgClosed
(K F : Type*) [Field K] [Field F] [Algebra K F]
[IsAlgClosed K]
(hfg : ∃ x : F, Transcendental K x ∧
FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
[IsCurveOver K F] :
∃ (J : AlgebraicGeometry.Scheme) (c : J ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)),
AlgebraicGeometry.Smooth c ∧ AlgebraicGeometry.IsProper c ∧ ConnectedSpace J ∧
∃ (mul : CategoryTheory.Limits.pullback c c ⟶ J)
(pts : Pic0 K F ≃
{σ : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ J // σ ≫ c = 𝟙 _}),
∀ x y : Pic0 K F, (pts (x + y)).1 =
CategoryTheory.Limits.pullback.lift (pts x).1 (pts y).1
((pts x).2.trans (pts y).2.symm) ≫ mul