English
Let f: X → Y be a morphism of schemes and U an open subset of Y. The isomorphism that identifies the restricted pullback with the corresponding pullback commutes with the restriction map: the hom part of the restriction iso composed with the restriction embedding equals the canonical pullback projection to X.
Русский
Пусть f: X → Y — морфизм схем, U — открытое подмножество Y. Изоморфизм, связывающий ограниченный взятие произведения по ограничению с соответствующим произведением, удовлетворяет тождественному свойству: композиция гомотряRestriction-изоморфизмом с инклузией ограничения равна каноническому проектору на X.
LaTeX
$$$\big(\mathrm{pullbackRestrictIsoRestrict}(f,U)\big)^{\mathrm{hom}} \;\circ \; (f|_{U})_{ι} = \mathrm{pullback.fst}(f,U.ι).$$$
Lean4
@[reassoc (attr := simp)]
theorem pullbackRestrictIsoRestrict_hom_ι {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) :
(pullbackRestrictIsoRestrict f U).hom ≫ (f ⁻¹ᵁ U).ι = pullback.fst f _ := by delta pullbackRestrictIsoRestrict; simp
