English
There is a functor from Opens X to Opens Y associated with an open immersion f: X → Y.
Русский
Существует функтор от Opens X в Opens Y, связанный с открытым вложением f: X → Y.
LaTeX
$$$\text{opensFunctor} : \mathrm{Opens}(X) \to \mathrm{Opens}(Y).$$$
Lean4
/-- Suppose `X Y : SheafedSpace C`, where `C` is a concrete category,
whose forgetful functor reflects isomorphisms, preserves limits and filtered colimits.
Then a morphism `X ⟶ Y` that is a topological open embedding
is an open immersion iff every stalk map is an iso.
-/
theorem of_stalk_iso {X Y : SheafedSpace C} (f : X ⟶ Y) (hf : IsOpenEmbedding f.base)
[H : ∀ x : X.1, IsIso (f.stalkMap x)] : SheafedSpace.IsOpenImmersion f :=
{ base_open := hf
c_iso := fun U =>
by
apply (config := { allowSynthFailures := true })
TopCat.Presheaf.app_isIso_of_stalkFunctor_map_iso
(show Y.sheaf ⟶ (TopCat.Sheaf.pushforward _ f.base).obj X.sheaf from ⟨f.c⟩)
rintro ⟨_, y, hy, rfl⟩
specialize H y
delta PresheafedSpace.Hom.stalkMap at H
haveI H' := TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing C hf.toIsInducing X.presheaf y
have := IsIso.comp_isIso' H (@IsIso.inv_isIso _ _ _ _ _ H')
rwa [Category.assoc, IsIso.hom_inv_id, Category.comp_id] at this }
