Theorems · Definition · category theory

CategoryTheory.Presieve.FamilyOfElements.SieveCompatible.cone

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {P : CategoryTheory.Functor Cᵒᵖ A} →
          {X : C} →
            {S : CategoryTheory.Sieve X} →
              {E : Aᵒᵖ} →
                {x : CategoryTheory.Presieve.FamilyOfElements (P.comp (CategoryTheory.coyoneda.obj E)) S.arrows} →
                  x.SieveCompatible → CategoryTheory.Limits.Cone (S.arrows.diagram.op.comp P)

The cone corresponding to a SieveCompatible family of elements, dot notation enabled.

Defined in

Mathlib.CategoryTheory.Sites.Sheaf

Cited by

2 results in Mathlib

Foundations

Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Category