Module

RepresentsRelSubPic_nonempty_poincare_pullbackAlong_mul_iso.lean

Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_nonempty_poincare_pullbackAlong_mul_iso

1 declaration indexed from sourceView source ↗

Module documentation

Compare the Poincare bundle along multiplication with the tensor product of its two pullbacks.

Imports6

Imported by17

theorem

nonempty_poincare_pullbackAlong_mul_iso

L42 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic.nonempty_poincare_pullbackAlong_mul_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_mul_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.MonObj

Lean source · full declaration

theorem
    _root_.AlgebraicGeometry.RelPicard.RepresentsRelSubPic.nonempty_poincare_pullbackAlong_mul_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))} (a b : T ⟶ Over.mk D.toBase) :
    let _ : GrpObj (Over.mk D.toBase) := h.grpObj
    Nonempty ((h.poincare.pullbackAlong ⟨(a * b).left, Over.w (a * b)⟩).L ≅
      ((h.poincare.pullbackAlong ⟨a.left, Over.w a⟩).tensor (h.poincare.pullbackAlong ⟨b.left,
        Over.w b⟩)).L) := by
  intro groupObject
  let _ : CommGroup ((relSubPicPresheaf c ε P.toSubPicCondition).obj (Opposite.op T)) :=
    P.commGroupObj (Opposite.op T)
  have hmul := congrArg Subtype.val (h.homEquiv_mul T a b)
  exact Quotient.exact hmul

Module documentation

Declarations

nonempty_poincare_pullbackAlong_mul_iso