Presheaf

📁 Source: Mathlib/CategoryTheory/Generator/Presheaf.lean

Statistics

Metric	Count
Definitions freeYoneda, freeYonedaHomEquiv	2
Theorems freeYonedaHomEquiv_comp, freeYonedaHomEquiv_comp_assoc, freeYonedaHomEquiv_symm_comp, freeYonedaHomEquiv_symm_comp_assoc, freeYoneda_map, freeYoneda_obj, hasSeparator, isSeparating, isSeparator	9
Total	11

CategoryTheory.Presheaf

Definitions

Name	Category	Theorems
freeYoneda 📖	CompOp	10 math math: instIsCardinalPresentableFunctorOppositeFreeYonedaOfHasColimitsOfSize, isSeparating, freeYonedaHomEquiv_comp, freeYoneda_map, freeYonedaHomEquiv_symm_comp, isSeparator, isStrongGenerator, freeYonedaHomEquiv_comp_assoc, freeYonedaHomEquiv_symm_comp_assoc, freeYoneda_obj
freeYonedaHomEquiv 📖	CompOp	4 math math: freeYonedaHomEquiv_comp, freeYonedaHomEquiv_symm_comp, freeYonedaHomEquiv_comp_assoc, freeYonedaHomEquiv_symm_comp_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
freeYonedaHomEquiv_comp 📖	mathematical	CategoryTheory.Limits.HasCoproducts	DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category freeYoneda CategoryTheory.Functor.obj Opposite.op EquivLike.toFunLike Equiv.instEquivLike freeYonedaHomEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app	—	CategoryTheory.Category.assoc
freeYonedaHomEquiv_comp_assoc 📖	mathematical	CategoryTheory.Limits.HasCoproducts	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.category freeYoneda EquivLike.toFunLike Equiv.instEquivLike freeYonedaHomEquiv CategoryTheory.NatTrans.app	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' freeYonedaHomEquiv_comp
freeYonedaHomEquiv_symm_comp 📖	mathematical	CategoryTheory.Limits.HasCoproducts	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category freeYoneda DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.obj Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm freeYonedaHomEquiv CategoryTheory.NatTrans.app	—	Equiv.injective freeYonedaHomEquiv_comp Equiv.apply_symm_apply
freeYonedaHomEquiv_symm_comp_assoc 📖	mathematical	CategoryTheory.Limits.HasCoproducts	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category freeYoneda DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.obj Opposite.op EquivLike.toFunLike Equiv.instEquivLike Equiv.symm freeYonedaHomEquiv CategoryTheory.NatTrans.app	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' freeYonedaHomEquiv_symm_comp
freeYoneda_map 📖	mathematical	CategoryTheory.Limits.HasCoproducts	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite freeYoneda CategoryTheory.Limits.Sigma.map' CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
freeYoneda_obj 📖	mathematical	CategoryTheory.Limits.HasCoproducts	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite freeYoneda CategoryTheory.Limits.sigmaObj CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda	—	—
hasSeparator 📖	mathematical	CategoryTheory.Limits.HasCoproducts	CategoryTheory.HasSeparator CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category	—	CategoryTheory.Limits.functorCategoryHasColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape isSeparator CategoryTheory.isSeparator_separator
isSeparating 📖	mathematical	CategoryTheory.Limits.HasCoproducts CategoryTheory.ObjectProperty.IsSeparating CategoryTheory.ObjectProperty.ofObj CategoryTheory.Category.toCategoryStruct	CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category freeYoneda	—	CategoryTheory.NatTrans.ext' Equiv.injective freeYonedaHomEquiv_symm_comp CategoryTheory.ObjectProperty.ofObj_apply
isSeparator 📖	mathematical	CategoryTheory.Limits.HasCoproducts CategoryTheory.ObjectProperty.IsSeparating CategoryTheory.ObjectProperty.ofObj CategoryTheory.Category.toCategoryStruct	CategoryTheory.IsSeparator CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Limits.sigmaObj freeYoneda	—	CategoryTheory.ObjectProperty.IsSeparating.isSeparator_coproduct isSeparating

---

← Back to Index