English
If i ≠ j in a discrete index, then a certain induced open image is empty (⊥).
Русский
Если i ≠ j в дискретном индексе, то полученный образ открытых множеств пуст.
LaTeX
$$$(\text{Opens.map}(\operatorname{colimit}.ι\; (F\cdot \mathrm{forgetToPresheafedSpace})\; j).base).obj( (\text{Opens.map}(\mathrm{preservesColimitIso}\; \mathrm{forgetToPresheafedSpace}\; F).inv.base).obj(\dots) ) = ⊥$$$
Lean4
theorem sigma_ι_isOpenEmbedding : IsOpenEmbedding (colimit.ι F i).base :=
by
rw [← show _ = (colimit.ι F i).base from ι_preservesColimitIso_inv (SheafedSpace.forget C) F i]
have : _ = _ ≫ colimit.ι (Discrete.functor ((F ⋙ SheafedSpace.forget C).obj ∘ Discrete.mk)) i :=
HasColimit.isoOfNatIso_ι_hom Discrete.natIsoFunctor i
rw [← Iso.eq_comp_inv] at this
rw [this]
have : colimit.ι _ _ ≫ _ = _ := TopCat.sigmaIsoSigma_hom_ι.{v, v} ((F ⋙ SheafedSpace.forget C).obj ∘ Discrete.mk) i.as
rw [← Iso.eq_comp_inv] at this
cases i
rw [this, ← Category.assoc]
simp_rw [TopCat.isOpenEmbedding_iff_comp_isIso]
-- Porting note: `simp_rw` can't use `TopCat.isOpenEmbedding_iff_isIso_comp`.
-- See https://github.com/leanprover-community/mathlib4/issues/5026
rw [TopCat.isOpenEmbedding_iff_isIso_comp]
exact .sigmaMk
