English
A canonical comparison between the restriction of X and the original X is given by a morphism whose c-component is a specific eqToHom.
Русский
Каноническое сравнение между ограничением X и X задаётся морфизмом с компонентой c равной конкретному eqToHom.
LaTeX
$$$(X.ofRestrict(\mathrm{Opens.isOpenEmbedding}\;\top)).c = \mathrm{eqToHom}(\text{...})$$$
Lean4
instance ofRestrict_mono {U : TopCat} (X : PresheafedSpace C) (f : U ⟶ X.1) (hf : IsOpenEmbedding f) :
Mono (X.ofRestrict hf) :=
by
haveI : Mono f := (TopCat.mono_iff_injective _).mpr hf.injective
constructor
intro Z g₁ g₂ eq
ext1
· have := congr_arg PresheafedSpace.Hom.base eq
simp only [PresheafedSpace.comp_base, PresheafedSpace.ofRestrict_base] at this
rw [cancel_mono] at this
exact this
· ext V
have hV : (Opens.map (X.ofRestrict hf).base).obj (hf.isOpenMap.functor.obj V) = V :=
by
ext1
exact Set.preimage_image_eq _ hf.injective
haveI : IsIso (hf.isOpenMap.adjunction.counit.app (unop (op (hf.isOpenMap.functor.obj V)))) :=
NatIso.isIso_app_of_isIso (whiskerLeft hf.isOpenMap.functor hf.isOpenMap.adjunction.counit) V
have := PresheafedSpace.congr_app eq (op (hf.isOpenMap.functor.obj V))
rw [PresheafedSpace.comp_c_app, PresheafedSpace.comp_c_app, PresheafedSpace.ofRestrict_c_app, Category.assoc,
cancel_epi] at this
have h : _ ≫ _ = _ ≫ _ ≫ _ := congr_arg (fun f => (X.restrict hf).presheaf.map (eqToHom hV).op ≫ f) this
simp only [g₁.c.naturality, g₂.c.naturality_assoc] at h
simp only [eqToHom_op, eqToHom_map, eqToHom_trans, ← IsIso.comp_inv_eq, inv_eqToHom, Category.assoc] at h
simpa using h
