Basic

📁 Source: Mathlib/CategoryTheory/Limits/ConcreteCategory/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems colimit_exists_of_rep_eq, colimit_exists_rep, colimit_rep_eq_iff_exists, colimit_rep_eq_of_exists, from_union_surjective_of_isColimit, isColimit_exists_of_rep_eq, isColimit_exists_rep, isColimit_rep_eq_iff_exists, isColimit_rep_eq_of_exists, isLimit_ext, limit_ext, small_sections_of_hasLimit, surjective_π_app_zero_of_surjective_map, to_product_injective_of_isLimit, instFullForgetTypeHom, instIsCorepresentableForgetTypeHom, instIsEquivalenceForgetTypeHom, instPreservesColimitsOfSizeForgetTypeHom, instPreservesLimitsOfSizeForgetTypeHom, instReflectsColimitsOfSizeForgetTypeHom, instReflectsLimitsOfSizeForgetTypeHom	21
Total	21

CategoryTheory.Limits.Concrete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colimit_exists_of_rep_eq 📖	mathematical	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.Limits.colimit CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.colimit.ι	CategoryTheory.Functor.map	—	isColimit_exists_of_rep_eq
colimit_exists_rep 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.Limits.colimit CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.colimit.ι	—	isColimit_exists_rep
colimit_rep_eq_iff_exists 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.Limits.colimit CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.colimit.ι CategoryTheory.Functor.map	—	colimit_exists_of_rep_eq colimit_rep_eq_of_exists
colimit_rep_eq_of_exists 📖	mathematical	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map	CategoryTheory.Limits.colimit CategoryTheory.Limits.colimit.ι	—	isColimit_rep_eq_of_exists
from_union_surjective_of_isColimit 📖	—	—	—	—	CategoryTheory.Limits.Types.jointly_surjective_of_isColimit
isColimit_exists_of_rep_eq 📖	mathematical	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	CategoryTheory.Functor.map	—	CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff CategoryTheory.IsFiltered.toIsFilteredOrEmpty
isColimit_exists_rep 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	from_union_surjective_of_isColimit
isColimit_rep_eq_iff_exists 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Functor.map	—	isColimit_exists_of_rep_eq isColimit_rep_eq_of_exists
isColimit_rep_eq_of_exists 📖	mathematical	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map	CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	CategoryTheory.NatTrans.naturality CategoryTheory.types_comp_apply
isLimit_ext 📖	—	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	—	to_product_injective_of_isLimit
limit_ext 📖	—	DFunLike.coe CategoryTheory.Limits.limit CategoryTheory.Functor.obj CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.limit.π	—	—	isLimit_ext
small_sections_of_hasLimit 📖	mathematical	—	Small Set.Elem CategoryTheory.Functor.sections CategoryTheory.Functor.comp CategoryTheory.types CategoryTheory.forget	—	CategoryTheory.Limits.Types.hasLimit_iff_small_sections CategoryTheory.Limits.instHasLimitCompOfPreservesLimit CategoryTheory.Functor.corepresentable_preservesLimit
surjective_π_app_zero_of_surjective_map 📖	mathematical	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory Nat.instPreorder Opposite.op DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.homOfLE	CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit
to_product_injective_of_isLimit 📖	mathematical	—	CategoryTheory.ToType CategoryTheory.Limits.Cone.pt DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.ConcreteCategory.hom CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	Equiv.injective

CategoryTheory.Types

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFullForgetTypeHom 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.types CategoryTheory.forget Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instFunLike instConcreteCategory	—	CategoryTheory.Functor.Full.id
instIsCorepresentableForgetTypeHom 📖	mathematical	—	CategoryTheory.Functor.IsCorepresentable CategoryTheory.types CategoryTheory.forget Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instFunLike instConcreteCategory	—	CategoryTheory.instIsCorepresentableIdType
instIsEquivalenceForgetTypeHom 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.types CategoryTheory.forget Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instFunLike instConcreteCategory	—	CategoryTheory.Functor.isEquivalence_refl
instPreservesColimitsOfSizeForgetTypeHom 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.types CategoryTheory.forget Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instFunLike instConcreteCategory	—	CategoryTheory.Limits.id_preservesColimitsOfSize
instPreservesLimitsOfSizeForgetTypeHom 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize CategoryTheory.types CategoryTheory.forget Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instFunLike instConcreteCategory	—	CategoryTheory.Limits.id_preservesLimitsOfSize
instReflectsColimitsOfSizeForgetTypeHom 📖	mathematical	—	CategoryTheory.Limits.ReflectsColimitsOfSize CategoryTheory.types CategoryTheory.forget Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instFunLike instConcreteCategory	—	CategoryTheory.Limits.id_reflectsColimits
instReflectsLimitsOfSizeForgetTypeHom 📖	mathematical	—	CategoryTheory.Limits.ReflectsLimitsOfSize CategoryTheory.types CategoryTheory.forget Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instFunLike instConcreteCategory	—	CategoryTheory.Limits.id_reflectsLimits

---

← Back to Index