isoRestrict — Mathlib

Lean4
/-- An open immersion `f : X ⟶ Y` induces an isomorphism `X ≅ Y|_{f(X)}`. -/
@[simps! hom_c_app]
noncomputable def isoRestrict : X ≅ Y.restrict H.base_open :=
  PresheafedSpace.isoOfComponents (Iso.refl _) <| by
    symm
    fapply NatIso.ofComponents
    · intro U
      refine asIso (f.c.app (op (opensFunctor f |>.obj (unop U)))) ≪≫ X.presheaf.mapIso (eqToIso ?_)
      induction U with
      | op U => ?_
      cases U
      dsimp only [IsOpenMap.functor, Functor.op, Opens.map]
      congr 2
      erw [Set.preimage_image_eq _ H.base_open.injective]
      rfl
    · intro U V i
      dsimp
      simp only [NatTrans.naturality_assoc, TopCat.Presheaf.pushforward_obj_obj, TopCat.Presheaf.pushforward_obj_map,
        Quiver.Hom.unop_op, Category.assoc]
      rw [← X.presheaf.map_comp, ← X.presheaf.map_comp]
      congr 1
Похожие утверждения