NYLL
Module

baseChangeSnd_comp_restrictHom_eq_of_baseChangeSnd_comp.lean

Nyll.JacobianVarieties.Picard.baseChangeSnd_comp_restrictHom_eq_of_baseChangeSnd_comp
45 declarations indexed from sourceView source ↗

Module documentation

Restriction maps on Picard points commute with a compatible base change. The proof compares the pulled-back Poincare bundles using explicit pullback isomorphisms.

Imports13
Imported by1

Declarations

theorem

rigSection_fst''

L58 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.rigSection_fst''
Documentation

The first projection of the rigidifying section.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Basic
Lean source · statement
theorem rigSection_fst'' {C T : Scheme.{u}} (cc : C ⟶ Spec (CommRingCat.of κ))
    (t : T ⟶ Spec (CommRingCat.of κ))
    (e : SchemeHomOver (𝟙 (Spec (CommRingCat.of κ))) cc) : rigSection cc t e ≫ pullback.fst cc t =
      t ≫ e.1
theorem

rigSection_snd''

L65 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.rigSection_snd''
Documentation

The second projection of the rigidifying section.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Basic
Lean source · statement
theorem rigSection_snd'' {C T : Scheme.{u}} (cc : C ⟶ Spec (CommRingCat.of κ))
    (t : T ⟶ Spec (CommRingCat.of κ))
    (e : SchemeHomOver (𝟙 (Spec (CommRingCat.of κ))) cc) : rigSection cc t e ≫ pullback.snd cc t =
      𝟙 T
theorem

baseChangeSnd_fst''

L72 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.baseChangeSnd_fst''
Documentation

Changing the base leaves the first pullback projection unchanged.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Basic
Lean source · statement
theorem baseChangeSnd_fst'' {S : Type u} [CommRing S] {C T T' : Scheme.{u}}
    (cc : C ⟶ Spec (CommRingCat.of S))
    {t : T ⟶ Spec (CommRingCat.of S)} {t' : T' ⟶ Spec (CommRingCat.of S)}
    (ψ : SchemeHomOver t' t) : baseChangeSnd cc ψ ≫ pullback.fst cc t = pullback.fst cc t'
theorem

baseChangeSnd_snd''

L79 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.baseChangeSnd_snd''
Documentation

The second projection after a change of base.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Basic
Lean source · statement
theorem baseChangeSnd_snd'' {S : Type u} [CommRing S] {C T T' : Scheme.{u}}
    (cc : C ⟶ Spec (CommRingCat.of S))
    {t : T ⟶ Spec (CommRingCat.of S)} {t' : T' ⟶ Spec (CommRingCat.of S)}
    (ψ : SchemeHomOver t' t) : baseChangeSnd cc ψ ≫ pullback.snd cc t = pullback.snd cc t' ≫ ψ.1
theorem

sectionBaseChange_fst''

L86 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.sectionBaseChange_fst''
Documentation

The first projection of the base-changed section.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Basic
Lean source · statement
theorem sectionBaseChange_fst'' {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
    (e : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) :
    (sectionBaseChange κ e).1 ≫ pullback.fst c 𝔰 = 𝔰 ≫ e.1
theorem

sectionBaseChange_snd''

L92 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.sectionBaseChange_snd''
Documentation

The second projection of the base-changed section.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Basic
Lean source · statement
theorem sectionBaseChange_snd'' {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
    (e : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) :
    (sectionBaseChange κ e).1 ≫ pullback.snd c 𝔰 = 𝟙 _
theorem

curveChange_fst''

L98 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.curveChange_fst''
Documentation

The first projection after changing the curve.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Basic
Lean source · statement
theorem curveChange_fst'' {S : Type u} [CommRing S] {C C' T : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of S)}
    {c' : C' ⟶ Spec (CommRingCat.of S)} (f : C' ⟶ C) (hf : f ≫ c = c')
    (t : T ⟶ Spec (CommRingCat.of S)) : curveChange f hf t ≫ pullback.fst c t = pullback.fst c' t ≫
      f
theorem

curveChange_snd''

L106 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.curveChange_snd''
Documentation

Changing the curve preserves the second projection.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Basic
Lean source · statement
theorem curveChange_snd'' {S : Type u} [CommRing S] {C C' T : Scheme.{u}}
    {c : C ⟶ Spec (CommRingCat.of S)}
    {c' : C' ⟶ Spec (CommRingCat.of S)} (f : C' ⟶ C) (hf : f ≫ c = c')
    (t : T ⟶ Spec (CommRingCat.of S)) : curveChange f hf t ≫ pullback.snd c t = pullback.snd c' t
def

flatPt

L120 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.flatPt
Documentation

Replace the base coordinate of a point while keeping its curve coordinate.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Points
variable {Y : Scheme.{u}} (y : Y ⟶ Spec (CommRingCat.of R)) (τ : SchemeHomOver (specMap R κ)
  (specMap R κ))
Lean source · statement
def flatPt {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ)) (b : T ⟶ pullback y 𝔰)
    (hb : b ≫ pullback.snd y 𝔰 = t ≫ τ.1) : SchemeHomOver t (pullback.snd y 𝔰)
theorem

flatPt_coe_fst

L127 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.flatPt_coe_fst
Documentation

The flattened point has the original first coordinate.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Points
variable {Y : Scheme.{u}} (y : Y ⟶ Spec (CommRingCat.of R)) (τ : SchemeHomOver (specMap R κ)
  (specMap R κ))
Lean source · statement
theorem flatPt_coe_fst {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ))
    (b : T ⟶ pullback y 𝔰)
    (hb : b ≫ pullback.snd y 𝔰 = t ≫ τ.1) : (flatPt y τ t b hb).1 ≫ pullback.fst y 𝔰 = b ≫
      pullback.fst y 𝔰
theorem

flatPt_coe_snd

L134 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.flatPt_coe_snd
Documentation

The flattened point lies over the specified base map.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Points
variable {Y : Scheme.{u}} (y : Y ⟶ Spec (CommRingCat.of R)) (τ : SchemeHomOver (specMap R κ)
  (specMap R κ))
Lean source · statement
theorem flatPt_coe_snd {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ))
    (b : T ⟶ pullback y 𝔰)
    (hb : b ≫ pullback.snd y 𝔰 = t ≫ τ.1) : (flatPt y τ t b hb).1 ≫ pullback.snd y 𝔰 = t
theorem

flatPt_comp_baseChangeSnd

L140 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.flatPt_comp_baseChangeSnd
Documentation

Changing the base of the flattened point recovers the original map.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Points
variable {Y : Scheme.{u}} (y : Y ⟶ Spec (CommRingCat.of R)) (τ : SchemeHomOver (specMap R κ)
  (specMap R κ))
Lean source · statement
theorem flatPt_comp_baseChangeSnd {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ))
    (b : T ⟶ pullback y 𝔰)
    (hb : b ≫ pullback.snd y 𝔰 = t ≫ τ.1) : (flatPt y τ t b hb).1 ≫ baseChangeSnd y τ = b
def

twistPt

L148 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.twistPt
Documentation

Change the base coordinate of a point by the specified endomorphism.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Points
variable {Y : Scheme.{u}} (y : Y ⟶ Spec (CommRingCat.of R)) (τ : SchemeHomOver (specMap R κ)
  (specMap R κ))
Lean source · statement
def twistPt {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of κ)}
    (a : SchemeHomOver t (pullback.snd y 𝔰)) :
    SchemeHomOver (t ≫ τ.1) (pullback.snd y 𝔰)
theorem

twistPt_coe

L154 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.twistPt_coe
Documentation

The underlying map of a twisted point.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Points
variable {Y : Scheme.{u}} (y : Y ⟶ Spec (CommRingCat.of R)) (τ : SchemeHomOver (specMap R κ)
  (specMap R κ))
Lean source · statement
theorem twistPt_coe {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of κ)}
    (a : SchemeHomOver t (pullback.snd y 𝔰)) :
    (twistPt y τ a).1 = a.1 ≫ baseChangeSnd y τ
theorem

twistPt_coe_fst

L159 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.twistPt_coe_fst
Documentation

Twisting preserves the first coordinate.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Points
variable {Y : Scheme.{u}} (y : Y ⟶ Spec (CommRingCat.of R)) (τ : SchemeHomOver (specMap R κ)
  (specMap R κ))
Lean source · statement
theorem twistPt_coe_fst {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of κ)}
    (a : SchemeHomOver t (pullback.snd y 𝔰)) :
    (twistPt y τ a).1 ≫ pullback.fst y 𝔰 = a.1 ≫ pullback.fst y 𝔰
def

piHom

L173 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.piHom
Documentation

Compare the two iterated pullbacks after twisting the base coordinate.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Pi
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (τ : SchemeHomOver (specMap R κ)
  (specMap R κ))
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ))
Lean source · statement
def piHom : pullback (baseChange R c κ) (t ≫ τ.1) ⟶ pullback (baseChange R c κ) t
def

piInv

L180 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.piInv
Documentation

The inverse comparison between the iterated pullbacks.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Pi
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (τ : SchemeHomOver (specMap R κ)
  (specMap R κ))
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ))
Lean source · statement
def piInv : pullback (baseChange R c κ) t ⟶ pullback (baseChange R c κ) (t ≫ τ.1)
theorem

piHom_snd

L187 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.piHom_snd
Documentation

The comparison preserves the outer second projection.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Pi
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (τ : SchemeHomOver (specMap R κ)
  (specMap R κ))
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ))
Lean source · statement
theorem piHom_snd : piHom c τ t ≫ pullback.snd _ _ = pullback.snd _ _
theorem

piInv_snd

L190 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.piInv_snd
Documentation

The inverse comparison preserves the outer second projection.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Pi
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (τ : SchemeHomOver (specMap R κ)
  (specMap R κ))
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ))
Lean source · statement
theorem piInv_snd : piInv c τ t ≫ pullback.snd _ _ = pullback.snd _ _
theorem

piHom_fst_fst

L193 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.piHom_fst_fst
Documentation

The comparison preserves the inner first projection.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Pi
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (τ : SchemeHomOver (specMap R κ)
  (specMap R κ))
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ))
Lean source · statement
theorem piHom_fst_fst :
    piHom c τ t ≫ pullback.fst _ _ ≫ pullback.fst c 𝔰 = pullback.fst _ _ ≫ pullback.fst c 𝔰
theorem

piInv_fst_fst

L197 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.piInv_fst_fst
Documentation

The inverse comparison preserves the inner first projection.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Pi
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (τ : SchemeHomOver (specMap R κ)
  (specMap R κ))
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ))
Lean source · statement
theorem piInv_fst_fst :
    piInv c τ t ≫ pullback.fst _ _ ≫ pullback.fst c 𝔰 = pullback.fst _ _ ≫ pullback.fst c 𝔰
theorem

piHom_fst_snd

L201 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.piHom_fst_snd
Documentation

The inner base coordinate after the comparison.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Pi
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (τ : SchemeHomOver (specMap R κ)
  (specMap R κ))
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ))
Lean source · statement
theorem piHom_fst_snd :
    piHom c τ t ≫ pullback.fst _ _ ≫ pullback.snd c 𝔰 = pullback.snd _ _ ≫ t
theorem

piInv_fst_snd

L205 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.piInv_fst_snd
Documentation

The inner base coordinate after the inverse comparison.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Pi
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (τ : SchemeHomOver (specMap R κ)
  (specMap R κ))
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ))
Lean source · statement
theorem piInv_fst_snd :
    piInv c τ t ≫ pullback.fst _ _ ≫ pullback.snd c 𝔰 = pullback.snd _ _ ≫ t ≫ τ.1
def

piIso

L210 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.piIso
Documentation

The isomorphism between the two iterated pullbacks.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Pi
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (τ : SchemeHomOver (specMap R κ)
  (specMap R κ))
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ))
Lean source · full declaration
def piIso : pullback (baseChange R c κ) (t ≫ τ.1) ≅ pullback (baseChange R c κ) t where
  hom := piHom c τ t
  inv := piInv c τ t
  hom_inv_id := by
    apply pullback.hom_ext
    · apply pullback.hom_ext
      · simp only [Category.assoc, Category.id_comp, piInv_fst_fst, piHom_fst_fst]
      · simp only [Category.assoc, Category.id_comp, piInv_fst_snd, piHom_snd_assoc]
        exact pullback.condition.symm
    · simp only [Category.assoc, piInv_snd, piHom_snd, Category.id_comp]
  inv_hom_id := by
    apply pullback.hom_ext
    · apply pullback.hom_ext
      · simp only [Category.assoc, Category.id_comp, piHom_fst_fst, piInv_fst_fst]
      · simp only [Category.assoc, Category.id_comp, piHom_fst_snd, piInv_snd_assoc]
        exact pullback.condition.symm
    · simp only [Category.assoc, piHom_snd, piInv_snd, Category.id_comp]
theorem

piIso_hom

L229 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.piIso_hom
Documentation

The forward map of the iterated pullback isomorphism.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Pi
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (τ : SchemeHomOver (specMap R κ)
  (specMap R κ))
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ))
Lean source · statement
theorem piIso_hom : (piIso c τ t).hom = piHom c τ t
theorem

piIso_inv

L231 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.piIso_inv
Documentation

The inverse map of the iterated pullback isomorphism.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Pi
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (τ : SchemeHomOver (specMap R κ)
  (specMap R κ))
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ))
Lean source · statement
theorem piIso_inv : (piIso c τ t).inv = piInv c τ t
theorem

rigSection_piHom

L234 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.rigSection_piHom
Documentation

The iterated pullback comparison respects the rigidifying section.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Pi
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (τ : SchemeHomOver (specMap R κ)
  (specMap R κ))
  {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ))
Lean source · statement
theorem rigSection_piHom (e : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) :
    rigSection (baseChange R c κ) (t ≫ τ.1) (sectionBaseChange κ e) ≫ piHom c τ t =
      rigSection (baseChange R c κ) t (sectionBaseChange κ e)
def

objIso

L250 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.objIso
Documentation

Compare an iterated module pullback with pullback along the composite.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Transport
Lean source · statement
def objIso {P Q S : Scheme.{u}} (A : P ⟶ Q) (B : Q ⟶ S) (C : P ⟶ S) (h : A ≫ B = C) (L : S.Modules)
    :
    (Scheme.Modules.pullback A).obj ((Scheme.Modules.pullback B).obj L) ≅ (Scheme.Modules.pullback
      C).obj L
def

invHomIso

L257 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.invHomIso
Documentation

Cancel pullback along an isomorphism and its inverse.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Transport
Lean source · statement
def invHomIso {P Q : Scheme.{u}} (e : P ≅ Q) (N : Q.Modules) :
    (Scheme.Modules.pullback e.inv).obj ((Scheme.Modules.pullback e.hom).obj N) ≅ N
def

squareIso

L262 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.squareIso
Documentation

Compare module pullbacks around a commutative square.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Transport
Lean source · statement
def squareIso {P Q P' Q' : Scheme.{u}} (A : P ⟶ Q) (B : Q ⟶ Q') (A' : P ⟶ P') (B' : P' ⟶ Q')
    (h : A ≫ B = A' ≫ B')
    (L : Q'.Modules) :
    (Scheme.Modules.pullback A).obj ((Scheme.Modules.pullback B).obj L) ≅
      (Scheme.Modules.pullback A').obj ((Scheme.Modules.pullback B').obj L)
def

rigidifyTransport

L270 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.rigidifyTransport
Documentation

Transport rigidification through an isomorphism preserving the section and base.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Transport
Lean source · statement
def rigidifyTransport {P₁ P₂ T : Scheme.{u}} (e : P₁ ≅ P₂) (σ₁ : T ⟶ P₁) (σ₂ : T ⟶ P₂)
    (hσ : σ₁ ≫ e.hom = σ₂)
    (q₁ : P₁ ⟶ T) (q₂ : P₂ ⟶ T) (hq : e.hom ≫ q₂ = q₁) (N : P₂.Modules) :
    (Scheme.Modules.pullback e.inv).obj (Scheme.Modules.rigidify σ₁ q₁ ((Scheme.Modules.pullback
      e.hom).obj N)) ≅
      Scheme.Modules.rigidify σ₂ q₂ N
def

qMap

L295 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.qMap
Documentation

Map an iterated base change to the original universal family.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Poincare
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)} {e : SchemeHomOver (𝟙 (Spec
  (CommRingCat.of R))) c}
  {G : RelativePic0Designation R c} (hGR : RepresentsRelSubPic c e (algEquivZeroCut c e) G)
  (hG : RepresentsRelSubPic (baseChange R c κ) (sectionBaseChange κ e)
    (algEquivZeroCut (baseChange R c κ) (sectionBaseChange κ e)) (G.baseChange κ))
  (hPG : Nonempty (hG.poincare.L ≅ (BaseChange.ofR c e κ
    (hGR.poincare.pullbackAlong ⟨pullback.fst G.toBase (specMap R κ), pullback.condition⟩)).L))
  (τ : SchemeHomOver (specMap R κ) (specMap R κ))
Lean source · statement
def qMap {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of κ)}
    (p : SchemeHomOver t (G.baseChange κ).toBase) :
    pullback (baseChange R c κ) t ⟶ pullback c G.toBase
theorem

qMap_fst

L303 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.qMap_fst
Documentation

The curve coordinate of the map to the universal family.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Poincare
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)} {e : SchemeHomOver (𝟙 (Spec
  (CommRingCat.of R))) c}
  {G : RelativePic0Designation R c} (hGR : RepresentsRelSubPic c e (algEquivZeroCut c e) G)
  (hG : RepresentsRelSubPic (baseChange R c κ) (sectionBaseChange κ e)
    (algEquivZeroCut (baseChange R c κ) (sectionBaseChange κ e)) (G.baseChange κ))
  (hPG : Nonempty (hG.poincare.L ≅ (BaseChange.ofR c e κ
    (hGR.poincare.pullbackAlong ⟨pullback.fst G.toBase (specMap R κ), pullback.condition⟩)).L))
  (τ : SchemeHomOver (specMap R κ) (specMap R κ))
Lean source · statement
theorem qMap_fst {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of κ)}
    (p : SchemeHomOver t (G.baseChange κ).toBase) :
    qMap p ≫ pullback.fst c G.toBase = pullback.fst _ _ ≫ pullback.fst c 𝔰
theorem

qMap_snd

L310 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.qMap_snd
Documentation

The parameter coordinate of the map to the universal family.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Poincare
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)} {e : SchemeHomOver (𝟙 (Spec
  (CommRingCat.of R))) c}
  {G : RelativePic0Designation R c} (hGR : RepresentsRelSubPic c e (algEquivZeroCut c e) G)
  (hG : RepresentsRelSubPic (baseChange R c κ) (sectionBaseChange κ e)
    (algEquivZeroCut (baseChange R c κ) (sectionBaseChange κ e)) (G.baseChange κ))
  (hPG : Nonempty (hG.poincare.L ≅ (BaseChange.ofR c e κ
    (hGR.poincare.pullbackAlong ⟨pullback.fst G.toBase (specMap R κ), pullback.condition⟩)).L))
  (τ : SchemeHomOver (specMap R κ) (specMap R κ))
Lean source · statement
theorem qMap_snd {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of κ)}
    (p : SchemeHomOver t (G.baseChange κ).toBase) :
    qMap p ≫ pullback.snd c G.toBase = pullback.snd _ _ ≫ p.1 ≫ pullback.fst G.toBase 𝔰
theorem

nonempty_poincare_pullbackAlong_iso

L319 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.nonempty_poincare_pullbackAlong_iso
Documentation

Compare the base-changed Poincare bundle with its original pullback.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Poincare
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)} {e : SchemeHomOver (𝟙 (Spec
  (CommRingCat.of R))) c}
  {G : RelativePic0Designation R c} (hGR : RepresentsRelSubPic c e (algEquivZeroCut c e) G)
  (hG : RepresentsRelSubPic (baseChange R c κ) (sectionBaseChange κ e)
    (algEquivZeroCut (baseChange R c κ) (sectionBaseChange κ e)) (G.baseChange κ))
  (hPG : Nonempty (hG.poincare.L ≅ (BaseChange.ofR c e κ
    (hGR.poincare.pullbackAlong ⟨pullback.fst G.toBase (specMap R κ), pullback.condition⟩)).L))
  (τ : SchemeHomOver (specMap R κ) (specMap R κ))
include hPG in
Lean source · statement
theorem nonempty_poincare_pullbackAlong_iso {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of κ)}
    (p : SchemeHomOver t (G.baseChange κ).toBase) :
    Nonempty ((hG.poincare.pullbackAlong p).L ≅ (Scheme.Modules.pullback (qMap p)).obj
      hGR.poincare.L)
theorem

nonempty_poincare_pullbackAlong_iso_of_fst_eq

L328 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.nonempty_poincare_pullbackAlong_iso_of_fst_eq
Documentation

Compare Poincare bundles at points with the same original coordinate.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Poincare
variable {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)} {e : SchemeHomOver (𝟙 (Spec
  (CommRingCat.of R))) c}
  {G : RelativePic0Designation R c} (hGR : RepresentsRelSubPic c e (algEquivZeroCut c e) G)
  (hG : RepresentsRelSubPic (baseChange R c κ) (sectionBaseChange κ e)
    (algEquivZeroCut (baseChange R c κ) (sectionBaseChange κ e)) (G.baseChange κ))
  (hPG : Nonempty (hG.poincare.L ≅ (BaseChange.ofR c e κ
    (hGR.poincare.pullbackAlong ⟨pullback.fst G.toBase (specMap R κ), pullback.condition⟩)).L))
  (τ : SchemeHomOver (specMap R κ) (specMap R κ))
include hPG in
Lean source · statement
theorem nonempty_poincare_pullbackAlong_iso_of_fst_eq {T : Scheme.{u}}
    {t : T ⟶ Spec (CommRingCat.of κ)}
    (p : SchemeHomOver (t ≫ τ.1) (G.baseChange κ).toBase) (q : SchemeHomOver t (G.baseChange
      κ).toBase)
    (hpq : p.1 ≫ pullback.fst G.toBase 𝔰 = q.1 ≫ pullback.fst G.toBase 𝔰) :
    Nonempty ((hG.poincare.pullbackAlong p).L ≅
      (Scheme.Modules.pullback (piHom c τ t)).obj (hG.poincare.pullbackAlong q).L)
theorem

piHom_fst_baseChangeSnd

L354 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.piHom_fst_baseChangeSnd
Documentation

The iterated pullback comparison cancels the change of base.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Curves
variable {𝔛 𝔛₀ : Scheme.{u}} {x : 𝔛 ⟶ Spec (CommRingCat.of R)} {x₀ : 𝔛₀ ⟶ Spec (CommRingCat.of R)}
  (f : pullback x₀ (specMap R κ) ⟶ pullback x (specMap R κ)) (hf : f ≫ baseChange R x κ =
    baseChange R x₀ κ)
  (τ : SchemeHomOver (specMap R κ) (specMap R κ))
  (hcomm : baseChangeSnd x₀ τ ≫ f = f ≫ baseChangeSnd x τ)
Lean source · statement
theorem piHom_fst_baseChangeSnd {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) {T : Scheme.{u}}
    (t : T ⟶ Spec (CommRingCat.of κ)) :
    piHom c τ t ≫ pullback.fst _ _ ≫ baseChangeSnd c τ = pullback.fst _ _
theorem

baseChangeSnd_f_fst

L364 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.baseChangeSnd_f_fst
Documentation

A compatible curve map preserves its first coordinate under base change.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Curves
variable {𝔛 𝔛₀ : Scheme.{u}} {x : 𝔛 ⟶ Spec (CommRingCat.of R)} {x₀ : 𝔛₀ ⟶ Spec (CommRingCat.of R)}
  (f : pullback x₀ (specMap R κ) ⟶ pullback x (specMap R κ)) (hf : f ≫ baseChange R x κ =
    baseChange R x₀ κ)
  (τ : SchemeHomOver (specMap R κ) (specMap R κ))
  (hcomm : baseChangeSnd x₀ τ ≫ f = f ≫ baseChangeSnd x τ)
include hcomm in
Lean source · statement
theorem baseChangeSnd_f_fst : baseChangeSnd x₀ τ ≫ f ≫ pullback.fst x 𝔰 = f ≫ pullback.fst x 𝔰
theorem

curveChange_piHom

L369 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.curveChange_piHom
Documentation

Changing the curve commutes with the iterated pullback comparison.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Curves
variable {𝔛 𝔛₀ : Scheme.{u}} {x : 𝔛 ⟶ Spec (CommRingCat.of R)} {x₀ : 𝔛₀ ⟶ Spec (CommRingCat.of R)}
  (f : pullback x₀ (specMap R κ) ⟶ pullback x (specMap R κ)) (hf : f ≫ baseChange R x κ =
    baseChange R x₀ κ)
  (τ : SchemeHomOver (specMap R κ) (specMap R κ))
  (hcomm : baseChangeSnd x₀ τ ≫ f = f ≫ baseChangeSnd x τ)
include hcomm in
Lean source · statement
theorem curveChange_piHom {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ)) :
    curveChange f hf (t ≫ τ.1) ≫ piHom x τ t = piHom x₀ τ t ≫ curveChange f hf t
theorem

nonempty_curveChange_piHom_iso

L386 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.nonempty_curveChange_piHom_iso
Documentation

The commuting comparison square gives an isomorphism of module pullbacks.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Curves
variable {𝔛 𝔛₀ : Scheme.{u}} {x : 𝔛 ⟶ Spec (CommRingCat.of R)} {x₀ : 𝔛₀ ⟶ Spec (CommRingCat.of R)}
  (f : pullback x₀ (specMap R κ) ⟶ pullback x (specMap R κ)) (hf : f ≫ baseChange R x κ =
    baseChange R x₀ κ)
  (τ : SchemeHomOver (specMap R κ) (specMap R κ))
  (hcomm : baseChangeSnd x₀ τ ≫ f = f ≫ baseChangeSnd x τ)
include hcomm in
Lean source · statement
theorem nonempty_curveChange_piHom_iso {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ))
    (M : (pullback (baseChange R x κ) t).Modules) :
    Nonempty ((Scheme.Modules.pullback (curveChange f hf (t ≫ τ.1))).obj ((Scheme.Modules.pullback
      (piHom x τ t)).obj M) ≅
      (Scheme.Modules.pullback (piHom x₀ τ t)).obj ((Scheme.Modules.pullback (curveChange f hf
        t)).obj M))
theorem

twist_comp_snd

L425 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.twist_comp_snd
Documentation

The composite from a twisted point has the twisted base coordinate.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Core
variable {𝔛 𝔛₀ : Scheme.{u}} {x : 𝔛 ⟶ Spec (CommRingCat.of R)} {x₀ : 𝔛₀ ⟶ Spec (CommRingCat.of R)}
  {εR : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) x} {ε₀R : SchemeHomOver (𝟙 (Spec
    (CommRingCat.of R))) x₀}
  {D_R : RelativePic0Designation R x} {D₀ : RelativePic0Designation R x₀}
  (hD_R : RepresentsRelSubPic x εR (algEquivZeroCut x εR) D_R)
  (hD₀ : RepresentsRelSubPic x₀ ε₀R (algEquivZeroCut x₀ ε₀R) D₀)
  (hD : RepresentsRelSubPic (baseChange R x κ) (sectionBaseChange κ εR)
    (algEquivZeroCut (baseChange R x κ) (sectionBaseChange κ εR)) (D_R.baseChange κ))
  (hPD : Nonempty (hD.poincare.L ≅ (BaseChange.ofR x εR κ
    (hD_R.poincare.pullbackAlong ⟨pullback.fst D_R.toBase (specMap R κ), pullback.condition⟩)).L))
  (hD' : RepresentsRelSubPic (baseChange R x₀ κ) (sectionBaseChange κ ε₀R)
    (algEquivZeroCut (baseChange R x₀ κ) (sectionBaseChange κ ε₀R)) (D₀.baseChange κ))
  (hPD' : Nonempty (hD'.poincare.L ≅ (BaseChange.ofR x₀ ε₀R κ
    (hD₀.poincare.pullbackAlong ⟨pullback.fst D₀.toBase (specMap R κ), pullback.condition⟩)).L))
  (f : pullback x₀ (specMap R κ) ⟶ pullback x (specMap R κ)) (hf : f ≫ baseChange R x κ =
    baseChange R x₀ κ)
  (τ : SchemeHomOver (specMap R κ) (specMap R κ))
  (hcomm : baseChangeSnd x₀ τ ≫ f = f ≫ baseChangeSnd x τ)
  (ν : SchemeHomOver (D_R.baseChange κ).toBase (D₀.baseChange κ).toBase)
  (hν : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ)) (a : SchemeHomOver t (D_R.baseChange
    κ).toBase),
    Nonempty ((hD'.poincare.pullbackAlong (NeronModelInfra.schemeHomOverComp a ν)).L ≅
      Scheme.Modules.rigidify (rigSection (baseChange R x₀ κ) t (sectionBaseChange κ ε₀R))
        (pullback.snd (baseChange R x₀ κ) t)
        ((Scheme.Modules.pullback (curveChange f hf t)).obj (hD.poincare.pullbackAlong a).L)))
Lean source · statement
theorem twist_comp_snd {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of κ)}
    (a : SchemeHomOver t (D_R.baseChange κ).toBase) :
    ((twistPt D_R.toBase τ a).1 ≫ ν.1) ≫ pullback.snd D₀.toBase 𝔰 = t ≫ τ.1
theorem

flatPt_twist_eq

L433 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.flatPt_twist_eq
Documentation

Poincare classification identifies the flattened twisted image with the original image.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Core
variable {𝔛 𝔛₀ : Scheme.{u}} {x : 𝔛 ⟶ Spec (CommRingCat.of R)} {x₀ : 𝔛₀ ⟶ Spec (CommRingCat.of R)}
  {εR : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) x} {ε₀R : SchemeHomOver (𝟙 (Spec
    (CommRingCat.of R))) x₀}
  {D_R : RelativePic0Designation R x} {D₀ : RelativePic0Designation R x₀}
  (hD_R : RepresentsRelSubPic x εR (algEquivZeroCut x εR) D_R)
  (hD₀ : RepresentsRelSubPic x₀ ε₀R (algEquivZeroCut x₀ ε₀R) D₀)
  (hD : RepresentsRelSubPic (baseChange R x κ) (sectionBaseChange κ εR)
    (algEquivZeroCut (baseChange R x κ) (sectionBaseChange κ εR)) (D_R.baseChange κ))
  (hPD : Nonempty (hD.poincare.L ≅ (BaseChange.ofR x εR κ
    (hD_R.poincare.pullbackAlong ⟨pullback.fst D_R.toBase (specMap R κ), pullback.condition⟩)).L))
  (hD' : RepresentsRelSubPic (baseChange R x₀ κ) (sectionBaseChange κ ε₀R)
    (algEquivZeroCut (baseChange R x₀ κ) (sectionBaseChange κ ε₀R)) (D₀.baseChange κ))
  (hPD' : Nonempty (hD'.poincare.L ≅ (BaseChange.ofR x₀ ε₀R κ
    (hD₀.poincare.pullbackAlong ⟨pullback.fst D₀.toBase (specMap R κ), pullback.condition⟩)).L))
  (f : pullback x₀ (specMap R κ) ⟶ pullback x (specMap R κ)) (hf : f ≫ baseChange R x κ =
    baseChange R x₀ κ)
  (τ : SchemeHomOver (specMap R κ) (specMap R κ))
  (hcomm : baseChangeSnd x₀ τ ≫ f = f ≫ baseChangeSnd x τ)
  (ν : SchemeHomOver (D_R.baseChange κ).toBase (D₀.baseChange κ).toBase)
  (hν : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ)) (a : SchemeHomOver t (D_R.baseChange
    κ).toBase),
    Nonempty ((hD'.poincare.pullbackAlong (NeronModelInfra.schemeHomOverComp a ν)).L ≅
      Scheme.Modules.rigidify (rigSection (baseChange R x₀ κ) t (sectionBaseChange κ ε₀R))
        (pullback.snd (baseChange R x₀ κ) t)
        ((Scheme.Modules.pullback (curveChange f hf t)).obj (hD.poincare.pullbackAlong a).L)))
include hD_R hD₀ hPD hPD' hcomm hν in
Lean source · statement
theorem flatPt_twist_eq {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of κ)}
    (a : SchemeHomOver t (D_R.baseChange κ).toBase) :
    flatPt D₀.toBase τ t ((twistPt D_R.toBase τ a).1 ≫ ν.1) (twist_comp_snd τ ν a) =
      NeronModelInfra.schemeHomOverComp a ν
theorem

comm_of_characterisation

L459 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.comm_of_characterisation
Documentation

A map characterized by Poincare pullback commutes with the base endomorphism.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Core
variable {𝔛 𝔛₀ : Scheme.{u}} {x : 𝔛 ⟶ Spec (CommRingCat.of R)} {x₀ : 𝔛₀ ⟶ Spec (CommRingCat.of R)}
  {εR : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) x} {ε₀R : SchemeHomOver (𝟙 (Spec
    (CommRingCat.of R))) x₀}
  {D_R : RelativePic0Designation R x} {D₀ : RelativePic0Designation R x₀}
  (hD_R : RepresentsRelSubPic x εR (algEquivZeroCut x εR) D_R)
  (hD₀ : RepresentsRelSubPic x₀ ε₀R (algEquivZeroCut x₀ ε₀R) D₀)
  (hD : RepresentsRelSubPic (baseChange R x κ) (sectionBaseChange κ εR)
    (algEquivZeroCut (baseChange R x κ) (sectionBaseChange κ εR)) (D_R.baseChange κ))
  (hPD : Nonempty (hD.poincare.L ≅ (BaseChange.ofR x εR κ
    (hD_R.poincare.pullbackAlong ⟨pullback.fst D_R.toBase (specMap R κ), pullback.condition⟩)).L))
  (hD' : RepresentsRelSubPic (baseChange R x₀ κ) (sectionBaseChange κ ε₀R)
    (algEquivZeroCut (baseChange R x₀ κ) (sectionBaseChange κ ε₀R)) (D₀.baseChange κ))
  (hPD' : Nonempty (hD'.poincare.L ≅ (BaseChange.ofR x₀ ε₀R κ
    (hD₀.poincare.pullbackAlong ⟨pullback.fst D₀.toBase (specMap R κ), pullback.condition⟩)).L))
  (f : pullback x₀ (specMap R κ) ⟶ pullback x (specMap R κ)) (hf : f ≫ baseChange R x κ =
    baseChange R x₀ κ)
  (τ : SchemeHomOver (specMap R κ) (specMap R κ))
  (hcomm : baseChangeSnd x₀ τ ≫ f = f ≫ baseChangeSnd x τ)
  (ν : SchemeHomOver (D_R.baseChange κ).toBase (D₀.baseChange κ).toBase)
  (hν : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ)) (a : SchemeHomOver t (D_R.baseChange
    κ).toBase),
    Nonempty ((hD'.poincare.pullbackAlong (NeronModelInfra.schemeHomOverComp a ν)).L ≅
      Scheme.Modules.rigidify (rigSection (baseChange R x₀ κ) t (sectionBaseChange κ ε₀R))
        (pullback.snd (baseChange R x₀ κ) t)
        ((Scheme.Modules.pullback (curveChange f hf t)).obj (hD.poincare.pullbackAlong a).L)))
include hD_R hD₀ hPD hPD' hcomm hν in
Lean source · statement
theorem comm_of_characterisation :
    baseChangeSnd D_R.toBase τ ≫ ν.1 = ν.1 ≫ baseChangeSnd D₀.toBase τ
theorem

characterisation_pullbackHom

L486 ↗
JacobianVarieties.Picard.Proofs.RestrictedBaseChange.TwistNatAux.characterisation_pullbackHom
Documentation

The Picard pullback map is characterized by rigidified curve pullback.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
noncomputable section
namespace TwistNatAux
variable {R : Type u} [CommRing R] {κ : Type u} [CommRing κ] [Algebra R κ]
local notation "𝔰" => specMap R κ
section Clause1
variable {𝔛 𝔛₀ : Scheme.{u}} {x : 𝔛 ⟶ Spec (CommRingCat.of R)} {x₀ : 𝔛₀ ⟶ Spec (CommRingCat.of R)}
  {εR : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) x} {ε₀R : SchemeHomOver (𝟙 (Spec
    (CommRingCat.of R))) x₀}
  {D_R : RelativePic0Designation R x} {D₀ : RelativePic0Designation R x₀}
  (hD : RepresentsRelSubPic (baseChange R x κ) (sectionBaseChange κ εR)
    (algEquivZeroCut (baseChange R x κ) (sectionBaseChange κ εR)) (D_R.baseChange κ))
  (hD' : RepresentsRelSubPic (baseChange R x₀ κ) (sectionBaseChange κ ε₀R)
    (algEquivZeroCut (baseChange R x₀ κ) (sectionBaseChange κ ε₀R)) (D₀.baseChange κ))
  (f : pullback x₀ (specMap R κ) ⟶ pullback x (specMap R κ)) (hf : f ≫ baseChange R x κ =
    baseChange R x₀ κ)
  (hε : (sectionBaseChange κ ε₀R).1 ≫ f = (sectionBaseChange κ εR).1)
Lean source · statement
theorem characterisation_pullbackHom {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ))
    (a : SchemeHomOver t (D_R.baseChange κ).toBase) :
    Nonempty ((hD'.poincare.pullbackAlong
        (NeronModelInfra.schemeHomOverComp a (RepresentsRelSubPic.pullbackHom f hf hε hD hD'))).L ≅
      Scheme.Modules.rigidify (rigSection (baseChange R x₀ κ) t (sectionBaseChange κ ε₀R))
        (pullback.snd (baseChange R x₀ κ) t)
        ((Scheme.Modules.pullback (curveChange f hf t)).obj (hD.poincare.pullbackAlong a).L))
theorem

baseChangeSnd_comp_restrictHom_eq_of_baseChangeSnd_comp

L526 ↗
AlgebraicGeometry.RelPicard.baseChangeSnd_comp_restrictHom_eq_of_baseChangeSnd_comp
Documentation

Picard restriction and maps with its Poincare characterization commute with base change.

Source context 15 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.RestrictedBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
attribute [local simp] TwistNatAux.twistPt_coe
attribute [local simp] TwistNatAux.piIso_hom
attribute [local simp] TwistNatAux.piIso_inv
open TwistNatAux in
Lean source · statement
theorem _root_.AlgebraicGeometry.RelPicard.baseChangeSnd_comp_restrictHom_eq_of_baseChangeSnd_comp
    {R : Type u} [CommRing R] (κ : Type u) [CommRing κ] [Algebra R κ]
    {𝔛 𝔛₀ : Scheme.{u}} {x : 𝔛 ⟶ Spec (CommRingCat.of R)} {x₀ : 𝔛₀ ⟶ Spec (CommRingCat.of R)}
    {εR : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) x} {ε₀R : SchemeHomOver (𝟙 (Spec
      (CommRingCat.of R))) x₀}
    {D_R : RelativePic0Designation R x} {D₀ : RelativePic0Designation R x₀}
    (hD_R : RepresentsRelSubPic x εR (algEquivZeroCut x εR) D_R)
    (hD₀ : RepresentsRelSubPic x₀ ε₀R (algEquivZeroCut x₀ ε₀R) D₀)
    (hD : RepresentsRelSubPic (baseChange R x κ) (sectionBaseChange κ εR)
      (algEquivZeroCut (baseChange R x κ) (sectionBaseChange κ εR)) (D_R.baseChange κ))
    (hPD : Nonempty (hD.poincare.L ≅ (BaseChange.ofR x εR κ
      (hD_R.poincare.pullbackAlong ⟨pullback.fst D_R.toBase (specMap R κ), pullback.condition⟩)).L))
    (hD' : RepresentsRelSubPic (baseChange R x₀ κ) (sectionBaseChange κ ε₀R)
      (algEquivZeroCut (baseChange R x₀ κ) (sectionBaseChange κ ε₀R)) (D₀.baseChange κ))
    (hPD' : Nonempty (hD'.poincare.L ≅ (BaseChange.ofR x₀ ε₀R κ
      (hD₀.poincare.pullbackAlong ⟨pullback.fst D₀.toBase (specMap R κ), pullback.condition⟩)).L))
    (f : pullback x₀ (specMap R κ) ⟶ pullback x (specMap R κ)) (hf : f ≫ baseChange R x κ =
      baseChange R x₀ κ)
    (τ : SchemeHomOver (specMap R κ) (specMap R κ))
    (hcomm : baseChangeSnd x₀ τ ≫ f = f ≫ baseChangeSnd x τ) :
    (∀ hε : (sectionBaseChange κ ε₀R).1 ≫ f = (sectionBaseChange κ εR).1,
      baseChangeSnd D_R.toBase τ ≫ (RepresentsRelSubPic.pullbackHom f hf hε hD hD').1 =
        (RepresentsRelSubPic.pullbackHom f hf hε hD hD').1 ≫ baseChangeSnd D₀.toBase τ) ∧
    (∀ ν : SchemeHomOver (D_R.baseChange κ).toBase (D₀.baseChange κ).toBase,
      (∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of κ)) (a : SchemeHomOver t (D_R.baseChange
        κ).toBase),
        Nonempty ((hD'.poincare.pullbackAlong (NeronModelInfra.schemeHomOverComp a ν)).L ≅
          Scheme.Modules.rigidify (rigSection (baseChange R x₀ κ) t (sectionBaseChange κ ε₀R))
            (pullback.snd (baseChange R x₀ κ) t)
            ((Scheme.Modules.pullback (curveChange f hf t)).obj (hD.poincare.pullbackAlong a).L))) →
      baseChangeSnd D_R.toBase τ ≫ ν.1 = ν.1 ≫ baseChangeSnd D₀.toBase τ)

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