English
Each inclusion map i from the discrete index into the colimit carries an open embedding on bases.
Русский
Каждое вложение i из дискретного индекса в колимит сохраняет открытое вложение на базисе.
LaTeX
$$$\text{IsOpenEmbedding}(((\text{functor}) X)\, .base)$ for the colimit injections$$
Lean4
theorem image_preimage_is_empty (j : Discrete ι) (h : i ≠ j) (U : Opens (F.obj i)) :
(Opens.map (colimit.ι (F ⋙ SheafedSpace.forgetToPresheafedSpace) j).base).obj
((Opens.map (preservesColimitIso SheafedSpace.forgetToPresheafedSpace F).inv.base).obj
((sigma_ι_isOpenEmbedding F i).isOpenMap.functor.obj U)) =
⊥ :=
by
ext x
apply iff_false_intro
rintro ⟨y, hy, eq⟩
replace eq :=
ConcreteCategory.congr_arg
(preservesColimitIso (SheafedSpace.forget C) F ≪≫
HasColimit.isoOfNatIso Discrete.natIsoFunctor ≪≫ TopCat.sigmaIsoSigma.{v, v} _).hom
eq
simp_rw [CategoryTheory.Iso.trans_hom, ← TopCat.comp_app, ← PresheafedSpace.comp_base] at eq
rw [ι_preservesColimitIso_inv] at eq
change ((SheafedSpace.forget C).map (colimit.ι F i) ≫ _) y = ((SheafedSpace.forget C).map (colimit.ι F j) ≫ _) x at eq
cases i; cases j
rw [ι_preservesColimitIso_hom_assoc, ι_preservesColimitIso_hom_assoc, HasColimit.isoOfNatIso_ι_hom_assoc,
HasColimit.isoOfNatIso_ι_hom_assoc, TopCat.sigmaIsoSigma_hom_ι, TopCat.sigmaIsoSigma_hom_ι] at eq
exact h (congr_arg Discrete.mk (congr_arg Sigma.fst eq))
