Locally directed gluing

We say that a diagram of sets is "locally directed" if for any V, W ⊆ U in the diagram, V ∩ W is a union of elements in the diagram. Equivalently, for every x ∈ U in the diagram, the set of elements containing x is directed (and hence the name).

This is the condition needed to show that a colimit (in TopCat) of open embeddings is the gluing of the open sets. See Mathlib/AlgebraicGeometry/Gluing.lean for an actual application.

class CategoryTheory.Functor.IsLocallyDirected {J : Type u_1} [Category.{u_3, u_1} J] (F : Functor J (Type u_2)) : Prop

We say that a functor F to Type* is locally directed if for every x ∈ F.obj k, the set of F.obj containing x is (co)directed. That is, for each diagram

      x ∈ Fₖ
    ↗       ↖
xᵢ ∈ Fᵢ    xⱼ ∈ Fⱼ

there exists

xᵢ ∈ Fᵢ    xⱼ ∈ Fⱼ
    ↖       ↗
      xₗ ∈ Fₗ

that commutes with it.

• cond {i j k : J} (fi : i ⟶ k) (fj : j ⟶ k) (xi : F.obj i) (xj : F.obj j) : F.map fi xi = F.map fj xj → ∃ (l : J) (fli : l ⟶ i) (flj : l ⟶ j) (x : F.obj l), F.map fli x = xi ∧ F.map flj x = xj

theorem CategoryTheory.Functor.exists_map_eq_of_isLocallyDirected {J : Type u_1} {inst✝ : Category.{u_3, u_1} J} (F : Functor J (Type u_2)) [self : F.IsLocallyDirected] {i j k : J} (fi : i ⟶ k) (fj : j ⟶ k) (xi : F.obj i) (xj : F.obj j) : F.map fi xi = F.map fj xj → ∃ (l : J) (fli : l ⟶ i) (flj : l ⟶ j) (x : F.obj l), F.map fli x = xi ∧ F.map flj x = xj

Alias of CategoryTheory.Functor.IsLocallyDirected.cond.

instance CategoryTheory.instIsLocallyDirectedDiscrete {J : Type u_1} (F : Functor (Discrete J) (Type u_2)) : F.IsLocallyDirected

instance CategoryTheory.instIsLocallyDirectedWidePushoutShapeOfMonoObjNoneSomeMapInit {J : Type u_1} (F : Functor (Limits.WidePushoutShape J) (Type u_2)) [∀ (i : J), Mono (F.map (Limits.WidePushoutShape.Hom.init i))] : F.IsLocallyDirected