Yoneda

📁 Source: Mathlib/CategoryTheory/Limits/Yoneda.lean

Statistics

Metric	Count
Definitions colimitCocone, colimitCoconeIsColimit, colimitCoyonedaIso, isColimitYonedaEquiv, isLimitCoyonedaEquiv, coneOfSectionCompCoyoneda, coneOfSectionCompYoneda, coyonedaJointlyReflectsLimits, yonedaJointlyReflectsLimits	9
Theorems colimitCoconeIsColimit_desc, colimitCocone_pt, colimitCocone_ι_app, instHasColimitObjOppositeFunctorTypeCoyoneda, corepresentable_preservesLimit, corepresentable_preservesLimits, corepresentable_preservesLimitsOfShape, representable_preservesLimit, representable_preservesLimits, representable_preservesLimitsOfShape, coneOfSectionCompCoyoneda_pt, coneOfSectionCompCoyoneda_π, coneOfSectionCompYoneda_pt, coneOfSectionCompYoneda_π, coyonedaFunctor_preservesLimits, coyonedaFunctor_reflectsLimits, coyonedaPreservesLimitsOfShape, coyoneda_preservesLimit, coyoneda_preservesLimits, uliftYonedaFunctor_preservesLimits, yonedaFunctor_preservesLimits, yonedaFunctor_reflectsLimits, yoneda_preservesLimit, yoneda_preservesLimits, yoneda_preservesLimitsOfShape	25
Total	34

CategoryTheory

Definitions

Name	Category	Theorems
coyonedaJointlyReflectsLimits 📖	CompOp	—
yonedaJointlyReflectsLimits 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coyonedaFunctor_preservesLimits 📖	mathematical	—	Limits.PreservesLimitsOfSize Opposite Category.opposite Functor types Functor.category coyoneda	—	Limits.preservesLimits_of_evaluation yoneda_preservesLimits
coyonedaFunctor_reflectsLimits 📖	mathematical	—	Limits.ReflectsLimitsOfSize Opposite Category.opposite Functor types Functor.category coyoneda	—	Limits.fullyFaithful_reflectsLimits Coyoneda.coyoneda_full Coyoneda.coyoneda_faithful
coyonedaPreservesLimitsOfShape 📖	mathematical	—	Limits.PreservesLimitsOfShape types Functor.obj Opposite Category.opposite Functor Functor.category coyoneda	—	coyoneda_preservesLimit
coyoneda_preservesLimit 📖	mathematical	—	Limits.PreservesLimit types Functor.obj Opposite Category.opposite Functor Functor.category coyoneda	—	Limits.Types.isLimit_iff Limits.IsLimit.fac Limits.IsLimit.uniq
coyoneda_preservesLimits 📖	mathematical	—	Limits.PreservesLimitsOfSize types Functor.obj Opposite Category.opposite Functor Functor.category coyoneda	—	coyonedaPreservesLimitsOfShape
uliftYonedaFunctor_preservesLimits 📖	mathematical	—	Limits.PreservesLimitsOfSize Functor Opposite Category.opposite types Functor.category uliftYoneda	—	Limits.preservesLimits_of_evaluation Limits.comp_preservesLimits coyoneda_preservesLimits Limits.Types.instPreservesLimitsOfSizeUliftFunctor
yonedaFunctor_preservesLimits 📖	mathematical	—	Limits.PreservesLimitsOfSize Functor Opposite Category.opposite types Functor.category yoneda	—	Limits.preservesLimits_of_evaluation coyoneda_preservesLimits
yonedaFunctor_reflectsLimits 📖	mathematical	—	Limits.ReflectsLimitsOfSize Functor Opposite Category.opposite types Functor.category yoneda	—	Limits.fullyFaithful_reflectsLimits Yoneda.yoneda_full Yoneda.yoneda_faithful
yoneda_preservesLimit 📖	mathematical	—	Limits.PreservesLimit Opposite Category.opposite types Functor.obj Functor Functor.category yoneda	—	Limits.Types.isLimit_iff Limits.IsLimit.fac Limits.IsLimit.uniq
yoneda_preservesLimits 📖	mathematical	—	Limits.PreservesLimitsOfSize Opposite Category.opposite types Functor.obj Functor Functor.category yoneda	—	yoneda_preservesLimitsOfShape
yoneda_preservesLimitsOfShape 📖	mathematical	—	Limits.PreservesLimitsOfShape Opposite Category.opposite types Functor.obj Functor Functor.category yoneda	—	yoneda_preservesLimit

CategoryTheory.Coyoneda

Definitions

Name	Category	Theorems
colimitCocone 📖	CompOp	3 math math: colimitCocone_ι_app, colimitCoconeIsColimit_desc, colimitCocone_pt
colimitCoconeIsColimit 📖	CompOp	1 math math: colimitCoconeIsColimit_desc
colimitCoyonedaIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colimitCoconeIsColimit_desc 📖	mathematical	—	CategoryTheory.Limits.IsColimit.desc CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda colimitCocone colimitCoconeIsColimit CategoryTheory.NatTrans.app CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι Opposite.unop CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
colimitCocone_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda colimitCocone	—	—
colimitCocone_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.ι colimitCocone	—	—
instHasColimitObjOppositeFunctorTypeCoyoneda 📖	mathematical	—	CategoryTheory.Limits.HasColimit CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda	—	—

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
corepresentable_preservesLimit 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit CategoryTheory.types	—	CategoryTheory.Limits.preservesLimit_of_natIso CategoryTheory.coyoneda_preservesLimit
corepresentable_preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize CategoryTheory.types	—	corepresentable_preservesLimitsOfShape
corepresentable_preservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.types	—	corepresentable_preservesLimit
representable_preservesLimit 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit Opposite CategoryTheory.Category.opposite CategoryTheory.types	—	CategoryTheory.Limits.preservesLimit_of_natIso CategoryTheory.yoneda_preservesLimit
representable_preservesLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize Opposite CategoryTheory.Category.opposite CategoryTheory.types	—	representable_preservesLimitsOfShape
representable_preservesLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape Opposite CategoryTheory.Category.opposite CategoryTheory.types	—	representable_preservesLimit

CategoryTheory.Limits

Definitions

Name	Category	Theorems
coneOfSectionCompCoyoneda 📖	CompOp	2 math math: coneOfSectionCompCoyoneda_pt, coneOfSectionCompCoyoneda_π
coneOfSectionCompYoneda 📖	CompOp	2 math math: coneOfSectionCompYoneda_pt, coneOfSectionCompYoneda_π

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coneOfSectionCompCoyoneda_pt 📖	mathematical	—	Cone.pt coneOfSectionCompCoyoneda Opposite.unop	—	—
coneOfSectionCompCoyoneda_π 📖	mathematical	—	Cone.π coneOfSectionCompCoyoneda DFunLike.coe Equiv Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda Opposite.op Opposite.unop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.const EquivLike.toFunLike Equiv.instEquivLike compCoyonedaSectionsEquiv	—	—
coneOfSectionCompYoneda_pt 📖	mathematical	—	Cone.pt Opposite CategoryTheory.Category.opposite coneOfSectionCompYoneda Opposite.op	—	—
coneOfSectionCompYoneda_π 📖	mathematical	—	Cone.π Opposite CategoryTheory.Category.opposite coneOfSectionCompYoneda DFunLike.coe Equiv Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.const Opposite.op EquivLike.toFunLike Equiv.instEquivLike compYonedaSectionsEquiv	—	—

CategoryTheory.Limits.Cocone

Definitions

Name	Category	Theorems
isColimitYonedaEquiv 📖	CompOp	—

CategoryTheory.Limits.Cone

Definitions

Name	Category	Theorems
isLimitCoyonedaEquiv 📖	CompOp	—

---

← Back to Index