AlgebraicGeometry.RelPicard.exists_fibreIso_hom_comp_eq
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FibreProjectionComparison
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
open NeronModelInfraLean source · statement
theorem _root_.AlgebraicGeometry.RelPicard.exists_fibreIso_hom_comp_eq
{R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
{T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
{k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ T)
(x : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
(hx : s ≫ t = x) :
∃ φ : pullback (pullback.snd c t) s ≅ pullback c x,
φ.hom ≫ pullback.snd c x = fibreAt c t s ∧
φ.hom ≫ pullback.fst c x = pullback.fst (pullback.snd c t) s ≫ pullback.fst c t ∧
φ.hom ≫ baseChangeSnd c (⟨s, hx⟩ : SchemeHomOver x t) =
pullback.fst (pullback.snd c t) s