isoOfRangeEq — Mathlib

English

Two open immersions f: X → Z and g: Y → Z with equal images (range) are isomorphic: X ≅ Y.

Русский

Два открытых вложения f: X → Z и g: Y → Z с равными образами образуют изоморфизм X ≅ Y.

LaTeX

$$$\exists\!\; \varphi: X \cong Y \text{ such that } \operatorname{range}(f) = \operatorname{range}(g)$$$

Lean4

/-- Two open immersions with equal range are isomorphic. -/
def isoOfRangeEq [IsOpenImmersion g] (e : Set.range f.base = Set.range g.base) : X ≅ Y
    where
  hom := lift g f (le_of_eq e)
  inv := lift f g (le_of_eq e.symm)
  hom_inv_id := by rw [← cancel_mono f]; simp
  inv_hom_id := by rw [← cancel_mono g]; simp

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