isoImage_inv_ι — Mathlib

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 _ _ _

Похожие утверждения