isoOfRangeEq — Mathlib

English

An open immersion of a PresheafedSpace yields an open immersion of the associated LocallyRingedSpace.

Русский

Открытое внедрение PresheafedSpace соответствует открытому внедрению LocallyRingedSpace.

LaTeX

$$$\text{LocallyRingedSpace.IsOpenImmersion} (toLocallyRingedSpaceHom Y f)$$$

Lean4

/-- Two open immersions with equal range is isomorphic. -/
@[simps]
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

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