app_inv_app' — Mathlib

English

If an open immersion base map is epi, then f is an isomorphism in LocallyRingedSpace.

Русский

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

LaTeX

$$$[\text{epi}(f.base)] \Rightarrow IsIso(f)$$$

Lean4

/-- A variant of `app_inv_app` that gives an `eqToHom` instead of `homOfLe`. -/
@[reassoc]
theorem app_inv_app' (U : Opens Y) (hU : (U : Set Y) ⊆ Set.range f.base) :
    f.c.app (op U) ≫ H.invApp _ ((Opens.map f.base).obj U) =
      Y.presheaf.map
        (eqToHom <|
            le_antisymm (Set.image_preimage_subset f.base U.1) <|
              (Set.image_preimage_eq_inter_range (f := f.base) (t := U.1)).symm ▸
                Set.subset_inter_iff.mpr ⟨fun _ h => h, hU⟩).op :=
  PresheafedSpace.IsOpenImmersion.app_invApp f.1 U

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