Grothendieck

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/Grothendieck.lean

Statistics

Metric	Count
Definitions coconeFiberwiseColimitOfCocone, coconeOfCoconeFiberwiseColimit, colimitFiberwiseColimitIso, fiberwiseColim, fiberwiseColimCompColimIso, fiberwiseColimCompEvaluationIso, fiberwiseColimit, isColimitCoconeFiberwiseColimitOfCocone, isColimitCoconeOfFiberwiseCocone, natTransIntoForgetCompFiberwiseColimit	10
Theorems coconeFiberwiseColimitOfCocone_pt, coconeFiberwiseColimitOfCocone_ι_app, coconeOfCoconeFiberwiseColimit_pt, coconeOfCoconeFiberwiseColimit_ι_app, fiberwiseColimCompColimIso_hom_app, fiberwiseColimCompColimIso_inv_app, fiberwiseColimCompEvaluationIso_hom_app, fiberwiseColimCompEvaluationIso_inv_app, fiberwiseColim_map_app, fiberwiseColim_obj, fiberwiseColimit_map, fiberwiseColimit_obj, hasColimit_fiberwiseColimit, hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit, hasColimit_ι_comp, hasColimitsOfShape_grothendieck, natTransIntoForgetCompFiberwiseColimit_app, ι_colimitFiberwiseColimitIso_hom, ι_colimitFiberwiseColimitIso_hom_assoc, ι_colimitFiberwiseColimitIso_inv, ι_colimitFiberwiseColimitIso_inv_assoc	21
Total	31

CategoryTheory.Limits

Definitions

Name	Category	Theorems
coconeFiberwiseColimitOfCocone 📖	CompOp	2 math math: coconeFiberwiseColimitOfCocone_ι_app, coconeFiberwiseColimitOfCocone_pt
coconeOfCoconeFiberwiseColimit 📖	CompOp	2 math math: coconeOfCoconeFiberwiseColimit_pt, coconeOfCoconeFiberwiseColimit_ι_app
colimitFiberwiseColimitIso 📖	CompOp	6 math math: ι_colimitFiberwiseColimitIso_hom_assoc, ι_colimitFiberwiseColimitIso_inv_assoc, ι_colimitFiberwiseColimitIso_hom, fiberwiseColimCompColimIso_hom_app, ι_colimitFiberwiseColimitIso_inv, fiberwiseColimCompColimIso_inv_app
fiberwiseColim 📖	CompOp	8 math math: fiberwiseColimitLimitIso_hom_app, fiberwiseColim_obj, fiberwiseColim_map_app, fiberwiseColimitLimitIso_inv_app, fiberwiseColimCompEvaluationIso_hom_app, fiberwiseColimCompColimIso_hom_app, fiberwiseColimCompColimIso_inv_app, fiberwiseColimCompEvaluationIso_inv_app
fiberwiseColimCompColimIso 📖	CompOp	2 math math: fiberwiseColimCompColimIso_hom_app, fiberwiseColimCompColimIso_inv_app
fiberwiseColimCompEvaluationIso 📖	CompOp	4 math math: fiberwiseColimitLimitIso_hom_app, fiberwiseColimitLimitIso_inv_app, fiberwiseColimCompEvaluationIso_hom_app, fiberwiseColimCompEvaluationIso_inv_app
fiberwiseColimit 📖	CompOp	20 math math: fiberwiseColimit_map, fiberwiseColimit_obj, fiberwiseColimitLimitIso_hom_app, coconeOfCoconeFiberwiseColimit_pt, fiberwiseColim_obj, ι_colimitFiberwiseColimitIso_hom_assoc, ι_colimitFiberwiseColimitIso_inv_assoc, fiberwiseColim_map_app, fiberwiseColimitLimitIso_inv_app, natTransIntoForgetCompFiberwiseColimit_app, coconeFiberwiseColimitOfCocone_ι_app, hasColimit_fiberwiseColimit, coconeFiberwiseColimitOfCocone_pt, ι_colimitFiberwiseColimitIso_hom, fiberwiseColimCompColimIso_hom_app, CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_hom_app, ι_colimitFiberwiseColimitIso_inv, fiberwiseColimCompColimIso_inv_app, coconeOfCoconeFiberwiseColimit_ι_app, CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_inv_app
isColimitCoconeFiberwiseColimitOfCocone 📖	CompOp	—
isColimitCoconeOfFiberwiseCocone 📖	CompOp	—
natTransIntoForgetCompFiberwiseColimit 📖	CompOp	1 math math: natTransIntoForgetCompFiberwiseColimit_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coconeFiberwiseColimitOfCocone_pt 📖	mathematical	HasColimit CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι	Cocone.pt fiberwiseColimit coconeFiberwiseColimitOfCocone CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory	—	—
coconeFiberwiseColimitOfCocone_ι_app 📖	mathematical	HasColimit CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι	CategoryTheory.NatTrans.app fiberwiseColimit CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const Cocone.pt CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory Cocone.ι coconeFiberwiseColimitOfCocone colimit.desc CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Grothendieck.ι hasColimit_ι_comp Cocone.whisker	—	hasColimit_ι_comp
coconeOfCoconeFiberwiseColimit_pt 📖	mathematical	HasColimit CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι	Cocone.pt CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory coconeOfCoconeFiberwiseColimit fiberwiseColimit	—	—
coconeOfCoconeFiberwiseColimit_ι_app 📖	mathematical	HasColimit CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι	CategoryTheory.NatTrans.app CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const Cocone.pt fiberwiseColimit Cocone.ι coconeOfCoconeFiberwiseColimit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct colimit CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Grothendieck.base CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Grothendieck.ι colimit.ι CategoryTheory.Grothendieck.fiber	—	—
fiberwiseColimCompColimIso_hom_app 📖	mathematical	HasColimitsOfShape CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp fiberwiseColim colim hasColimitsOfShape_grothendieck CategoryTheory.Iso.hom fiberwiseColimCompColimIso colimit fiberwiseColimit hasColimitOfHasColimitsOfShape colimitFiberwiseColimitIso	—	hasColimitsOfShape_grothendieck
fiberwiseColimCompColimIso_inv_app 📖	mathematical	HasColimitsOfShape CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Functor.category colim hasColimitsOfShape_grothendieck CategoryTheory.Functor.comp fiberwiseColim CategoryTheory.Iso.inv fiberwiseColimCompColimIso colimit fiberwiseColimit hasColimitOfHasColimitsOfShape colimitFiberwiseColimitIso	—	hasColimitsOfShape_grothendieck
fiberwiseColimCompEvaluationIso_hom_app 📖	mathematical	HasColimitsOfShape CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp fiberwiseColim CategoryTheory.Functor.obj CategoryTheory.evaluation CategoryTheory.Iso.hom CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.whiskeringLeft CategoryTheory.Grothendieck.ι colim fiberwiseColimCompEvaluationIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct colimit hasColimit_ι_comp	—	—
fiberwiseColimCompEvaluationIso_inv_app 📖	mathematical	HasColimitsOfShape CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp fiberwiseColim CategoryTheory.Functor.obj CategoryTheory.evaluation CategoryTheory.Iso.inv CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.whiskeringLeft CategoryTheory.Grothendieck.ι colim fiberwiseColimCompEvaluationIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct colimit hasColimit_ι_comp	—	—
fiberwiseColim_map_app 📖	mathematical	HasColimitsOfShape CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str	CategoryTheory.NatTrans.app fiberwiseColimit CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Functor.category fiberwiseColim CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str colim CategoryTheory.Functor.comp CategoryTheory.Grothendieck.ι CategoryTheory.Functor.whiskerLeft	—	—
fiberwiseColim_obj 📖	mathematical	HasColimitsOfShape CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str	CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Functor.category fiberwiseColim fiberwiseColimit	—	—
fiberwiseColimit_map 📖	mathematical	HasColimit CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι	CategoryTheory.Functor.map fiberwiseColimit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct colimit CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι hasColimit_ι_comp CategoryTheory.Cat.Hom.toFunctor colimMap CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.whiskerRight CategoryTheory.Grothendieck.ιNatTrans CategoryTheory.Iso.hom CategoryTheory.Functor.associator colimit.pre	—	hasColimit_ι_comp
fiberwiseColimit_obj 📖	mathematical	HasColimit CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι	CategoryTheory.Functor.obj fiberwiseColimit colimit CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι hasColimit_ι_comp	—	—
hasColimit_fiberwiseColimit 📖	mathematical	HasColimit CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι	HasColimit fiberwiseColimit	—	—
hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit 📖	mathematical	HasColimit CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι	HasColimit CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory	—	—
hasColimit_ι_comp 📖	mathematical	HasColimit CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι	HasColimit CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι	—	hasColimit_of_iso CategoryTheory.Functor.map_id
hasColimitsOfShape_grothendieck 📖	mathematical	HasColimitsOfShape CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str	HasColimitsOfShape CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory	—	hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit hasColimitOfHasColimitsOfShape
natTransIntoForgetCompFiberwiseColimit_app 📖	mathematical	HasColimit CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι	CategoryTheory.NatTrans.app CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Functor.comp CategoryTheory.Grothendieck.forget fiberwiseColimit natTransIntoForgetCompFiberwiseColimit colimit.ι CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Grothendieck.base CategoryTheory.Cat.str CategoryTheory.Grothendieck.ι CategoryTheory.Grothendieck.fiber	—	—
ι_colimitFiberwiseColimitIso_hom 📖	mathematical	HasColimit CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι colimit hasColimit_ι_comp hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit colimit.ι fiberwiseColimit CategoryTheory.Iso.hom colimitFiberwiseColimitIso	—	hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit hasColimit_ι_comp colimit.comp_coconePointUniqueUpToIso_hom colimit.ι_desc
ι_colimitFiberwiseColimitIso_hom_assoc 📖	mathematical	HasColimit CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Grothendieck.ι colimit CategoryTheory.Functor.comp hasColimit_ι_comp colimit.ι fiberwiseColimit hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit CategoryTheory.Iso.hom colimitFiberwiseColimitIso	—	hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit hasColimit_ι_comp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_colimitFiberwiseColimitIso_hom
ι_colimitFiberwiseColimitIso_inv 📖	mathematical	HasColimit CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory colimit hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit fiberwiseColimit colimit.ι CategoryTheory.Iso.inv colimitFiberwiseColimitIso CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Grothendieck.base CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Grothendieck.ι CategoryTheory.Grothendieck.fiber hasColimit_ι_comp	—	hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit hasColimit_ι_comp CategoryTheory.Iso.comp_inv_eq CategoryTheory.Category.assoc ι_colimitFiberwiseColimitIso_hom
ι_colimitFiberwiseColimitIso_inv_assoc 📖	mathematical	HasColimit CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Functor.obj CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Functor.map CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory CategoryTheory.Grothendieck.ι	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Grothendieck CategoryTheory.Grothendieck.instCategory colimit hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit colimit.ι fiberwiseColimit CategoryTheory.Iso.inv colimitFiberwiseColimitIso CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Grothendieck.base CategoryTheory.Cat.str CategoryTheory.Functor.comp CategoryTheory.Grothendieck.ι hasColimit_ι_comp CategoryTheory.Grothendieck.fiber	—	hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit hasColimit_ι_comp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_colimitFiberwiseColimitIso_inv

---

← Back to Index