Module

RepresentsRelSubPicKerPoints.lean

Nyll.JacobianVarieties.Picard.RepresentsRelSubPicKerPoints

1 declaration indexed from sourceView source ↗

Module documentation

Dual-number kernel points and rigidified line bundles

Reduction-trivial points of a representing Picard scheme give rigidified dual-number deformations.

Imports11

Imported by15

def

kerPointsToRigKer

L47 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic.kerPointsToRigKer

Documentation

Send a point killed by dual-number reduction to its rigidified deformation class.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
noncomputable section
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
  AlgebraicGeometry.RelPicard NeronModelInfra GoodReductionJacobian
namespace AlgebraicGeometry.RelPicard
section KerPoints
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} {D : RelativePic0Designation R c}

Lean source · full declaration

def RepresentsRelSubPic.kerPointsToRigKer
    (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
    (A : Type u) [CommRing A] [Algebra R A] :
    let L := RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h
    { x : SchemeHomOver (Scheme.TwoAffineOpenCover.specMap R (DualNumber A)) D.toBase //
        dualNumberReduction R A ≫ x.1 = (L.one (Scheme.TwoAffineOpenCover.specMap R A)).1 } →
      RigKerDualNumber c ε A :=
  fun x => Quotient.mk _ ⟨h.poincare.pullbackAlong x.1, by
    let := RepresentsRelSubPic.grpObj (P := algEquivZeroGroupCut c ε) h
    let := (algEquivZeroGroupCut c ε).commGroupObj
      (Opposite.op (Over.mk (Scheme.TwoAffineOpenCover.specMap R A)))
    have h1 := congrArg Subtype.val
      (RepresentsRelSubPic.homEquiv_one (P := algEquivZeroGroupCut c ε) h
        (Over.mk (Scheme.TwoAffineOpenCover.specMap R A)))
    have one_iso : Nonempty ((h.poincare.pullbackAlong
        ((RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h).one
          (Scheme.TwoAffineOpenCover.specMap R A))).L ≅
          (RigidifiedLineBundle.unit (c := c) (ε := ε)
            (Scheme.TwoAffineOpenCover.specMap R A)).L) :=
      Quotient.exact h1
    have hx : GoodReductionJacobian.schemeHomOverComp (dualNumberReduction R A)
        (dualNumberReduction_comp_specMap R A) x.1 =
          (RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h).one
            (Scheme.TwoAffineOpenCover.specMap R A) :=
      Subtype.ext x.2
    rw [← hx] at one_iso
    exact ⟨h.poincare.pullbackAlongPullbackAlongIso x.1 (dualNumberReductionOver R A) ≪≫
      one_iso.some⟩⟩

Module documentation

Dual-number kernel points and rigidified line bundles

Declarations

kerPointsToRigKer