Theorems · Definition · category theory

CategoryTheory.Presheaf.equalizerSieve

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {FD : D → D → Type u_1} →
          {CD : D → Type w} →
            [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
              [inst_3 : CategoryTheory.ConcreteCategory D FD] →
                {F : CategoryTheory.Functor Cᵒᵖ D} →
                  {X : Cᵒᵖ} →
                    CategoryTheory.ToType (F.obj X) →
                      CategoryTheory.ToType (F.obj X) → CategoryTheory.Sieve (Opposite.unop X)

If F : Cᵒᵖ ⥤ D is a presheaf with values in a concrete category, if x and y are elements in F.obj X, this is the sieve of X.unop consisting of morphisms f such that F.map f.op x = F.map f.op y.

Defined in

Mathlib.CategoryTheory.Sites.LocallyInjective

Cited by

15 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategory