isIso_of_subset — Mathlib

English

Let f: X → Y be an open immersion of presheafed spaces. If U is an open subset of Y contained in the image of f, then the induced map f.c.app(op U) is an isomorphism.

Русский

Пусть f: X → Y — открытое вложение прешефед пространств. Если U — открытое подмножество Y, содержащееся в образе f, то полученное отображение f.c.app(op U) является изоморфизмом.

LaTeX

$$$ \\mathrm{IsIso}\\big( f.c.app\\,\\mathrm{op}(U) \\big)$$$

Lean4

theorem isIso_of_subset {X Y : PresheafedSpace C} (f : X ⟶ Y) [H : PresheafedSpace.IsOpenImmersion f]
    (U : Opens Y.carrier) (hU : (U : Set Y.carrier) ⊆ Set.range f.base) : IsIso (f.c.app <| op U) :=
  by
  have : U = H.base_open.isOpenMap.functor.obj ((Opens.map f.base).obj U) :=
    by
    ext1
    exact (Set.inter_eq_left.mpr hU).symm.trans Set.image_preimage_eq_inter_range.symm
  convert H.c_iso ((Opens.map f.base).obj U)

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