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