app_inv_app' — Mathlib

English

The base map of each colimit injection is an open embedding.

Русский

Базовая карта каждой инъекции в колимит является открытым вложением.

LaTeX

$$$\text{IsOpenEmbedding}((\text{colimit.ι } F i).\text{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 :=
  PresheafedSpace.IsOpenImmersion.app_invApp f U

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