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
šŸ”¶ coverage
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) :
    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.

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