English
Restriction along an open immersion g: U → Y identifies with a pullback along g; there is a natural isomorphism between the restricted morphism’s arrow and the pullback arrow.
Русский
Ограничение вдоль открытого вложения g: U → Y идентифицируется с ограничением по произведению; существует естественный изоморфизм между стрелами ограниченного морфизма и стрелой произведения.
LaTeX
$$$Arrow.mk (f\restriction g.opensRange) \cong Arrow.mk (pullback.snd f g)$$$
Lean4
/-- Restricting a morphism onto the image of an open immersion is isomorphic to the base change
along the immersion. -/
def morphismRestrictOpensRange {X Y U : Scheme.{u}} (f : X ⟶ Y) (g : U ⟶ Y) [hg : IsOpenImmersion g] :
Arrow.mk (f ∣_ g.opensRange) ≅ Arrow.mk (pullback.snd f g) :=
by
let V : Y.Opens := g.opensRange
let e := IsOpenImmersion.isoOfRangeEq g V.ι Subtype.range_coe.symm
let t : pullback f g ⟶ pullback f V.ι :=
pullback.map _ _ _ _ (𝟙 _) e.hom (𝟙 _) (by rw [Category.comp_id, Category.id_comp])
(by rw [Category.comp_id, IsOpenImmersion.isoOfRangeEq_hom_fac])
symm
refine Arrow.isoMk (asIso t ≪≫ pullbackRestrictIsoRestrict f V) e ?_
rw [Iso.trans_hom, asIso_hom, ← Iso.comp_inv_eq, ← cancel_mono g, Arrow.mk_hom, Arrow.mk_hom, Category.assoc,
Category.assoc, Category.assoc, IsOpenImmersion.isoOfRangeEq_inv_fac, ← pullback.condition, morphismRestrict_ι,
pullbackRestrictIsoRestrict_hom_ι_assoc, pullback.lift_fst_assoc, Category.comp_id]
