comp — Mathlib

English

Two open immersions with the same image are canonically isomorphic.

Русский

Два открытых внедрения с одинаковым изображением канонически изоморфны.

LaTeX

$$$\exists \; X\cong Y \text{ via the lift maps when } \mathrm{range}(f.base)=\mathrm{range}(g.base)$$$

Lean4

/-- The composition of two open immersions is an open immersion. -/
instance comp {Z : PresheafedSpace C} (g : Y ⟶ Z) [hg : IsOpenImmersion g] : IsOpenImmersion (f ≫ g)
    where
  base_open := hg.base_open.comp H.base_open
  c_iso
    U := by
    generalize_proofs h
    dsimp only [AlgebraicGeometry.PresheafedSpace.comp_c_app, unop_op, Functor.op, comp_base, Opens.map_comp_obj]
    apply IsIso.comp_isIso'
    · exact c_iso' g ((opensFunctor f).obj U) (by ext; simp)
    · apply c_iso' f U
      ext1
      dsimp only [Opens.map_coe, IsOpenMap.coe_functor_obj, comp_base, TopCat.coe_comp]
      rw [Set.image_comp, Set.preimage_image_eq _ hg.base_open.injective]

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