Theorems · Definition · category theory

CategoryTheory.Presieve.diagram

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → (S : CategoryTheory.Presieve X) → CategoryTheory.Functor S.category C

Given a sieve S on X : C, its associated diagram S.diagram is defined to be the natural functor from the full subcategory of the over category C/X consisting of arrows in S to C.

Defined in

Mathlib.CategoryTheory.Sites.Sieves

Cited by

17 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category