Module

RepresentsRelSubPic_nonempty_poincare_pullbackAlong_iso_rigidify_normModule_baseChange.lean

Nyll.JacobianVarieties.Picard.RepresentsRelSubPic_nonempty_poincare_pullbackAlong_iso_rigidify_normModule_baseChange

16 declarations indexed from sourceView source ↗

Module documentation

Base change of the norm Poincaré comparison

Compare the represented norm transformation and its Poincaré family after base change.

Imports41

Imported by2

theorem

isPullback_of_mono

L93 ↗

JacobianVarieties.Picard.Proofs.NormPoincareBaseChange.T2Sol.isPullback_of_mono

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.NormPoincareBaseChange
attribute [-simp]
  PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app TwoChartCech.Mumford.dK_apply
  TwoChartCech.Mumford.ι0_apply TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply
  TwoChartCech.KerCoprod.ι1_apply TwoChartCech.KerCoprod.ι0_apply
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 _root_.AlgebraicCurve
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace T2Sol
section MonoBase
variable (R : Type u) [CommRing R] (K : Type u) [CommRing K] [Algebra R K] [Mono (specMap R K)]
  {Y T : Scheme.{u}} (y : Y ⟶ Spec (.of K)) (t : T ⟶ Spec (.of K))

Lean source · statement

theorem isPullback_of_mono :
    IsPullback (pullback.fst y t) (pullback.snd y t) (y ≫ specMap R K) (t ≫ specMap R K)

def

eY

L99 ↗

JacobianVarieties.Picard.Proofs.NormPoincareBaseChange.T2Sol.eY

Documentation

The pullback comparison induced by a monomorphism of base spectra.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.NormPoincareBaseChange
attribute [-simp]
  PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app TwoChartCech.Mumford.dK_apply
  TwoChartCech.Mumford.ι0_apply TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply
  TwoChartCech.KerCoprod.ι1_apply TwoChartCech.KerCoprod.ι0_apply
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 _root_.AlgebraicCurve
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace T2Sol
section MonoBase
variable (R : Type u) [CommRing R] (K : Type u) [CommRing K] [Algebra R K] [Mono (specMap R K)]
  {Y T : Scheme.{u}} (y : Y ⟶ Spec (.of K)) (t : T ⟶ Spec (.of K))

Lean source · statement

def eY : Limits.pullback y t ≅ Limits.pullback (y ≫ specMap R K) (t ≫ specMap R K)

theorem

eY_hom_fst

L102 ↗

JacobianVarieties.Picard.Proofs.NormPoincareBaseChange.T2Sol.eY_hom_fst

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.NormPoincareBaseChange
attribute [-simp]
  PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app TwoChartCech.Mumford.dK_apply
  TwoChartCech.Mumford.ι0_apply TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply
  TwoChartCech.KerCoprod.ι1_apply TwoChartCech.KerCoprod.ι0_apply
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 _root_.AlgebraicCurve
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace T2Sol
section MonoBase
variable (R : Type u) [CommRing R] (K : Type u) [CommRing K] [Algebra R K] [Mono (specMap R K)]
  {Y T : Scheme.{u}} (y : Y ⟶ Spec (.of K)) (t : T ⟶ Spec (.of K))

Lean source · statement

theorem eY_hom_fst :
    (eY R K y t).hom ≫ pullback.fst (y ≫ specMap R K) (t ≫ specMap R K) = pullback.fst y t

theorem

eY_hom_snd

L106 ↗

JacobianVarieties.Picard.Proofs.NormPoincareBaseChange.T2Sol.eY_hom_snd

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.NormPoincareBaseChange
attribute [-simp]
  PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app TwoChartCech.Mumford.dK_apply
  TwoChartCech.Mumford.ι0_apply TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply
  TwoChartCech.KerCoprod.ι1_apply TwoChartCech.KerCoprod.ι0_apply
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 _root_.AlgebraicCurve
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace T2Sol
section MonoBase
variable (R : Type u) [CommRing R] (K : Type u) [CommRing K] [Algebra R K] [Mono (specMap R K)]
  {Y T : Scheme.{u}} (y : Y ⟶ Spec (.of K)) (t : T ⟶ Spec (.of K))

Lean source · statement

theorem eY_hom_snd :
    (eY R K y t).hom ≫ pullback.snd (y ≫ specMap R K) (t ≫ specMap R K) = pullback.snd y t

theorem

eY_curveChange

L120 ↗

JacobianVarieties.Picard.Proofs.NormPoincareBaseChange.T2Sol.eY_curveChange

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.NormPoincareBaseChange
attribute [-simp]
  PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app TwoChartCech.Mumford.dK_apply
  TwoChartCech.Mumford.ι0_apply TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply
  TwoChartCech.KerCoprod.ι1_apply TwoChartCech.KerCoprod.ι0_apply
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 _root_.AlgebraicCurve
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace T2Sol
section Squares
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (K : Type u) [CommRing
  K] [Algebra R K]
  [Mono (specMap R K)] {Y T : Scheme.{u}} (y : Y ⟶ Spec (.of K)) (t : T ⟶ Spec (.of K))
  (π : Y ⟶ C) (Hπ : π ≫ c = y ≫ specMap R K) (Hπ₁ : pullback.lift π y Hπ ≫
    SmoothProperCurve.baseChange R c K = y)

Lean source · statement

theorem eY_curveChange :
    (eY R K y t).hom ≫ curveChange (c' := y ≫ specMap R K) π Hπ (t ≫ specMap R K) =
      curveChange (c' := y) (pullback.lift π y Hπ) Hπ₁ t ≫ (BaseChange.κ c K t).hom

theorem

eY_inv_curveChange

L131 ↗

JacobianVarieties.Picard.Proofs.NormPoincareBaseChange.T2Sol.eY_inv_curveChange

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.NormPoincareBaseChange
attribute [-simp]
  PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app TwoChartCech.Mumford.dK_apply
  TwoChartCech.Mumford.ι0_apply TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply
  TwoChartCech.KerCoprod.ι1_apply TwoChartCech.KerCoprod.ι0_apply
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 _root_.AlgebraicCurve
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace T2Sol
section Squares
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (K : Type u) [CommRing
  K] [Algebra R K]
  [Mono (specMap R K)] {Y T : Scheme.{u}} (y : Y ⟶ Spec (.of K)) (t : T ⟶ Spec (.of K))
  (π : Y ⟶ C) (Hπ : π ≫ c = y ≫ specMap R K) (Hπ₁ : pullback.lift π y Hπ ≫
    SmoothProperCurve.baseChange R c K = y)

Lean source · statement

theorem eY_inv_curveChange :
    (eY R K y t).inv ≫ curveChange (c' := y) (pullback.lift π y Hπ) Hπ₁ t =
      curveChange (c' := y ≫ specMap R K) π Hπ (t ≫ specMap R K) ≫ (BaseChange.κ c K t).inv

theorem

isPullback_curveChange

L137 ↗

JacobianVarieties.Picard.Proofs.NormPoincareBaseChange.T2Sol.isPullback_curveChange

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.NormPoincareBaseChange
attribute [-simp]
  PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app TwoChartCech.Mumford.dK_apply
  TwoChartCech.Mumford.ι0_apply TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply
  TwoChartCech.KerCoprod.ι1_apply TwoChartCech.KerCoprod.ι0_apply
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 _root_.AlgebraicCurve
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace T2Sol
section Squares
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (K : Type u) [CommRing
  K] [Algebra R K]
  [Mono (specMap R K)] {Y T : Scheme.{u}} (y : Y ⟶ Spec (.of K)) (t : T ⟶ Spec (.of K))
  (π : Y ⟶ C) (Hπ : π ≫ c = y ≫ specMap R K) (Hπ₁ : pullback.lift π y Hπ ≫
    SmoothProperCurve.baseChange R c K = y)

Lean source · statement

theorem isPullback_curveChange :
    IsPullback (eY R K y t).inv (curveChange (c' := y ≫ specMap R K) π Hπ (t ≫ specMap R K))
      (curveChange (c' := y) (pullback.lift π y Hπ) Hπ₁ t) (BaseChange.κ c K t).inv

theorem

isPullback_fst_curveChange

L143 ↗

JacobianVarieties.Picard.Proofs.NormPoincareBaseChange.T2Sol.isPullback_fst_curveChange

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.NormPoincareBaseChange
attribute [-simp]
  PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app TwoChartCech.Mumford.dK_apply
  TwoChartCech.Mumford.ι0_apply TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply
  TwoChartCech.KerCoprod.ι1_apply TwoChartCech.KerCoprod.ι0_apply
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 _root_.AlgebraicCurve
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace T2Sol
section Squares
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (K : Type u) [CommRing
  K] [Algebra R K]
  [Mono (specMap R K)] {Y T : Scheme.{u}} (y : Y ⟶ Spec (.of K)) (t : T ⟶ Spec (.of K))
  (π : Y ⟶ C) (Hπ : π ≫ c = y ≫ specMap R K) (Hπ₁ : pullback.lift π y Hπ ≫
    SmoothProperCurve.baseChange R c K = y)
omit [Mono (specMap R K)] in

Lean source · statement

theorem isPullback_fst_curveChange :
    IsPullback (pullback.fst y t) (curveChange (c' := y) (pullback.lift π y Hπ) Hπ₁ t)
      (pullback.lift π y Hπ)
      (pullback.fst (SmoothProperCurve.baseChange R c K) t)

theorem

finrank_curveChange

L150 ↗

JacobianVarieties.Picard.Proofs.NormPoincareBaseChange.T2Sol.finrank_curveChange

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.NormPoincareBaseChange
attribute [-simp]
  PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app TwoChartCech.Mumford.dK_apply
  TwoChartCech.Mumford.ι0_apply TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply
  TwoChartCech.KerCoprod.ι1_apply TwoChartCech.KerCoprod.ι0_apply
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 _root_.AlgebraicCurve
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace T2Sol
section Squares
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (K : Type u) [CommRing
  K] [Algebra R K]
  [Mono (specMap R K)] {Y T : Scheme.{u}} (y : Y ⟶ Spec (.of K)) (t : T ⟶ Spec (.of K))
  (π : Y ⟶ C) (Hπ : π ≫ c = y ≫ specMap R K) (Hπ₁ : pullback.lift π y Hπ ≫
    SmoothProperCurve.baseChange R c K = y)
omit [Mono (specMap R K)] in

Lean source · statement

theorem finrank_curveChange [Flat (pullback.lift π y Hπ)] [IsFinite (pullback.lift π y Hπ)] (z) :
    (curveChange (c' := y) (pullback.lift π y Hπ) Hπ₁ t).finrank z =
      (pullback.lift π y Hπ).finrank (pullback.fst (SmoothProperCurve.baseChange R c K) t z)

def

pullbackRigidifyIso

L163 ↗

JacobianVarieties.Picard.Proofs.NormPoincareBaseChange.T2Sol.pullbackRigidifyIso

Documentation

Pullback commutes with rigidification along the compatible section and projection.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.NormPoincareBaseChange
attribute [-simp]
  PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app TwoChartCech.Mumford.dK_apply
  TwoChartCech.Mumford.ι0_apply TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply
  TwoChartCech.KerCoprod.ι1_apply TwoChartCech.KerCoprod.ι0_apply
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 _root_.AlgebraicCurve
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace T2Sol
section Rigidify
variable {T P P' : Scheme.{u}} (σ : T ⟶ P) (q : P ⟶ T) (σ' : T ⟶ P') (q' : P' ⟶ T) (e : P' ⟶ P)
  (hσ : σ' ≫ e = σ) (hq : e ≫ q = q')

Lean source · statement

def pullbackRigidifyIso (L : P.Modules) :
    (Scheme.Modules.pullback e).obj (Scheme.Modules.rigidify σ q L) ≅
      Scheme.Modules.rigidify σ' q' ((Scheme.Modules.pullback e).obj L)

def

fstPoint

L193 ↗

JacobianVarieties.Picard.Proofs.NormPoincareBaseChange.T2Sol.fstPoint

Documentation

The relative point obtained from a base-changed point by the first projection.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.NormPoincareBaseChange
attribute [-simp]
  PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app TwoChartCech.Mumford.dK_apply
  TwoChartCech.Mumford.ι0_apply TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply
  TwoChartCech.KerCoprod.ι1_apply TwoChartCech.KerCoprod.ι0_apply
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 _root_.AlgebraicCurve
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace T2Sol
section Classify
open AlgebraicGeometry.RelPicard.BaseTransport
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙
  (Spec (.of R))) c)
  (K : Type u) [CommRing K] [Algebra R K]
  (D : RelativePic0Designation R c) (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
  (h' : RepresentsRelSubPic (SmoothProperCurve.baseChange R c K)
    (SmoothProperCurve.sectionBaseChange K ε)
    (algEquivZeroCut (SmoothProperCurve.baseChange R c K) (SmoothProperCurve.sectionBaseChange K
      ε)) (D.baseChange K))
  (hP : Nonempty (h'.poincare.L ≅ (BaseChange.ofR c ε K
    (h.poincare.pullbackAlong ⟨pullback.fst D.toBase (specMap R K), pullback.condition⟩)).L))
  {T : Scheme.{u}} (t : T ⟶ Spec (.of K))

Lean source · statement

def fstPoint (b : SchemeHomOver t (D.baseChange K).toBase) :
    SchemeHomOver (t ≫ specMap R K) D.toBase

theorem

fstPoint_coe

L197 ↗

JacobianVarieties.Picard.Proofs.NormPoincareBaseChange.T2Sol.fstPoint_coe

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.NormPoincareBaseChange
attribute [-simp]
  PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app TwoChartCech.Mumford.dK_apply
  TwoChartCech.Mumford.ι0_apply TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply
  TwoChartCech.KerCoprod.ι1_apply TwoChartCech.KerCoprod.ι0_apply
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 _root_.AlgebraicCurve
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace T2Sol
section Classify
open AlgebraicGeometry.RelPicard.BaseTransport
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙
  (Spec (.of R))) c)
  (K : Type u) [CommRing K] [Algebra R K]
  (D : RelativePic0Designation R c) (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
  (h' : RepresentsRelSubPic (SmoothProperCurve.baseChange R c K)
    (SmoothProperCurve.sectionBaseChange K ε)
    (algEquivZeroCut (SmoothProperCurve.baseChange R c K) (SmoothProperCurve.sectionBaseChange K
      ε)) (D.baseChange K))
  (hP : Nonempty (h'.poincare.L ≅ (BaseChange.ofR c ε K
    (h.poincare.pullbackAlong ⟨pullback.fst D.toBase (specMap R K), pullback.condition⟩)).L))
  {T : Scheme.{u}} (t : T ⟶ Spec (.of K))

Lean source · statement

theorem fstPoint_coe (b : SchemeHomOver t (D.baseChange K).toBase) :
    (fstPoint c K D t b).1 = b.1 ≫ pullback.fst D.toBase (specMap R K)

def

poincareFstIso

L201 ↗

JacobianVarieties.Picard.Proofs.NormPoincareBaseChange.T2Sol.poincareFstIso

Documentation

Compare the Poincaré family at a projected point with its base transport.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.NormPoincareBaseChange
attribute [-simp]
  PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app TwoChartCech.Mumford.dK_apply
  TwoChartCech.Mumford.ι0_apply TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply
  TwoChartCech.KerCoprod.ι1_apply TwoChartCech.KerCoprod.ι0_apply
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 _root_.AlgebraicCurve
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace T2Sol
section Classify
open AlgebraicGeometry.RelPicard.BaseTransport
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙
  (Spec (.of R))) c)
  (K : Type u) [CommRing K] [Algebra R K]
  (D : RelativePic0Designation R c) (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
  (h' : RepresentsRelSubPic (SmoothProperCurve.baseChange R c K)
    (SmoothProperCurve.sectionBaseChange K ε)
    (algEquivZeroCut (SmoothProperCurve.baseChange R c K) (SmoothProperCurve.sectionBaseChange K
      ε)) (D.baseChange K))
  (hP : Nonempty (h'.poincare.L ≅ (BaseChange.ofR c ε K
    (h.poincare.pullbackAlong ⟨pullback.fst D.toBase (specMap R K), pullback.condition⟩)).L))
  {T : Scheme.{u}} (t : T ⟶ Spec (.of K))

Lean source · statement

def poincareFstIso (b : SchemeHomOver t (D.baseChange K).toBase) :
    (h.poincare.pullbackAlong (fstPoint c K D t b)).L ≅ (BaseChange.toR c ε K
      (h'.poincare.pullbackAlong b)).L

theorem

toR_mem

L210 ↗

JacobianVarieties.Picard.Proofs.NormPoincareBaseChange.T2Sol.toR_mem

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.NormPoincareBaseChange
attribute [-simp]
  PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app TwoChartCech.Mumford.dK_apply
  TwoChartCech.Mumford.ι0_apply TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply
  TwoChartCech.KerCoprod.ι1_apply TwoChartCech.KerCoprod.ι0_apply
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 _root_.AlgebraicCurve
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace T2Sol
section Classify
open AlgebraicGeometry.RelPicard.BaseTransport
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙
  (Spec (.of R))) c)
  (K : Type u) [CommRing K] [Algebra R K]
  (D : RelativePic0Designation R c) (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
  (h' : RepresentsRelSubPic (SmoothProperCurve.baseChange R c K)
    (SmoothProperCurve.sectionBaseChange K ε)
    (algEquivZeroCut (SmoothProperCurve.baseChange R c K) (SmoothProperCurve.sectionBaseChange K
      ε)) (D.baseChange K))
  (hP : Nonempty (h'.poincare.L ≅ (BaseChange.ofR c ε K
    (h.poincare.pullbackAlong ⟨pullback.fst D.toBase (specMap R K), pullback.condition⟩)).L))
  {T : Scheme.{u}} (t : T ⟶ Spec (.of K))

Lean source · statement

theorem toR_mem
    (M : RigidifiedLineBundle (SmoothProperCurve.baseChange R c K)
      (SmoothProperCurve.sectionBaseChange K ε) t)
    (hM : (algEquivZeroCut (SmoothProperCurve.baseChange R c K)
      (SmoothProperCurve.sectionBaseChange K ε)).P t M) :
    (algEquivZeroCut c ε).P (t ≫ specMap R K) (BaseChange.toR c ε K M)

theorem

fstPoint_classify

L221 ↗

JacobianVarieties.Picard.Proofs.NormPoincareBaseChange.T2Sol.fstPoint_classify

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.NormPoincareBaseChange
attribute [-simp]
  PresheafOfModules.pushforwardCongr_inv_app_app_apply
  PresheafOfModules.pushforwardNatTrans_app_app_apply
  PresheafOfModules.pushforwardCongr_hom_app_app_apply
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app TwoChartCech.Mumford.dK_apply
  TwoChartCech.Mumford.ι0_apply TwoChartCech.Mumford.ι1_apply TwoChartCech.KerCoprod.dK_apply
  TwoChartCech.KerCoprod.ι1_apply TwoChartCech.KerCoprod.ι0_apply
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 _root_.AlgebraicCurve
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
namespace T2Sol
section Classify
open AlgebraicGeometry.RelPicard.BaseTransport
variable {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙
  (Spec (.of R))) c)
  (K : Type u) [CommRing K] [Algebra R K]
  (D : RelativePic0Designation R c) (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
  (h' : RepresentsRelSubPic (SmoothProperCurve.baseChange R c K)
    (SmoothProperCurve.sectionBaseChange K ε)
    (algEquivZeroCut (SmoothProperCurve.baseChange R c K) (SmoothProperCurve.sectionBaseChange K
      ε)) (D.baseChange K))
  (hP : Nonempty (h'.poincare.L ≅ (BaseChange.ofR c ε K
    (h.poincare.pullbackAlong ⟨pullback.fst D.toBase (specMap R K), pullback.condition⟩)).L))
  {T : Scheme.{u}} (t : T ⟶ Spec (.of K))
include hP in

Lean source · statement

theorem fstPoint_classify
    (M : RigidifiedLineBundle (SmoothProperCurve.baseChange R c K)
      (SmoothProperCurve.sectionBaseChange K ε) t)
    (hM : (algEquivZeroCut (SmoothProperCurve.baseChange R c K)
      (SmoothProperCurve.sectionBaseChange K ε)).P t M) :
    fstPoint c K D t (h'.classify t M hM) = h.classify (t ≫ specMap R K) (BaseChange.toR c ε K M)
      (toR_mem c ε K t M hM)

theorem

nonempty_poincare_pullbackAlong_iso_rigidify_normModule_baseChange

L250 ↗

AlgebraicGeometry.RelPicard.RepresentsRelSubPic.nonempty_poincare_pullbackAlong_iso_rigidify_normModule_baseChange

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicGeometry.RelPicard
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open NeronModelInfra GoodReductionJacobian
open AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicCurve
universe u
open _root_.JacobianVarieties.Picard.Proofs in
open NormPoincareBaseChange.T2Sol in
open _root_.AlgebraicGeometry.RelPicard.BaseTransport in

Lean source · statement

theorem RepresentsRelSubPic.nonempty_poincare_pullbackAlong_iso_rigidify_normModule_baseChange
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R)) (ε : SchemeHomOver (𝟙 (Spec
      (.of R))) c)
    (K : Type u) [CommRing K] [Algebra R K] [Mono (specMap R K)]
    (D : RelativePic0Designation R c) (h : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
    (h' : RepresentsRelSubPic (SmoothProperCurve.baseChange R c K)
      (SmoothProperCurve.sectionBaseChange K ε)
      (algEquivZeroCut (SmoothProperCurve.baseChange R c K) (SmoothProperCurve.sectionBaseChange K
        ε)) (D.baseChange K))
    (hP : Nonempty (h'.poincare.L ≅ (BaseChange.ofR c ε K
      (h.poincare.pullbackAlong ⟨pullback.fst D.toBase (specMap R K), pullback.condition⟩)).L))
    {Y : Scheme.{u}} (y : Y ⟶ Spec (.of K))
    (πα πβ : Y ⟶ C) (Hα : πα ≫ c = y ≫ specMap R K) (Hβ : πβ ≫ c = y ≫ specMap R K)
    [IsFinite (pullback.lift πα y Hα : Y ⟶ Limits.pullback c (specMap R K))]
    [Flat (pullback.lift πα y Hα : Y ⟶ Limits.pullback c (specMap R K))]
    [LocallyOfFinitePresentation (pullback.lift πα y Hα : Y ⟶ Limits.pullback c (specMap R K))]
    (d : ℕ) (hd : ∀ z, (pullback.lift πα y Hα : Y ⟶ Limits.pullback c (specMap R K)).finrank z = d)
    (φ₁ : SchemeHomOver D.toBase D.toBase)
    (hmoduli :
      ∀ (T : Scheme.{u}) (t' : T ⟶ Spec (.of K))
          (M : RigidifiedLineBundle c ε (t' ≫ specMap R K))
          (hM : (algEquivZeroCut c ε).P (t' ≫ specMap R K) M),
        Nonempty ((h.poincare.pullbackAlong
            (NeronModelInfra.schemeHomOverComp (h.classify (t' ≫ specMap R K) M hM) φ₁)).L ≅
          Scheme.Modules.rigidify (rigSection c (t' ≫ specMap R K) ε) (pullback.snd c (t' ≫ specMap
            R K))
            (Scheme.Modules.normModule (curveChange (c' := y ≫ specMap R K) πα Hα (t' ≫ specMap R
              K)) d
              ((Scheme.Modules.pullback (curveChange (c' := y ≫ specMap R K) πβ Hβ (t' ≫ specMap R
                K))).obj M.L))))
    (φ₁K : SchemeHomOver (D.baseChange K).toBase (D.baseChange K).toBase)
    (hφ₁K : φ₁K.1 ≫ pullback.fst D.toBase (specMap R K) = pullback.fst D.toBase (specMap R K) ≫
      φ₁.1)
    (Hα₁ : pullback.lift πα y Hα ≫ SmoothProperCurve.baseChange R c K = y)
    (Hβ₁ : pullback.lift πβ y Hβ ≫ SmoothProperCurve.baseChange R c K = y)
    (T : Scheme.{u}) (t : T ⟶ Spec (.of K))
    (M : RigidifiedLineBundle (SmoothProperCurve.baseChange R c K)
      (SmoothProperCurve.sectionBaseChange K ε) t)
    (hM : (algEquivZeroCut (SmoothProperCurve.baseChange R c K)
      (SmoothProperCurve.sectionBaseChange K ε)).P t M) :
    Nonempty ((h'.poincare.pullbackAlong (NeronModelInfra.schemeHomOverComp (h'.classify t M hM)
      φ₁K)).L ≅
      Scheme.Modules.rigidify
        (rigSection (SmoothProperCurve.baseChange R c K) t (SmoothProperCurve.sectionBaseChange K
          ε))
        (pullback.snd (SmoothProperCurve.baseChange R c K) t)
        (Scheme.Modules.normModule (curveChange (c' := y) (pullback.lift πα y Hα) Hα₁ t) d
          ((Scheme.Modules.pullback (curveChange (c' := y) (pullback.lift πβ y Hβ) Hβ₁ t)).obj
            M.L)))

Module documentation

Base change of the norm Poincaré comparison

Declarations