Theorems · Definition · category theory
CategoryTheory.coyoneda
{C : Type u₁} →
[inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C (Type v₁))The co-Yoneda embedding, as a functor from Cᵒᵖ into co-presheaves on C.
- Defined in
- Mathlib.CategoryTheory.Yoneda
- Cited by
- 208 results in Mathlib
- Foundations
- Depth 27 from the axioms, rests on 163 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Functorstatement · cited by 16,252
- Oppositestatement · cited by 8,081
- CategoryTheory.yonedaproof · cited by 351
- CategoryTheory.Functor.flipproof · cited by 320
Cited by328
Results whose statement or proof uses this declaration.
- CategoryTheory.Presheaf.IsSheafproof · cited by 991
- CategoryTheory.IsCardinalPresentableproof · cited by 39
- CategoryTheory.isSheaf_iff_isSheaf_of_typeproof · cited by 30
- CategoryTheory.Functor.leftAdjointObjIsDefinedproof · cited by 16
- CategoryTheory.Functor.functorHomproof · cited by 16
- CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBystatement · cited by 10
- CategoryTheory.coyonedaEquivstatement and proof · cited by 9
- CategoryTheory.Functor.partialLeftAdjointObjproof · cited by 9
- CategoryTheory.Functor.coconesproof · cited by 9
- CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitorproof · cited by 9
- CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitorproof · cited by 9
- CategoryTheory.Presheaf.isSheaf_of_iso_iffproof · cited by 8
Showing the 200 most cited of 328.