Construction

📁 Source: Mathlib/CategoryTheory/SmallObject/Construction.lean

Statistics

Metric	Count
Definitions FunctorObjIndex, b, i, t, attachCellsιFunctorObj, attachCellsιFunctorObjOfSmall, functor, functorMap, functorMapSrc, functorMapTgt, functorObj, functorObjLeft, functorObjLeftFamily, functorObjSrcFamily, functorObjTgtFamily, functorObjTop, ε, ιFunctorObj, π'FunctorObj, πFunctorObj, ρFunctorObj	21
Theorems comm, comm_assoc, w, w_assoc, attachCellsιFunctorObj_cofan₁, attachCellsιFunctorObj_cofan₂, attachCellsιFunctorObj_g₁, attachCellsιFunctorObj_g₂, attachCellsιFunctorObj_isColimit₁, attachCellsιFunctorObj_isColimit₂, attachCellsιFunctorObj_m, attachCellsιFunctorObj_ι, attachCellsιFunctorObj_π, functorMapSrc_functorObjTop, functorMapSrc_functorObjTop_assoc, functorMap_comm, functorMap_id, functorMap_π, functorMap_π_assoc, functorObj_comm, functorObj_comm_assoc, functorObj_isPushout, functor_map, functor_obj, instSmallFunctorObjIndex, instSmallιAttachCellsιFunctorObj, ε_app, ιFunctorObj_extension, ιFunctorObj_extension', ιFunctorObj_naturality, ιFunctorObj_naturality_assoc, ιFunctorObj_πFunctorObj, ιFunctorObj_πFunctorObj_assoc, ι_functorMapSrc, ι_functorMapSrc_assoc, ι_functorMapTgt, ι_functorMapTgt_assoc, ρFunctorObj_π, ρFunctorObj_π_assoc	39
Total	60

CategoryTheory.SmallObject

Definitions

Name	Category	Theorems
FunctorObjIndex 📖	CompData	23 math math: ρFunctorObj_π_assoc, ι_functorMapSrc, FunctorObjIndex.comm, attachCellsιFunctorObj_cofan₂, functorMapSrc_functorObjTop, functorObj_comm, ιFunctorObj_eq, ι_functorMapSrc_assoc, ι_functorMapTgt, ρFunctorObj_π, functorMap_comm, functorMapSrc_functorObjTop_assoc, attachCellsιFunctorObj_isColimit₁, instSmallFunctorObjIndex, πFunctorObj_eq, functorObj_comm_assoc, attachCellsιFunctorObj_ι, FunctorObjIndex.comm_assoc, attachCellsιFunctorObj_isColimit₂, functorObj_isPushout, attachCellsιFunctorObj_cofan₁, hasColimitsOfShape_discrete, ι_functorMapTgt_assoc
attachCellsιFunctorObj 📖	CompOp	10 math math: attachCellsιFunctorObj_g₂, attachCellsιFunctorObj_π, attachCellsιFunctorObj_m, attachCellsιFunctorObj_g₁, attachCellsιFunctorObj_cofan₂, instSmallιAttachCellsιFunctorObj, attachCellsιFunctorObj_isColimit₁, attachCellsιFunctorObj_ι, attachCellsιFunctorObj_isColimit₂, attachCellsιFunctorObj_cofan₁
attachCellsιFunctorObjOfSmall 📖	CompOp	—
functor 📖	CompOp	6 math math: functor_map, ε_app, iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc, iterationFunctorMapSuccAppArrowIso_hom_left, functor_obj, iterationFunctorMapSuccAppArrowIso_hom_right_right_comp
functorMap 📖	CompOp	6 math math: functorMap_id, functor_map, ιFunctorObj_naturality, functorMap_π_assoc, functorMap_π, ιFunctorObj_naturality_assoc
functorMapSrc 📖	CompOp	5 math math: ι_functorMapSrc, functorMapSrc_functorObjTop, ι_functorMapSrc_assoc, functorMap_comm, functorMapSrc_functorObjTop_assoc
functorMapTgt 📖	CompOp	3 math math: ι_functorMapTgt, functorMap_comm, ι_functorMapTgt_assoc
functorObj 📖	CompOp	29 math math: functorMap_id, ρFunctorObj_π_assoc, attachCellsιFunctorObj_g₂, attachCellsιFunctorObj_π, FunctorObjIndex.comm, functor_map, attachCellsιFunctorObj_m, attachCellsιFunctorObj_g₁, attachCellsιFunctorObj_cofan₂, ιFunctorObj_naturality, instSmallιAttachCellsιFunctorObj, ιFunctorObj_πFunctorObj_assoc, functorObj_comm, functorMap_π_assoc, ιFunctorObj_eq, ρFunctorObj_π, attachCellsιFunctorObj_isColimit₁, πFunctorObj_eq, functorMap_π, ιFunctorObj_naturality_assoc, functorObj_comm_assoc, functor_obj, attachCellsιFunctorObj_ι, FunctorObjIndex.comm_assoc, ιFunctorObj_πFunctorObj, attachCellsιFunctorObj_isColimit₂, ιFunctorObj_extension, functorObj_isPushout, attachCellsιFunctorObj_cofan₁
functorObjLeft 📖	CompOp	7 math math: attachCellsιFunctorObj_m, functorObj_comm, ιFunctorObj_eq, functorMap_comm, πFunctorObj_eq, functorObj_comm_assoc, functorObj_isPushout
functorObjLeftFamily 📖	CompOp	—
functorObjSrcFamily 📖	CompOp	10 math math: ι_functorMapSrc, functorMapSrc_functorObjTop, functorObj_comm, ιFunctorObj_eq, ι_functorMapSrc_assoc, functorMap_comm, functorMapSrc_functorObjTop_assoc, πFunctorObj_eq, functorObj_comm_assoc, functorObj_isPushout
functorObjTgtFamily 📖	CompOp	12 math math: ρFunctorObj_π_assoc, FunctorObjIndex.comm, functorObj_comm, ιFunctorObj_eq, ι_functorMapTgt, ρFunctorObj_π, functorMap_comm, πFunctorObj_eq, functorObj_comm_assoc, FunctorObjIndex.comm_assoc, functorObj_isPushout, ι_functorMapTgt_assoc
functorObjTop 📖	CompOp	8 math math: attachCellsιFunctorObj_g₁, functorMapSrc_functorObjTop, functorObj_comm, ιFunctorObj_eq, functorMapSrc_functorObjTop_assoc, πFunctorObj_eq, functorObj_comm_assoc, functorObj_isPushout
ε 📖	CompOp	4 math math: ε_app, iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc, iterationFunctorMapSuccAppArrowIso_hom_left, iterationFunctorMapSuccAppArrowIso_hom_right_right_comp
ιFunctorObj 📖	CompOp	22 math math: attachCellsιFunctorObj_g₂, attachCellsιFunctorObj_π, FunctorObjIndex.comm, attachCellsιFunctorObj_m, ε_app, attachCellsιFunctorObj_g₁, attachCellsιFunctorObj_cofan₂, ιFunctorObj_naturality, instSmallιAttachCellsιFunctorObj, ιFunctorObj_πFunctorObj_assoc, functorObj_comm, ιFunctorObj_eq, attachCellsιFunctorObj_isColimit₁, ιFunctorObj_naturality_assoc, functorObj_comm_assoc, attachCellsιFunctorObj_ι, FunctorObjIndex.comm_assoc, ιFunctorObj_πFunctorObj, attachCellsιFunctorObj_isColimit₂, ιFunctorObj_extension, functorObj_isPushout, attachCellsιFunctorObj_cofan₁
π'FunctorObj 📖	CompOp	2 math math: ρFunctorObj_π_assoc, ρFunctorObj_π
πFunctorObj 📖	CompOp	10 math math: ρFunctorObj_π_assoc, functor_map, ιFunctorObj_πFunctorObj_assoc, functorMap_π_assoc, ρFunctorObj_π, πFunctorObj_eq, functorMap_π, functor_obj, ιFunctorObj_πFunctorObj, ιFunctorObj_extension
ρFunctorObj 📖	CompOp	8 math math: ρFunctorObj_π_assoc, attachCellsιFunctorObj_g₂, FunctorObjIndex.comm, functorObj_comm, ρFunctorObj_π, functorObj_comm_assoc, FunctorObjIndex.comm_assoc, functorObj_isPushout

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
attachCellsιFunctorObj_cofan₁ 📖	mathematical	—	HomotopicalAlgebra.AttachCells.cofan₁ functorObj ιFunctorObj attachCellsιFunctorObj FunctorObjIndex FunctorObjIndex.i CategoryTheory.Limits.sigmaObj CategoryTheory.Limits.Sigma.ι	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
attachCellsιFunctorObj_cofan₂ 📖	mathematical	—	HomotopicalAlgebra.AttachCells.cofan₂ functorObj ιFunctorObj attachCellsιFunctorObj FunctorObjIndex FunctorObjIndex.i CategoryTheory.Limits.sigmaObj CategoryTheory.Limits.Sigma.ι	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
attachCellsιFunctorObj_g₁ 📖	mathematical	—	HomotopicalAlgebra.AttachCells.g₁ functorObj ιFunctorObj attachCellsιFunctorObj functorObjTop	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
attachCellsιFunctorObj_g₂ 📖	mathematical	—	HomotopicalAlgebra.AttachCells.g₂ functorObj ιFunctorObj attachCellsιFunctorObj ρFunctorObj	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
attachCellsιFunctorObj_isColimit₁ 📖	mathematical	—	HomotopicalAlgebra.AttachCells.isColimit₁ functorObj ιFunctorObj attachCellsιFunctorObj CategoryTheory.Limits.coproductIsCoproduct FunctorObjIndex FunctorObjIndex.i	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
attachCellsιFunctorObj_isColimit₂ 📖	mathematical	—	HomotopicalAlgebra.AttachCells.isColimit₂ functorObj ιFunctorObj attachCellsιFunctorObj CategoryTheory.Limits.coproductIsCoproduct FunctorObjIndex FunctorObjIndex.i	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
attachCellsιFunctorObj_m 📖	mathematical	—	HomotopicalAlgebra.AttachCells.m functorObj ιFunctorObj attachCellsιFunctorObj functorObjLeft	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
attachCellsιFunctorObj_ι 📖	mathematical	—	HomotopicalAlgebra.AttachCells.ι functorObj ιFunctorObj attachCellsιFunctorObj FunctorObjIndex	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
attachCellsιFunctorObj_π 📖	mathematical	—	HomotopicalAlgebra.AttachCells.π functorObj ιFunctorObj attachCellsιFunctorObj FunctorObjIndex.i	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
functorMapSrc_functorObjTop 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.sigmaObj FunctorObjIndex functorObjSrcFamily CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor functorMapSrc functorObjTop CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.CommaMorphism.left	—	CategoryTheory.Limits.Sigma.hom_ext CategoryTheory.Limits.hasColimitOfHasColimitsOfShape ι_functorMapSrc_assoc CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Limits.colimit.ι_desc_assoc
functorMapSrc_functorObjTop_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.sigmaObj FunctorObjIndex functorObjSrcFamily CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor functorMapSrc functorObjTop CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' functorMapSrc_functorObjTop
functorMap_comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.sigmaObj FunctorObjIndex functorObjSrcFamily CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor functorObjTgtFamily functorObjLeft functorMapTgt functorMapSrc	—	CategoryTheory.Limits.Sigma.hom_ext CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.ι_colimMap_assoc ι_functorMapTgt ι_functorMapSrc_assoc CategoryTheory.Limits.ι_colimMap
functorMap_id 📖	mathematical	—	functorMap CategoryTheory.CategoryStruct.id CategoryTheory.Arrow CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryArrow functorObj	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.pushout.hom_ext functorMap_comm CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.Limits.Sigma.hom_ext ι_functorMapTgt_assoc
functorMap_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct functorObj functorMap πFunctorObj CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.pushout.hom_ext functorMap_comm CategoryTheory.Limits.colimit.ι_desc_assoc CategoryTheory.Category.assoc ιFunctorObj_πFunctorObj CategoryTheory.Arrow.w_mk_right ιFunctorObj_πFunctorObj_assoc CategoryTheory.Limits.Sigma.hom_ext ρFunctorObj_π ι_functorMapTgt_assoc CategoryTheory.Limits.colimit.ι_desc ρFunctorObj_π_assoc
functorMap_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct functorObj functorMap πFunctorObj CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' functorMap_π
functorObj_comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.sigmaObj FunctorObjIndex functorObjSrcFamily CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor functorObj functorObjTop ιFunctorObj functorObjTgtFamily functorObjLeft ρFunctorObj	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.pushout.condition
functorObj_comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.sigmaObj FunctorObjIndex functorObjSrcFamily CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor functorObjTop functorObj ιFunctorObj functorObjTgtFamily functorObjLeft ρFunctorObj	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' functorObj_comm
functorObj_isPushout 📖	mathematical	—	CategoryTheory.IsPushout CategoryTheory.Limits.sigmaObj FunctorObjIndex functorObjSrcFamily CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor functorObjTgtFamily functorObj functorObjTop functorObjLeft ιFunctorObj ρFunctorObj	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.IsPushout.of_hasPushout
functor_map 📖	mathematical	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Discrete FunctorObjIndex CategoryTheory.discreteCategory	CategoryTheory.Functor.map CategoryTheory.Arrow CategoryTheory.instCategoryArrow functor CategoryTheory.Arrow.homMk functorObj CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom πFunctorObj functorMap CategoryTheory.CommaMorphism.right	—	—
functor_obj 📖	mathematical	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Discrete FunctorObjIndex CategoryTheory.discreteCategory	CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow functor functorObj CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom πFunctorObj	—	—
instSmallFunctorObjIndex 📖	mathematical	—	Small FunctorObjIndex	—	small_prod CategoryTheory.instSmallHomOfLocallySmall Equiv.symm_apply_apply EquivLike.toEmbeddingLike CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.instIsIsoEqToHom small_of_injective small_sigma UnivLE.small UnivLE.self
instSmallιAttachCellsιFunctorObj 📖	mathematical	—	Small HomotopicalAlgebra.AttachCells.ι functorObj ιFunctorObj attachCellsιFunctorObj	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instSmallFunctorObjIndex
ε_app 📖	mathematical	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Discrete FunctorObjIndex CategoryTheory.discreteCategory	CategoryTheory.NatTrans.app CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.id functor ε CategoryTheory.Arrow.homMk CategoryTheory.Functor.obj ιFunctorObj CategoryTheory.Comma.right CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
ιFunctorObj_extension 📖	mathematical	CategoryTheory.CommSq	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct functorObj ιFunctorObj πFunctorObj	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.CommSq.w FunctorObjIndex.comm CategoryTheory.Category.assoc ρFunctorObj_π CategoryTheory.Limits.colimit.ι_desc
ιFunctorObj_extension' 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct functorObj CategoryTheory.Iso.hom ιFunctorObj πFunctorObj	—	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape ιFunctorObj_extension CategoryTheory.Category.assoc ιFunctorObj_πFunctorObj Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.inv_hom_id_assoc
ιFunctorObj_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct functorObj ιFunctorObj functorMap CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.CommaMorphism.left	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.colimit.ι_desc functorMap_comm
ιFunctorObj_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct functorObj ιFunctorObj functorMap CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.CommaMorphism.left	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιFunctorObj_naturality
ιFunctorObj_πFunctorObj 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct functorObj ιFunctorObj πFunctorObj	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.colimit.ι_desc
ιFunctorObj_πFunctorObj_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct functorObj ιFunctorObj πFunctorObj	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιFunctorObj_πFunctorObj
ι_functorMapSrc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right CategoryTheory.Comma.left CategoryTheory.CommaMorphism.left	functorObjSrcFamily CategoryTheory.Limits.sigmaObj FunctorObjIndex CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.Limits.Sigma.ι functorMapSrc	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.Sigma.ι_comp_map' CategoryTheory.Category.id_comp
ι_functorMapSrc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right CategoryTheory.Comma.left CategoryTheory.CommaMorphism.left	functorObjSrcFamily CategoryTheory.Limits.sigmaObj FunctorObjIndex CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.Limits.Sigma.ι functorMapSrc	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_functorMapSrc
ι_functorMapTgt 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right CategoryTheory.Comma.left CategoryTheory.CommaMorphism.left	functorObjTgtFamily CategoryTheory.Limits.sigmaObj FunctorObjIndex CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.Limits.Sigma.ι functorMapTgt	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.Sigma.ι_comp_map' CategoryTheory.Category.id_comp
ι_functorMapTgt_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right CategoryTheory.Comma.left CategoryTheory.CommaMorphism.left	functorObjTgtFamily CategoryTheory.Limits.sigmaObj FunctorObjIndex CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.Limits.Sigma.ι functorMapTgt	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_functorMapTgt
ρFunctorObj_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.sigmaObj FunctorObjIndex functorObjTgtFamily CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor functorObj ρFunctorObj πFunctorObj π'FunctorObj	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.colimit.ι_desc
ρFunctorObj_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.sigmaObj FunctorObjIndex functorObjTgtFamily CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor functorObj ρFunctorObj πFunctorObj π'FunctorObj	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ρFunctorObj_π

CategoryTheory.SmallObject.FunctorObjIndex

Definitions

Name	Category	Theorems
b 📖	CompOp	2 math math: w_assoc, w
i 📖	CompOp	9 math math: CategoryTheory.SmallObject.attachCellsιFunctorObj_π, comm, CategoryTheory.SmallObject.attachCellsιFunctorObj_cofan₂, w_assoc, CategoryTheory.SmallObject.attachCellsιFunctorObj_isColimit₁, comm_assoc, w, CategoryTheory.SmallObject.attachCellsιFunctorObj_isColimit₂, CategoryTheory.SmallObject.attachCellsιFunctorObj_cofan₁
t 📖	CompOp	4 math math: comm, w_assoc, comm_assoc, w

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct i CategoryTheory.SmallObject.functorObj CategoryTheory.Limits.sigmaObj CategoryTheory.SmallObject.FunctorObjIndex CategoryTheory.SmallObject.functorObjTgtFamily CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.Limits.Sigma.ι CategoryTheory.SmallObject.ρFunctorObj t CategoryTheory.SmallObject.ιFunctorObj	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.Sigma.ι_map_assoc CategoryTheory.Limits.colimit.ι_desc_assoc CategoryTheory.whisker_eq CategoryTheory.SmallObject.functorObj_comm
comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct i CategoryTheory.Limits.sigmaObj CategoryTheory.SmallObject.FunctorObjIndex CategoryTheory.SmallObject.functorObjTgtFamily CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor CategoryTheory.Limits.Sigma.ι CategoryTheory.SmallObject.functorObj CategoryTheory.SmallObject.ρFunctorObj t CategoryTheory.SmallObject.ιFunctorObj	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm
w 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct i t b	—	—
w_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct i t b	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' w

---

← Back to Index