Theorems · Definition · category theory

CategoryTheory.Equalizer.Presieve.Arrows.FirstObj

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor Cᵒᵖ (Type w) → {I : Type t} → [Small.{w, t} I] → (I → C) → Type w

The middle object of the fork diagram of the Stacks entry. The difference between this and Equalizer.FirstObj P (ofArrows X π) arises if the family of arrows π contains duplicates. The Presieve.ofArrows doesn't see those.

Defined in

Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Cited by

9 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategorySmall