AlgebraicGeometry.Scheme.Cover.recoveredOverlapTransport_isPullback
A recovered overlap square remains cartesian after transporting the base-change functor and its actual overlap morphism.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Scheme.Cover
universe uLean source · statement
theorem recoveredOverlapTransport_isPullback
{S L : Scheme.{u}} {F G : Over S ⥤ Over L} (e : F ≅ G)
{A B V W : Over S} {Z : Over L}
(d : V ⟶ A) (r : W ⟶ B) (hA : F.obj A ⟶ Z) (hB : F.obj B ⟶ Z)
(a : F.obj V ⟶ F.obj W) (b : G.obj V ⟶ G.obj W)
(hab : e.hom.app V ≫ b = a ≫ e.hom.app W)
(hPB : IsPullback (F.map d).left (a ≫ F.map r).left hA.left hB.left) :
IsPullback (G.map d).left (b ≫ G.map r).left
(e.inv.app A ≫ hA).left (e.inv.app B ≫ hB).left