Theorems · Definition · category theory

CategoryTheory.Equalizer.Presieve.Arrows.forkMap

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type w)) →
      {B : C} →
        {I : Type t} →
          [inst_1 : Small.{w, t} I] →
            (X : I → C) →
              ((i : I) → X i ⟶ B) → (P.obj (Opposite.op B) ⟶ CategoryTheory.Equalizer.Presieve.Arrows.FirstObj P X)

The left morphism of the fork diagram.

Defined in

Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategorySmall