Theorems · Definition · category theory

CategoryTheory.Presheaf.freeYonedaHomEquiv

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} A] →
        [inst_2 : CategoryTheory.Limits.HasCoproducts A] →
          {X : C} →
            {M : A} →
              {F : CategoryTheory.Functor Cᵒᵖ A} →
                (CategoryTheory.Presheaf.freeYoneda X M ⟶ F) ≃ (M ⟶ F.obj (Opposite.op X))

The bijection (Presheaf.freeYoneda X M ⟶ F) ≃ (M ⟶ F.obj (op X)).

Defined in

Mathlib.CategoryTheory.Generator.Presheaf

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasCoproducts