English
In a localization setting, the basic open of x in Spec R is isomorphic to Spec of R localized away from x, matching with the away-to-awayRight map, and this is compatible with subsequent maps.
Русский
В конфигурации локализации базовое открытое множество в Spec R изоморфно Spec R локализованному away от x, совместимо с awayToAwayRight и дальнейшими отображениями.
LaTeX
$$$\\text{basicOpenIsoSpecAway}(x)^{-1} \\circ (\\text{Spec } R).homOfLE = \\text{Spec.map} \\circ (\\text{basicOpenIsoSpecAway}(f)^{-1})$$$
Lean4
/-- If `U ≤ V` are opens of `X`, the restriction of `U` to `V` is isomorphic to `U`. -/
noncomputable def isoOfLE {X : Scheme.{u}} {U V : X.Opens} (hUV : U ≤ V) : (V.ι ⁻¹ᵁ U).toScheme ≅ U :=
IsOpenImmersion.isoOfRangeEq ((V.ι ⁻¹ᵁ U).ι ≫ V.ι) U.ι <|
by
have : V.ι ''ᵁ (V.ι ⁻¹ᵁ U) = U := by simpa [Scheme.Hom.image_preimage_eq_opensRange_inter]
rw [Scheme.comp_coeBase, TopCat.coe_comp, Scheme.Opens.range_ι, Set.range_comp, ← this]
simp
