NYLL
Module

RepresentsRelSubPic_mul_comp_eq_of_classifies_rigidify_pullback_of_ofPoint_of_isIso.lean

Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_mul_comp_eq_of_classifies_rigidify_pullback_of_ofPoint_of_isIso
4 declarations indexed from sourceView source ↗

Module documentation

Point divisors and Picard multiplication under a curve isomorphism

Pullback identifies the line bundles and ideal modules of corresponding points. Combining these identifications with rigidification and the Poincare tensor product shows that the induced Picard map carries the specified point classes to their product.

Imports33
Imported by2

Declarations

theorem

poincare_mul

L79 ↗
JacobianVarieties.Picard.Proofs.PointPullback.GenPullIsoAJ.poincare_mul
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PointPullback
attribute [-simp]
  AlgebraicGeometry.Scheme.Modules.toUnitSection_ofUnitSection
  AlgebraicGeometry.Scheme.Modules.pullbackSection_def
  AlgebraicGeometry.Scheme.Modules.ofUnitSection_toUnitSection
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace GenPullIsoAJ
Lean source · statement
theorem poincare_mul {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 : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t D.toBase) :
    Nonempty ((h.poincare.pullbackAlong (h.relativeGroupLaw.mul t x y)).L ≅
      (h.poincare.pullbackAlong x).L ⊗ (h.poincare.pullbackAlong y).L)
theorem

isInvertible_I_ofPoint_field

L89 ↗
JacobianVarieties.Picard.Proofs.PointPullback.GenPullIsoAJ.isInvertible_I_ofPoint_field
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PointPullback
attribute [-simp]
  AlgebraicGeometry.Scheme.Modules.toUnitSection_ofUnitSection
  AlgebraicGeometry.Scheme.Modules.pullbackSection_def
  AlgebraicGeometry.Scheme.Modules.ofUnitSection_toUnitSection
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace GenPullIsoAJ
Lean source · statement
theorem isInvertible_I_ofPoint_field {R : Type u} [CommRing R] {K : Type u} [Field K]
    {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of R)) [IsSeparated c]
    (t : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of R))
    [SmoothOfRelativeDimension 1 (pullback.snd c t)]
    (x : Spec (CommRingCat.of K) ⟶ C) (hx : x ≫ c = t) :
    (RelEffCartierDiv.ofPoint c x hx).I.IsInvertible
theorem

pull_ofPoint

L105 ↗
JacobianVarieties.Picard.Proofs.PointPullback.GenPullIsoAJ.pull_ofPoint
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PointPullback
attribute [-simp]
  AlgebraicGeometry.Scheme.Modules.toUnitSection_ofUnitSection
  AlgebraicGeometry.Scheme.Modules.pullbackSection_def
  AlgebraicGeometry.Scheme.Modules.ofUnitSection_toUnitSection
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
noncomputable section
namespace GenPullIsoAJ
Lean source · statement
theorem pull_ofPoint {R : Type u} [CommRing R] {K : Type u} [Field K] {C C' : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of R))
    (c' : C' ⟶ Spec (CommRingCat.of R)) [IsSeparated c] [IsSeparated c']
    (t : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of R))
    [SmoothOfRelativeDimension 1 (pullback.snd c t)]
    [SmoothOfRelativeDimension 1 (pullback.snd c' t)]
    (π : C' ⟶ C) (hπ : π ≫ c = c') [IsIso π]
    (y : Spec (CommRingCat.of K) ⟶ C) (hy : y ≫ c = t)
    (y' : Spec (CommRingCat.of K) ⟶ C')
    (hy' : y' ≫ c' = t)
    (hyy : y' ≫ π = y) :
    Nonempty ((Scheme.Modules.pullback (curveChange π hπ t)).obj
      (RelEffCartierDiv.ofPoint c y hy).lineBundle ≅
        (RelEffCartierDiv.ofPoint c' y' hy').lineBundle) ∧
      Nonempty ((Scheme.Modules.pullback (curveChange π hπ t)).obj
        (RelEffCartierDiv.ofPoint c y hy).idealModule ≅
        (RelEffCartierDiv.ofPoint c' y' hy').idealModule)
theorem

mul_comp_eq_of_classifies_rigidify_pullback_of_ofPoint_of_isIso

L142 ↗
AlgebraicGeometry.RelPicard.RepresentsRelSubPic.mul_comp_eq_of_classifies_rigidify_pullback_of_ofPoint_of_isIso
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.PointPullback
attribute [-simp]
  AlgebraicGeometry.Scheme.Modules.toUnitSection_ofUnitSection
  AlgebraicGeometry.Scheme.Modules.pullbackSection_def
  AlgebraicGeometry.Scheme.Modules.ofUnitSection_toUnitSection
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
universe u
open GenPullIsoAJ in
with_weak_namespace _root_.AlgebraicGeometry.RelPicard.RepresentsRelSubPic
Lean source · statement
theorem mul_comp_eq_of_classifies_rigidify_pullback_of_ofPoint_of_isIso
    {R : Type u} [CommRing R] {C C' : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of R)}
    {c' : C' ⟶ Spec (CommRingCat.of R)} [IsSeparated c] [IsSeparated c']
    {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}
    {ε' : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c'}
    {D : RelativePic0Designation R c} {D' : RelativePic0Designation R c'}
    (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
    (h' : RepresentsRelSubPic c' ε' (algEquivZeroCut c' ε') D')
    (π : C' ⟶ C) (hπ : π ≫ c = c') [IsIso π]
    (N : SchemeHomOver D.toBase D'.toBase)
    (hN : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (a : SchemeHomOver t D.toBase),
      Nonempty ((h'.poincare.pullbackAlong (NeronModelInfra.schemeHomOverComp a N)).L ≅
        Scheme.Modules.rigidify (rigSection c' t ε') (pullback.snd c' t)
          ((Scheme.Modules.pullback (curveChange π hπ t)).obj (h.poincare.pullbackAlong a).L)))
    {K : Type u} [Field K] (t : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of R))
    [SmoothOfRelativeDimension 1 (pullback.snd c t)]
    [SmoothOfRelativeDimension 1 (pullback.snd c' t)]
    (y : SchemeHomOver t c) (y' xe : SchemeHomOver t c')
    (hy' : y'.1 ≫ π = y.1) (hxe : xe.1 ≫ π = t ≫ ε.1)
    (a : SchemeHomOver t D.toBase)
    (ha : Nonempty ((h.poincare.pullbackAlong a).L ≅
      (RelEffCartierDiv.ofPoint c y.1 y.2).lineBundle ⊗
        (RelEffCartierDiv.ofPoint c (t ≫ ε.1)
          ((Category.assoc _ _ _).trans
            ((congrArg (t ≫ ·) ε.2).trans (Category.comp_id t)))).idealModule))
    (b g : SchemeHomOver t D'.toBase)
    (hb : Nonempty ((h'.poincare.pullbackAlong b).L ≅
      (RelEffCartierDiv.ofPoint c' xe.1 xe.2).lineBundle ⊗
        (RelEffCartierDiv.ofPoint c' (t ≫ ε'.1)
          ((Category.assoc _ _ _).trans
            ((congrArg (t ≫ ·) ε'.2).trans (Category.comp_id t)))).idealModule))
    (hg : Nonempty ((h'.poincare.pullbackAlong g).L ≅
      (RelEffCartierDiv.ofPoint c' y'.1 y'.2).lineBundle ⊗
        (RelEffCartierDiv.ofPoint c' (t ≫ ε'.1)
          ((Category.assoc _ _ _).trans
            ((congrArg (t ≫ ·) ε'.2).trans (Category.comp_id t)))).idealModule)) :
    (RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c' ε') h').mul t
      (NeronModelInfra.schemeHomOverComp a N) b = g

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.