Points of glued presheafed spaces

For glue data D of presheafed spaces, two points of the charts U i and U j have the same image in the glued space exactly when they come from a common point of the overlap V i j, that is, when they are related by D.toTopGlueData.Rel. This is the statement TopCat.GlueData.ι_eq_iff_rel for the underlying glue data of topological spaces, transported along the identification of the underlying space of the glued presheafed space with the glued topological space. It is the presheafed-space counterpart of AlgebraicGeometry.Scheme.GlueData.ι_eq_iff, and is how data defined chartwise on a glued space is shown to be well defined.

Main results

• AlgebraicGeometry.PresheafedSpace.GlueData.ι_eq_iff_rel: ι i x = ι j y if and only if x and y come from a common point of V i j.

theorem AlgebraicGeometry.PresheafedSpace.GlueData.ι_eq_iff_rel {C : Type u} [CategoryTheory.Category.{v, u} C] (D : GlueData C) [CategoryTheory.Limits.HasMulticoequalizer D.diagram] [CategoryTheory.Limits.PreservesColimit D.diagram.multispan (forget C)] (i j : D.J) (x : ↑↑(D.U i)) (y : ↑↑(D.U j)) : (CategoryTheory.ConcreteCategory.hom (D.ι i).base) x = (CategoryTheory.ConcreteCategory.hom (D.ι j).base) y ↔ D.toTopGlueData.Rel ⟨i, x⟩ ⟨j, y⟩

Points with the same image in a glued presheafed space. Points x of U i and y of U j have the same image in the glued space if and only if there is a point z of V i j with f i j z = x and f j i (t i j z) = y. It suffices that this gluing colimit exists and is preserved by the forgetful functor to topological spaces.