AlgebraicGeometry.RelPicard.RepresentsRelSubPic.existsUnique_addMonoidHom_pts_eq_comp_of_mul_comp
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.AdditivePointMap
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.SmoothProperCurve
universe u
with_weak_namespace _root_.AlgebraicGeometry.RelPicard.RepresentsRelSubPicLean source · statement
theorem existsUnique_addMonoidHom_pts_eq_comp_of_mul_comp
{R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
{ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
{D : RelativePic0Designation R c} (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
(J : Type u) [AddCommGroup J]
(pts : J ≃ SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) D.toBase)
(hadd : ∀ a b : J, Nonempty
((h.poincare.pullbackAlong (pts (a + b))).L ≅
(h.poincare.pullbackAlong (pts a)).L ⊗ (h.poincare.pullbackAlong (pts b)).L))
(ψ : SchemeHomOver D.toBase D.toBase)
(hψmul : ∀ {T : Scheme.{u}} (s : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver s D.toBase),
NeronModelInfra.schemeHomOverComp
((RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h).mul s x y) ψ =
(RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h).mul s
(NeronModelInfra.schemeHomOverComp x ψ) (NeronModelInfra.schemeHomOverComp y ψ)) :
∃! e : J →+ J, ∀ y : J, (pts (e y)).1 = (pts y).1 ≫ ψ.1