isOpenEmbedding_iff_isIso_comp — Mathlib

English

If f: X ⟶ Y and g: Y ⟶ Z with IsIso g, then IsOpenEmbedding (f ≫ g) ↔ IsOpenEmbedding f.

Русский

Если f: X ⟶ Y и g: Y ⟶ Z с IsIso g, то IsOpenEmbedding (f ≫ g) эквивалентно IsOpenEmbedding f.

LaTeX

$$$\\mathrm{IsOpenEmbedding}(f \\;\\mathrm{≫}\\; g) \\iff \\mathrm{IsOpenEmbedding}(f)$$$

Lean4

theorem isOpenEmbedding_iff_isIso_comp {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] :
    IsOpenEmbedding (f ≫ g) ↔ IsOpenEmbedding g := by
  constructor
  · intro h
    convert h.comp (TopCat.homeoOfIso (asIso f).symm).isOpenEmbedding
    exact congr_arg (DFunLike.coe ∘ ConcreteCategory.hom) (IsIso.inv_hom_id_assoc f g).symm
  · exact fun h => h.comp (TopCat.homeoOfIso (asIso f)).isOpenEmbedding

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