English
The family of inclusion maps ι_i jointly surjects onto the glued space: every point of the glued space comes from some piece ι_i.
Русский
Семейство отображений ι_i совместно покрывает склеенное пространство: любой элемент склеенного пространства происходит как образ некоторого ι_i.
LaTeX
$$$\\forall x \\in 𝖣.glued,\\; \\exists i, y: y \\in U_i \\land (\\iota_i)_{base}(y)=x$$$
Lean4
theorem ι_image_preimage_eq (i j : D.J) (U : Opens (D.U i).carrier) :
(Opens.map (𝖣.ι j).base).obj ((D.ι_isOpenEmbedding i).isOpenMap.functor.obj U) =
(opensFunctor (D.f j i)).obj ((Opens.map (𝖣.t j i).base).obj ((Opens.map (𝖣.f i j).base).obj U)) :=
by
ext1
dsimp only [Opens.map_coe, IsOpenMap.coe_functor_obj]
rw [← show _ = (𝖣.ι i).base from 𝖣.ι_gluedIso_inv (PresheafedSpace.forget _) i, ←
show _ = (𝖣.ι j).base from 𝖣.ι_gluedIso_inv (PresheafedSpace.forget _) j]
rw [TopCat.coe_comp, TopCat.coe_comp, Set.image_comp, Set.preimage_comp, Set.preimage_image_eq]
· refine Eq.trans (D.toTopGlueData.preimage_image_eq_image' _ _ _) ?_
dsimp
rw [Set.image_comp]
refine congr_arg (_ '' ·) ?_
rw [Set.eq_preimage_iff_image_eq, ← Set.image_comp]
swap
· exact CategoryTheory.ConcreteCategory.bijective_of_isIso (C := TopCat) _
change (D.t i j ≫ D.t j i).base '' _ = _
rw [𝖣.t_inv]
simp
· rw [← TopCat.mono_iff_injective]
infer_instance
