English
A version of congruence for morphisms in the presheafed spaces category, relating components under an equality.
Русский
Версия конгруэнтности для морфизмов в категории прешефдов пространства, связывающая компоненты при равенстве.
LaTeX
$$$\forall X,Y, \alpha,\beta : X \to Y, (\alpha = \beta) \Rightarrow \alpha.c.app(U) = \beta.c.app(U) \circ X.presheaf.map(\text{eqToHom}(⋯))$$$
Lean4
/-- The isomorphism from the restriction to the top subspace.
-/
@[simps]
def restrictTopIso (X : PresheafedSpace C) : X.restrict (Opens.isOpenEmbedding ⊤) ≅ X
where
hom := X.ofRestrict _
inv := X.toRestrictTop
hom_inv_id := by
ext
· rfl
· erw [comp_c, toRestrictTop_c, whiskerRight_id', comp_id, ofRestrict_top_c, eqToHom_map, eqToHom_trans,
eqToHom_refl]
rfl
inv_hom_id := by
ext
· rfl
· erw [comp_c, ofRestrict_top_c, toRestrictTop_c, eqToHom_map, whiskerRight_id', comp_id, eqToHom_trans,
eqToHom_refl]
rfl
