Theorems · Definition · category theory

CategoryTheory.Presheaf.freeYoneda

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} A] →
        [CategoryTheory.Limits.HasCoproducts A] → C → A → CategoryTheory.Functor Cᵒᵖ A

Given X : C and M : A, this is the presheaf Cᵒᵖ ⥤ A which sends Y : Cᵒᵖ to the coproduct of copies of M indexed by Y.unop ⟶ X.

Defined in

Mathlib.CategoryTheory.Generator.Presheaf

Cited by

11 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasCoproducts