ColimitLimit

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

Statistics

Metric	Count
Definitions colimitLimitToLimitColimit, colimitLimitToLimitColimitCone	2
Theorems colimitLimitToLimitColimitCone_hom, map_id_left_eq_curry_map, map_id_right_eq_curry_swap_map, ι_colimitLimitToLimitColimit_π, ι_colimitLimitToLimitColimit_π_apply, ι_colimitLimitToLimitColimit_π_assoc	6
Total	8

CategoryTheory.Limits

Definitions

Name	Category	Theorems
colimitLimitToLimitColimit 📖	CompOp	7 math math: colimitLimitToLimitColimit_isIso, ι_colimitLimitToLimitColimit_π, colimitLimitToLimitColimitCone_hom, ι_colimitLimitToLimitColimit_π_apply, ι_colimitLimitToLimitColimit_π_assoc, colimitLimitToLimitColimit_injective, colimitLimitToLimitColimit_surjective
colimitLimitToLimitColimitCone 📖	CompOp	2 math math: colimitLimitToLimitColimitCone_hom, colimitLimitToLimitColimitCone_iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colimitLimitToLimitColimitCone_hom 📖	mathematical	—	ConeMorphism.hom CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category colim CategoryTheory.Functor.mapCone limit.cone hasLimitOfHasLimitsOfShape colimitLimitToLimitColimitCone CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Cone.pt CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.Functor.curry CategoryTheory.Prod.swap CategoryTheory.Functor.uncurry lim CategoryTheory.Functor.map CategoryTheory.Iso.hom limit limitIsoSwapCompLim colimitLimitToLimitColimit CategoryTheory.Functor.whiskerRight CategoryTheory.Equivalence.functor CategoryTheory.Functor.currying CategoryTheory.Equivalence.inverse CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Iso.app CategoryTheory.Equivalence.unitIso	—	hasLimitOfHasLimitsOfShape
map_id_left_eq_curry_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.prod' CategoryTheory.Prod.mkHom CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.curry	—	—
map_id_right_eq_curry_swap_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.prod' CategoryTheory.Prod.mkHom CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.curry CategoryTheory.Functor.comp CategoryTheory.Prod.swap	—	—
ι_colimitLimitToLimitColimit_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.prod' CategoryTheory.Functor.curry CategoryTheory.Prod.swap lim colimit hasColimitOfHasColimitsOfShape colim colimit.ι limit hasLimitOfHasLimitsOfShape colimitLimitToLimitColimit limit.π	—	hasColimitOfHasColimitsOfShape hasLimitOfHasLimitsOfShape limit.lift_π colimit.ι_desc
ι_colimitLimitToLimitColimit_π_apply 📖	mathematical	—	limit.π CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.Functor.curry colim Types.hasColimitsOfShape hasLimitOfHasLimitsOfShape Types.hasLimitsOfShape colimitLimitToLimitColimit colimit.ι CategoryTheory.Prod.swap lim Types.hasColimit Types.hasLimit	—	Types.hasLimitsOfShape Types.hasColimitsOfShape hasLimitOfHasLimitsOfShape Types.hasColimit Types.hasLimit hasColimitOfHasColimitsOfShape Types.Limit.lift_π_apply Types.Colimit.ι_desc_apply
ι_colimitLimitToLimitColimit_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category lim CategoryTheory.prod' CategoryTheory.Functor.curry CategoryTheory.Functor.comp CategoryTheory.Prod.swap colimit hasColimitOfHasColimitsOfShape colimit.ι limit colim hasLimitOfHasLimitsOfShape colimitLimitToLimitColimit limit.π	—	hasColimitOfHasColimitsOfShape hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_colimitLimitToLimitColimit_π

---

← Back to Index