AlgebraicGeometry.RelPicard.isPullback_baseChangeSnd_curveChange
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsPullback_baseChangeSnd_curveChange
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
GoodReductionJacobian AlgebraicGeometry.RelPicardLean source · statement
theorem _root_.AlgebraicGeometry.RelPicard.isPullback_baseChangeSnd_curveChange
{R : Type u} [CommRing R] {C C' : Scheme.{u}}
{c : C ⟶ Spec (CommRingCat.of R)} {c' : C' ⟶ Spec (CommRingCat.of R)}
(f : C' ⟶ C) (hf : f ≫ c = c')
{T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
(ψ : SchemeHomOver t' t) :
IsPullback (baseChangeSnd c' ψ) (curveChange f hf t')
(curveChange f hf t) (baseChangeSnd c ψ)