NYLL
Module

RigKerDualNumber_kerPointsToRigKer_baseTransport.lean

Nyll.JacobianVarieties.Picard.RigKerDualNumber_kerPointsToRigKer_baseTransport
9 declarations indexed from sourceView source ↗

Module documentation

Kernel point comparison under base transport

Imports6
Imported by2

Declarations

def

castBase

L89 ↗
JacobianVarieties.Picard.Proofs.RigKerTransport.AlgebraicGeometry.RelPicard.BaseTransport.castBase
Documentation

Transport a morphism over a base along an equality of its structure morphisms.

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RigKerTransport
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
namespace BaseTransport
open _root_.AlgebraicGeometry.RelPicard.BaseTransport
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
Lean source · statement
def castBase {B Y X : Scheme.{u}} {s s' : Y ⟶ B} {f : X ⟶ B} (e : s = s') (a : SchemeHomOver s f) :
    SchemeHomOver s' f
theorem

castBase_coe

L94 ↗
JacobianVarieties.Picard.Proofs.RigKerTransport.AlgebraicGeometry.RelPicard.BaseTransport.castBase_coe
Documentation

Transporting the base equality leaves the underlying morphism unchanged.

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RigKerTransport
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
namespace BaseTransport
open _root_.AlgebraicGeometry.RelPicard.BaseTransport
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
Lean source · statement
theorem castBase_coe {B Y X : Scheme.{u}} {s s' : Y ⟶ B} {f : X ⟶ B} (e : s = s')
    (a : SchemeHomOver s f) : (castBase e a).1 = a.1
theorem

mul_castBase

L98 ↗
JacobianVarieties.Picard.Proofs.RigKerTransport.AlgebraicGeometry.RelPicard.BaseTransport.mul_castBase
Documentation

Multiplication of points commutes with transport of the base equality.

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RigKerTransport
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
namespace BaseTransport
open _root_.AlgebraicGeometry.RelPicard.BaseTransport
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
Lean source · statement
theorem mul_castBase {R : Type u} [CommRing R] {A T : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
    (G : RelativeGroupLaw R f) {s s' : T ⟶ Spec (CommRingCat.of R)} (e : s = s') (a b :
      SchemeHomOver s f) :
    G.mul s' (castBase e a) (castBase e b) = castBase e (G.mul s a b)
def

liftPt

L105 ↗
JacobianVarieties.Picard.Proofs.RigKerTransport.AlgebraicGeometry.RelPicard.BaseTransport.liftPt
Documentation

Lift a point to the pullback along the specified base morphism.

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RigKerTransport
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
namespace BaseTransport
open _root_.AlgebraicGeometry.RelPicard.BaseTransport
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
Lean source · statement
def liftPt {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
    (D : RelativePic0Designation R c) (R' : Type u) [CommRing R'] [Algebra R R']
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R')) (a : SchemeHomOver (t ≫ specMap R R')
      D.toBase) :
    SchemeHomOver t (D.baseChange R').toBase
theorem

liftPt_fst

L113 ↗
JacobianVarieties.Picard.Proofs.RigKerTransport.AlgebraicGeometry.RelPicard.BaseTransport.liftPt_fst
Documentation

The first projection of a lifted point is the original point.

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RigKerTransport
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
namespace BaseTransport
open _root_.AlgebraicGeometry.RelPicard.BaseTransport
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
Lean source · statement
theorem liftPt_fst {R : Type u} [CommRing R] {C : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of R)}
    (D : RelativePic0Designation R c) (R' : Type u) [CommRing R'] [Algebra R R']
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R')) (a : SchemeHomOver (t ≫ specMap R R')
      D.toBase) :
    (liftPt D R' t a).1 ≫ pullback.fst D.toBase (specMap R R') = a.1
theorem

eq_liftPt

L122 ↗
JacobianVarieties.Picard.Proofs.RigKerTransport.AlgebraicGeometry.RelPicard.BaseTransport.eq_liftPt
Documentation

A point of the pullback is determined by its first projection.

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RigKerTransport
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
namespace BaseTransport
open _root_.AlgebraicGeometry.RelPicard.BaseTransport
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
Lean source · statement
theorem eq_liftPt {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
    (D : RelativePic0Designation R c) (R' : Type u) [CommRing R'] [Algebra R R']
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R')) (z : SchemeHomOver t (D.baseChange
      R').toBase)
    (a : SchemeHomOver (t ≫ specMap R R') D.toBase)
    (hz : z.1 ≫ pullback.fst D.toBase (specMap R R') = a.1) : z = liftPt D R' t a
theorem

poincare_liftPt_iso

L134 ↗
JacobianVarieties.Picard.Proofs.RigKerTransport.AlgebraicGeometry.RelPicard.BaseTransport.poincare_liftPt_iso
Documentation

Compare the Poincare modules at a point and its base change lift.

Source context 19 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RigKerTransport
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
namespace BaseTransport
open _root_.AlgebraicGeometry.RelPicard.BaseTransport
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
Lean source · statement
theorem poincare_liftPt_iso {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)
    (R' : Type u) [CommRing R'] [Algebra R R']
    (h' : RepresentsRelSubPic (baseChange R c R') (sectionBaseChange R' ε)
      (algEquivZeroCut (baseChange R c R') (sectionBaseChange R' ε)) (D.baseChange R'))
    (hP : Nonempty (h'.poincare.L ≅ (BaseChange.ofR c ε R'
      (h.poincare.pullbackAlong ⟨pullback.fst D.toBase (specMap R R'), pullback.condition⟩)).L))
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R')) (a : SchemeHomOver (t ≫ specMap R R')
      D.toBase) :
    Nonempty ((h'.poincare.pullbackAlong (liftPt D R' t a)).L ≅
      (Scheme.Modules.pullback (BaseChange.κ c R' t).hom).obj (h.poincare.pullbackAlong a).L)
theorem

kerPointsToRigKer_baseTransport_liftPt

L224 ↗
JacobianVarieties.Picard.Proofs.RigKerTransport.AlgebraicGeometry.RelPicard.RigKerDualNumber.kerPointsToRigKer_baseTransport_liftPt
Documentation

The rigidified kernel class of a lifted point agrees with base transport.

Source context 23 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RigKerTransport
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
noncomputable section
attribute [local simp] AlgebraicGeometry.RelPicard.BaseTransport.castBase_coe
attribute [local simp] AlgebraicGeometry.RelPicard.BaseTransport.liftPt_fst
namespace AlgebraicGeometry
namespace RelPicard
namespace RigKerDualNumber
open _root_.AlgebraicGeometry.RelPicard.RigKerDualNumber
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard.BaseTransport
open AlgebraicGeometry.RelPicard.BaseTransport
Lean source · statement
theorem kerPointsToRigKer_baseTransport_liftPt
    {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)
    (R' : Type u) [CommRing R'] [Algebra R R']
    (h' : RepresentsRelSubPic (baseChange R c R') (sectionBaseChange R' ε)
      (algEquivZeroCut (baseChange R c R') (sectionBaseChange R' ε)) (D.baseChange R'))
    (hP : Nonempty (h'.poincare.L ≅ (BaseChange.ofR c ε R'
      (h.poincare.pullbackAlong ⟨pullback.fst D.toBase (specMap R R'), pullback.condition⟩)).L))
    (B : Type u) [CommRing B] [Algebra R' B] [Algebra R B] [IsScalarTower R R' B]
    (x : { x : SchemeHomOver (Scheme.TwoAffineOpenCover.specMap R (DualNumber B)) D.toBase //
      dualNumberReduction R B ≫ x.1 =
        ((RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h).one
          (Scheme.TwoAffineOpenCover.specMap R B)).1 })
    (hx' : dualNumberReduction R' B ≫
        (liftPt D R' (Scheme.TwoAffineOpenCover.specMap R' (DualNumber B))
          (castBase (tower_dualNumber R' B) x.1)).1 =
      ((RepresentsRelSubPic.relativeGroupLaw
          (P := algEquivZeroGroupCut (baseChange R c R') (sectionBaseChange R' ε)) h').one
        (Scheme.TwoAffineOpenCover.specMap R' B)).1) :
    baseTransport R' c ε B (h.kerPointsToRigKer B x) =
      h'.kerPointsToRigKer B
        ⟨liftPt D R' (Scheme.TwoAffineOpenCover.specMap R' (DualNumber B)) (castBase
          (tower_dualNumber R' B) x.1),
          hx'⟩
theorem

kerPointsToRigKer_baseTransport

L299 ↗
AlgebraicGeometry.RelPicard.RigKerDualNumber.kerPointsToRigKer_baseTransport
Documentation

The kernel point comparison commutes with base transport.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicGeometry.RelPicard.RigKerDualNumber
open _root_.JacobianVarieties.Picard.Proofs.RigKerTransport
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
attribute [local simp] BaseTransport.castBase_coe
attribute [local simp] BaseTransport.liftPt_fst
open _root_.AlgebraicGeometry.RelPicard.BaseTransport
  _root_.JacobianVarieties.Picard.Proofs.RigKerTransport.AlgebraicGeometry.RelPicard.BaseTransport
  in
open JacobianVarieties.Picard.Proofs.RigKerTransport.AlgebraicGeometry.RelPicard.RigKerDualNumber in
Lean source · statement
theorem kerPointsToRigKer_baseTransport
    {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)
    (R' : Type u) [CommRing R'] [Algebra R R']
    (h' : RepresentsRelSubPic (baseChange R c R') (sectionBaseChange R' ε)
      (algEquivZeroCut (baseChange R c R') (sectionBaseChange R' ε)) (D.baseChange R'))
    (hP : Nonempty (h'.poincare.L ≅ (BaseChange.ofR c ε R'
      (h.poincare.pullbackAlong ⟨pullback.fst D.toBase (specMap R R'), pullback.condition⟩)).L))
    (B : Type u) [CommRing B] [Algebra R' B] [Algebra R B] [IsScalarTower R R' B]
    (x : { x : SchemeHomOver (Scheme.TwoAffineOpenCover.specMap R (DualNumber B)) D.toBase //
      dualNumberReduction R B ≫ x.1 =
        ((RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) h).one
          (Scheme.TwoAffineOpenCover.specMap R B)).1 })
    (x' : { x' : SchemeHomOver (Scheme.TwoAffineOpenCover.specMap R' (DualNumber B)) (D.baseChange
      R').toBase //
      dualNumberReduction R' B ≫ x'.1 =
        ((RepresentsRelSubPic.relativeGroupLaw
          (P := algEquivZeroGroupCut (baseChange R c R') (sectionBaseChange R' ε)) h').one
          (Scheme.TwoAffineOpenCover.specMap R' B)).1 })
    (hxx' : x'.1.1 ≫ pullback.fst D.toBase (specMap R R') = x.1.1) :
    RigKerDualNumber.baseTransport R' c ε B (h.kerPointsToRigKer B x) = h'.kerPointsToRigKer B x'

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