Theorems · Definition · category theory

CategoryTheory.Presieve.FamilyOfElements

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → CategoryTheory.Functor Cᵒᵖ (Type w) → CategoryTheory.Presieve X → Type (max (max u₁ w) v₁)

A family of elements for a presheaf P given a collection of arrows R with fixed codomain X consists of an element of P Y for every f : Y ⟶ X in R. A presheaf is a sheaf (resp, separated) if every compatible family of elements has exactly one (resp, at most one) amalgamation. This data is referred to as a family in [MM92], Chapter III, Section 4. It is also a concrete version of the elements of the middle object in the Stacks entry which is more useful for direct calculations. It is also used implicitly in Definition C2.1.2 in [Elephant].

Defined in

Mathlib.CategoryTheory.Sites.IsSheafFor

Cited by

103 results in Mathlib

Foundations

Depth 11 from the axioms, rests on 65 definitions · uses propext

Assumes

CategoryTheory.Category