Theorems · Definition · category theory

CategoryTheory.Presieve.FamilyOfElements.singletonEquiv

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type w)) →
      {X Y : C} →
        (f : X ⟶ Y) →
          CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Presieve.singleton f) ≃ P.obj (Opposite.op X)

A family of elements on { f : X ⟶ Y } is an element of F(X).

Defined in

Mathlib.CategoryTheory.Sites.IsSheafFor

Cited by

5 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.Category