Documentation

Mathlib.CategoryTheory.LocallyDirected

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.

source
class CategoryTheory.Functor.IsLocallyDirected {J : Type u_1} [Category.{v_1, 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.

Instances
    source
    theorem CategoryTheory.Functor.exists_map_eq_of_isLocallyDirected {J : Type u_1} {inst✝ : Category.{v_1, 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) :
    (ConcreteCategory.hom (F.map fi)) xi = (ConcreteCategory.hom (F.map fj)) xj → ∃ (l : J) (fli : l ⟶ i) (flj : l ⟶ j) (x : F.obj l), (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj

    Alias of CategoryTheory.Functor.IsLocallyDirected.cond.

    source
    instance CategoryTheory.instIsLocallyDirectedDiscrete {J : Type u_1} (F : Functor (Discrete J) (Type u_2)) :
    F.IsLocallyDirected
    source
    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