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	—	—
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 CategoryTheory.Functor.category CategoryTheory.Functor.const Cocone.pt Cocone.ι coconeFiberwiseColimitOfCocone colimit.desc 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 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.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const Cocone.pt fiberwiseColimit Cocone.ι coconeOfCoconeFiberwiseColimit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct colimit CategoryTheory.Grothendieck.base 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.evaluation CategoryTheory.Iso.hom 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.evaluation CategoryTheory.Iso.inv 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 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 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.ι	fiberwiseColimit CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct colimit hasColimit_ι_comp 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.ι	fiberwiseColimit colimit 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.ι	fiberwiseColimit	—	—
hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit 📖	—	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_ι_comp 📖	—	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_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	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.forget fiberwiseColimit natTransIntoForgetCompFiberwiseColimit colimit.ι CategoryTheory.Grothendieck.base 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 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 colimit 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 colimit hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit fiberwiseColimit colimit.ι CategoryTheory.Iso.inv colimitFiberwiseColimitIso CategoryTheory.Grothendieck.base 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 colimit hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit colimit.ι fiberwiseColimit CategoryTheory.Iso.inv colimitFiberwiseColimitIso CategoryTheory.Grothendieck.base 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