app_invApp — Mathlib

English

If the base map is epi, then an open immersion morphism is an isomorphism.

Русский

Если базовая карта является эпиморфизмом, то открытое вложение является изоморфизмом.

LaTeX

$$$[\text{h' : Epi } f.base] \Rightarrow IsIso f$$$

Lean4

@[reassoc (attr := simp)]
theorem app_invApp (U : Opens Y) :
    f.c.app (op U) ≫ H.invApp _ ((Opens.map f.base).obj U) =
      Y.presheaf.map
        ((homOfLE (Set.image_preimage_subset f.base U.1)).op :
          op U ⟶ op (opensFunctor f |>.obj ((Opens.map f.base).obj U))) :=
  PresheafedSpace.IsOpenImmersion.app_invApp f U

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