app_inv_app' — Mathlib

English

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

Русский

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

LaTeX

$$IsIso f (при условии) [h' : Epi f.base]$$

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) ≫ invApp f ((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 :=
  by
  simp only [TopCat.Presheaf.pushforward_obj_obj, app_invApp, Opens.carrier_eq_coe, homOfLE_leOfHom, eqToHom_op]
  tauto

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