English
Restricting a morphism twice is canonically isomorphic to a single restriction: restricting f to U and then to V is isomorphic to restricting f directly to V via the intermediate opens.
Русский
Двойное ограничение морфизма канонически изоморфно одному ограничению: ограничение f до U затем до V эквивалентно ограничению f непосредственно до V.
LaTeX
$$def morphismRestrictRestrict {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : U.toScheme.Opens) : Arrow.mk (f|_U|_V) ≅ Arrow.mk (f|_U.ι ''ᵁ V)$$
Lean4
/-- Restricting a morphism twice is isomorphic to one restriction. -/
def morphismRestrictRestrict {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V : U.toScheme.Opens) :
Arrow.mk (f ∣_ U ∣_ V) ≅ Arrow.mk (f ∣_ U.ι ''ᵁ V) :=
by
refine Arrow.isoMk' _ _ ((Scheme.Opens.ι _).isoImage _ ≪≫ Scheme.isoOfEq _ ?_) ((Scheme.Opens.ι _).isoImage _) ?_
· exact image_morphismRestrict_preimage f U V
·
rw [← cancel_mono (Scheme.Opens.ι _), Iso.trans_hom, Category.assoc, Category.assoc, Category.assoc,
morphismRestrict_ι, Scheme.isoOfEq_hom_ι_assoc, Scheme.Hom.isoImage_hom_ι_assoc, Scheme.Hom.isoImage_hom_ι,
morphismRestrict_ι_assoc, morphismRestrict_ι]
