AlgebraicGeometry.RelPicard.RepresentsRelSubPic.nonempty_poincare_pullbackAlong_one_iso
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace RepresentsRelSubPic_nonempty_poincare_pullbackAlong_one_iso
universe u
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 scoped CategoryTheory.MonObjLean source · full declaration
theorem
_root_.AlgebraicGeometry.RelPicard.RepresentsRelSubPic.nonempty_poincare_pullbackAlong_one_iso
{R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
{ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
{P : SubPicGroupCondition c ε} {D : RelativePic0Designation R c}
(h : RepresentsRelSubPic c ε P.toSubPicCondition D)
(T : Over (Spec (CommRingCat.of R))) :
let _ : GrpObj (Over.mk D.toBase) := h.grpObj
Nonempty ((h.poincare.pullbackAlong
⟨(1 : T ⟶ Over.mk D.toBase).left, Over.w (1 : T ⟶ Over.mk D.toBase)⟩).L ≅
(RigidifiedLineBundle.unit (c := c) (ε := ε) T.hom).L) := by
intro groupObject
let _ : CommGroup ((relSubPicPresheaf c ε P.toSubPicCondition).obj (Opposite.op T)) :=
P.commGroupObj (Opposite.op T)
have hone := congrArg Subtype.val (h.homEquiv_one T)
exact Quotient.exact hone