AttachCells

📁 Source: Mathlib/AlgebraicTopology/RelativeCellComplex/AttachCells.lean

Statistics

Metric	Count
Definitions `AttachCells`, `cell`, `cofan₁`, `cofan₂`, `g₁`, `g₂`, `isColimit₁`, `isColimit₂`, `m`, `ofArrowIso`, `reindex`, `reindexCellTypes`, `ι`, `π`	14
Theorems `cell_def`, `cell_def_assoc`, `hm`, `hm_assoc`, `hom_ext`, `isPushout`, `ofArrowIso_cofan₁`, `ofArrowIso_cofan₂`, `ofArrowIso_g₁`, `ofArrowIso_g₂`, `ofArrowIso_isColimit₁`, `ofArrowIso_isColimit₂`, `ofArrowIso_m`, `ofArrowIso_ι`, `ofArrowIso_π`, `pushouts_coproducts`, `reindex_cofan₁`, `reindex_cofan₂`, `reindex_g₁`, `reindex_g₂`, `reindex_isColimit₁`, `reindex_isColimit₂`, `reindex_m`, `reindex_ι`, `reindex_π`, `nonempty_attachCells_iff`	26
Total	40

HomotopicalAlgebra

Definitions

Name	Category	Theorems
`AttachCells` 📖	CompData	1 math math: `nonempty_attachCells_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nonempty_attachCells_iff` 📖	mathematical	—	`AttachCells` `CategoryTheory.MorphismProperty.pushouts` `CategoryTheory.MorphismProperty.coproducts` `CategoryTheory.MorphismProperty.ofHoms`	—	`AttachCells.pushouts_coproducts` `CategoryTheory.MorphismProperty.coproducts_iff` `CategoryTheory.MorphismProperty.ofHoms_iff` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.hom_inv_id_assoc` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.IsColimit.fac` `CategoryTheory.Arrow.w_mk_right_assoc`

HomotopicalAlgebra.AttachCells

Definitions

Name	Category	Theorems
`cell` 📖	CompOp	2 math math: `cell_def`, `cell_def_assoc`
`cofan₁` 📖	CompOp	8 math math: `hm_assoc`, `reindex_cofan₁`, `ofArrowIso_cofan₁`, `isPushout`, `CategoryTheory.SmallObject.attachCellsιFunctorObj_cofan₁`, `ofArrowIso_g₁`, `reindex_isColimit₁`, `hm`
`cofan₂` 📖	CompOp	10 math math: `ofArrowIso_g₂`, `cell_def`, `hm_assoc`, `CategoryTheory.SmallObject.attachCellsιFunctorObj_cofan₂`, `reindex_cofan₂`, `cell_def_assoc`, `isPushout`, `ofArrowIso_cofan₂`, `reindex_isColimit₂`, `hm`
`g₁` 📖	CompOp	4 math math: `CategoryTheory.SmallObject.attachCellsιFunctorObj_g₁`, `isPushout`, `reindex_g₁`, `ofArrowIso_g₁`
`g₂` 📖	CompOp	6 math math: `CategoryTheory.SmallObject.attachCellsιFunctorObj_g₂`, `ofArrowIso_g₂`, `cell_def`, `cell_def_assoc`, `reindex_g₂`, `isPushout`
`isColimit₁` 📖	CompOp	3 math math: `ofArrowIso_isColimit₁`, `CategoryTheory.SmallObject.attachCellsιFunctorObj_isColimit₁`, `reindex_isColimit₁`
`isColimit₂` 📖	CompOp	3 math math: `ofArrowIso_isColimit₂`, `CategoryTheory.SmallObject.attachCellsιFunctorObj_isColimit₂`, `reindex_isColimit₂`
`m` 📖	CompOp	6 math math: `reindex_m`, `hm_assoc`, `CategoryTheory.SmallObject.attachCellsιFunctorObj_m`, `isPushout`, `ofArrowIso_m`, `hm`
`ofArrowIso` 📖	CompOp	9 math math: `ofArrowIso_isColimit₁`, `ofArrowIso_g₂`, `ofArrowIso_isColimit₂`, `ofArrowIso_π`, `ofArrowIso_cofan₁`, `ofArrowIso_cofan₂`, `ofArrowIso_g₁`, `ofArrowIso_ι`, `ofArrowIso_m`
`reindex` 📖	CompOp	9 math math: `reindex_m`, `reindex_π`, `reindex_ι`, `reindex_cofan₂`, `reindex_cofan₁`, `reindex_g₂`, `reindex_g₁`, `reindex_isColimit₂`, `reindex_isColimit₁`
`reindexCellTypes` 📖	CompOp	—
`ι` 📖	CompOp	16 math math: `ofArrowIso_g₂`, `cell_def`, `hm_assoc`, `CategoryTheory.SmallObject.instSmallιAttachCellsιFunctorObj`, `reindex_π`, `reindex_ι`, `reindex_cofan₂`, `reindex_cofan₁`, `cell_def_assoc`, `isPushout`, `CategoryTheory.SmallObject.attachCellsιFunctorObj_ι`, `reindex_isColimit₂`, `ofArrowIso_g₁`, `ofArrowIso_ι`, `reindex_isColimit₁`, `hm`
`π` 📖	CompOp	14 math math: `ofArrowIso_g₂`, `CategoryTheory.SmallObject.attachCellsιFunctorObj_π`, `cell_def`, `hm_assoc`, `reindex_π`, `ofArrowIso_π`, `reindex_cofan₂`, `reindex_cofan₁`, `cell_def_assoc`, `isPushout`, `reindex_isColimit₂`, `ofArrowIso_g₁`, `reindex_isColimit₁`, `hm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cell_def` 📖	mathematical	—	`cell` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `π` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Discrete` `ι` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `cofan₂` `g₂`	—	—
`cell_def_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `π` `cell` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Discrete` `ι` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `cofan₂` `g₂`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `cell_def`
`hm` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `π` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Discrete` `ι` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `cofan₁` `cofan₂` `m`	—	—
`hm_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `π` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Discrete` `ι` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `cofan₁` `cofan₂` `m`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `hm`
`hom_ext` 📖	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `π` `cell`	—	—	`CategoryTheory.IsPushout.hom_ext` `isPushout` `CategoryTheory.Limits.Cofan.IsColimit.hom_ext` `CategoryTheory.Category.assoc`
`isPushout` 📖	mathematical	—	`CategoryTheory.IsPushout` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Discrete` `ι` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `π` `cofan₁` `cofan₂` `g₁` `m` `g₂`	—	—
`ofArrowIso_cofan₁` 📖	mathematical	—	`cofan₁` `ofArrowIso`	—	—
`ofArrowIso_cofan₂` 📖	mathematical	—	`cofan₂` `ofArrowIso`	—	—
`ofArrowIso_g₁` 📖	mathematical	—	`g₁` `ofArrowIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Discrete` `ι` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `π` `cofan₁` `CategoryTheory.Functor.map` `CategoryTheory.Arrow` `CategoryTheory.instCategoryArrow` `CategoryTheory.Arrow.leftFunc` `CategoryTheory.Iso.hom`	—	—
`ofArrowIso_g₂` 📖	mathematical	—	`g₂` `ofArrowIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Discrete` `ι` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `π` `cofan₂` `CategoryTheory.Functor.map` `CategoryTheory.Arrow` `CategoryTheory.instCategoryArrow` `CategoryTheory.Arrow.rightFunc` `CategoryTheory.Iso.hom`	—	—
`ofArrowIso_isColimit₁` 📖	mathematical	—	`isColimit₁` `ofArrowIso`	—	—
`ofArrowIso_isColimit₂` 📖	mathematical	—	`isColimit₂` `ofArrowIso`	—	—
`ofArrowIso_m` 📖	mathematical	—	`m` `ofArrowIso`	—	—
`ofArrowIso_ι` 📖	mathematical	—	`ι` `ofArrowIso`	—	—
`ofArrowIso_π` 📖	mathematical	—	`π` `ofArrowIso`	—	—
`pushouts_coproducts` 📖	mathematical	—	`CategoryTheory.MorphismProperty.pushouts` `CategoryTheory.MorphismProperty.coproducts` `CategoryTheory.MorphismProperty.ofHoms`	—	`CategoryTheory.Limits.IsColimit.hom_ext` `CategoryTheory.Limits.IsColimit.fac` `hm` `CategoryTheory.MorphismProperty.coproducts_iff` `isPushout`
`reindex_cofan₁` 📖	mathematical	—	`cofan₁` `reindex` `π` `DFunLike.coe` `Equiv` `ι` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor`	—	—
`reindex_cofan₂` 📖	mathematical	—	`cofan₂` `reindex` `π` `DFunLike.coe` `Equiv` `ι` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor`	—	—
`reindex_g₁` 📖	mathematical	—	`g₁` `reindex`	—	—
`reindex_g₂` 📖	mathematical	—	`g₂` `reindex`	—	—
`reindex_isColimit₁` 📖	mathematical	—	`isColimit₁` `reindex` `CategoryTheory.Limits.IsColimit.whiskerEquivalence` `CategoryTheory.Discrete` `ι` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `π` `cofan₁` `CategoryTheory.Discrete.equivalence`	—	—
`reindex_isColimit₂` 📖	mathematical	—	`isColimit₂` `reindex` `CategoryTheory.Limits.IsColimit.whiskerEquivalence` `CategoryTheory.Discrete` `ι` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `π` `cofan₂` `CategoryTheory.Discrete.equivalence`	—	—
`reindex_m` 📖	mathematical	—	`m` `reindex`	—	—
`reindex_ι` 📖	mathematical	—	`ι` `reindex`	—	—
`reindex_π` 📖	mathematical	—	`π` `reindex` `DFunLike.coe` `Equiv` `ι` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	—

---

← Back to Index