English
For any open immersion f: X → Y and open U ⊆ X, the composition (f.isoImage U).inv ≫ U.ι ≫ f equals (f ''ᵁ U).ι; equivalently, the inverse of the image is compatible with the inclusions.
Русский
Для открытого внедрения f: X → Y и открытого U ⊆ X выполняется равенство (f.isoImage U).inv ∘ U.ι ∘ f = (f ''ᵁ U).ι
LaTeX
$$$(f.isoImage U).inv \\circ U.\\iota \\circ f = (f ''ᵁ U).\\iota$$$
Lean4
@[reassoc (attr := simp)]
theorem isoImage_inv_ι {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] (U : X.Opens) :
(f.isoImage U).inv ≫ U.ι ≫ f = (f ''ᵁ U).ι :=
IsOpenImmersion.isoOfRangeEq_inv_fac _ _ _