English
For opens U ≤ V ≤ W in X, the restriction of the restriction X|_U|_V is isomorphic to X|_V|_U, exhibiting commutativity of successive restrictions.
Русский
Для открытых множеств U ≤ V ≤ W на X ограничение U внутри V внутри W эквивалентно ограничению V внутри U, то есть ограничение подмножеств ведёт к коммутативности последовательных ограничений.
LaTeX
$$$ (U.\\iota \\restriction V).toScheme \\cong (V.\\iota \\restriction U).toScheme $$$
Lean4
/-- `X ∣_ U ∣_ V` is isomorphic to `X ∣_ V ∣_ U` -/
noncomputable def restrictRestrictComm (X : Scheme.{u}) (U V : X.Opens) : (U.ι ⁻¹ᵁ V).toScheme ≅ V.ι ⁻¹ᵁ U :=
IsOpenImmersion.isoOfRangeEq (Opens.ι _ ≫ U.ι) (Opens.ι _ ≫ V.ι) <| by
simp only [comp_coeBase, TopCat.coe_comp, Set.range_comp, Opens.range_ι, Opens.map_coe,
Set.image_preimage_eq_inter_range, Set.inter_comm (U : Set X)]
