opensRange_comp_of_isIso — Mathlib

English

For an open immersion f, the preimage of the image of an open set U equals U.

Русский

Для открытого вложения f предобраз образа множества открытого U равен самому U.

LaTeX

$$$f^{-1}(f(U)) = U$ for open immersion f$$

Lean4

theorem opensRange_comp_of_isIso {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] [IsOpenImmersion g] :
    (f ≫ g).opensRange = g.opensRange := by rw [opensRange_comp, opensRange_of_isIso, image_top_eq_opensRange]

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