Documentation Verification Report

Factorisation

📁 Source: Mathlib/CategoryTheory/Category/Factorisation.lean

Statistics

Metric	Count
Definitions `Factorisation`, `h`, `IsInitial_initial`, `IsTerminal_terminal`, `forget`, `initial`, `initialHom`, `instCategory`, `instQuiver`, `instUniqueHomInitial`, `instUniqueHomTerminal`, `mid`, `terminal`, `terminalHom`, `ι`, `π`	16
Theorems `ext`, `ext_iff`, `h_π`, `h_π_assoc`, `ι_h`, `ι_h_assoc`, `comp_h`, `comp_h_assoc`, `forget_map`, `forget_obj`, `id_h`, `initialHom_h`, `initial_mid`, `initial_ι`, `initial_π`, `instHasInitial`, `instHasTerminal`, `terminalHom_h`, `terminal_mid`, `terminal_ι`, `terminal_π`, `ι_π`, `ι_π_assoc`	23
Total	39

CategoryTheory

Definitions

Name	Category	Theorems
`Factorisation` 📖	CompData	8 math math: `Factorisation.id_h`, `Factorisation.forget_map`, `Factorisation.comp_h`, `Factorisation.forget_obj`, `Factorisation.instHasInitial`, `CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step`, `Factorisation.comp_h_assoc`, `Factorisation.instHasTerminal`

CategoryTheory.Factorisation

Definitions

Name	Category	Theorems
`IsInitial_initial` 📖	CompOp	—
`IsTerminal_terminal` 📖	CompOp	—
`forget` 📖	CompOp	2 math math: `forget_map`, `forget_obj`
`initial` 📖	CompOp	4 math math: `initial_π`, `initial_ι`, `initial_mid`, `initialHom_h`
`initialHom` 📖	CompOp	1 math math: `initialHom_h`
`instCategory` 📖	CompOp	8 math math: `id_h`, `forget_map`, `comp_h`, `forget_obj`, `instHasInitial`, `CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step`, `comp_h_assoc`, `instHasTerminal`
`instQuiver` 📖	CompOp	—
`instUniqueHomInitial` 📖	CompOp	—
`instUniqueHomTerminal` 📖	CompOp	—
`mid` 📖	CompOp	12 math math: `id_h`, `comp_h`, `forget_obj`, `Hom.ι_h_assoc`, `comp_h_assoc`, `Hom.h_π_assoc`, `Hom.ι_h`, `initial_mid`, `Hom.h_π`, `ι_π`, `ι_π_assoc`, `terminal_mid`
`terminal` 📖	CompOp	4 math math: `terminalHom_h`, `terminal_π`, `terminal_ι`, `terminal_mid`
`terminalHom` 📖	CompOp	1 math math: `terminalHom_h`
`ι` 📖	CompOp	7 math math: `Hom.ι_h_assoc`, `initial_ι`, `Hom.ι_h`, `terminal_ι`, `ι_π`, `ι_π_assoc`, `initialHom_h`
`π` 📖	CompOp	7 math math: `terminalHom_h`, `initial_π`, `Hom.h_π_assoc`, `terminal_π`, `Hom.h_π`, `ι_π`, `ι_π_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_h` 📖	mathematical	—	`Hom.h` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Factorisation` `CategoryTheory.Category.toCategoryStruct` `instCategory` `mid`	—	—
`comp_h_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `mid` `Hom.h` `CategoryTheory.Factorisation` `instCategory`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_h`
`forget_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Factorisation` `instCategory` `forget` `Hom.h`	—	—
`forget_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Factorisation` `instCategory` `forget` `mid`	—	—
`id_h` 📖	mathematical	—	`Hom.h` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Factorisation` `CategoryTheory.Category.toCategoryStruct` `instCategory` `mid`	—	—
`initialHom_h` 📖	mathematical	—	`Hom.h` `initial` `initialHom` `ι`	—	—
`initial_mid` 📖	mathematical	—	`mid` `initial`	—	—
`initial_ι` 📖	mathematical	—	`ι` `initial` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`initial_π` 📖	mathematical	—	`π` `initial`	—	—
`instHasInitial` 📖	mathematical	—	`CategoryTheory.Limits.HasInitial` `CategoryTheory.Factorisation` `instCategory`	—	`CategoryTheory.Limits.hasInitial_of_unique` `Unique.instSubsingleton`
`instHasTerminal` 📖	mathematical	—	`CategoryTheory.Limits.HasTerminal` `CategoryTheory.Factorisation` `instCategory`	—	`CategoryTheory.Limits.hasTerminal_of_unique` `Unique.instSubsingleton`
`terminalHom_h` 📖	mathematical	—	`Hom.h` `terminal` `terminalHom` `π`	—	—
`terminal_mid` 📖	mathematical	—	`mid` `terminal`	—	—
`terminal_ι` 📖	mathematical	—	`ι` `terminal`	—	—
`terminal_π` 📖	mathematical	—	`π` `terminal` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`ι_π` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `mid` `ι` `π`	—	—
`ι_π_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `mid` `ι` `π`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι_π`

CategoryTheory.Factorisation.Hom

Definitions

Name	Category	Theorems
`h` 📖	CompOp	11 math math: `CategoryTheory.Factorisation.id_h`, `CategoryTheory.Factorisation.forget_map`, `CategoryTheory.Factorisation.comp_h`, `ι_h_assoc`, `CategoryTheory.Factorisation.terminalHom_h`, `CategoryTheory.Factorisation.comp_h_assoc`, `h_π_assoc`, `ι_h`, `ext_iff`, `h_π`, `CategoryTheory.Factorisation.initialHom_h`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`h`	—	—	—
`ext_iff` 📖	mathematical	—	`h`	—	`ext`
`h_π` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Factorisation.mid` `h` `CategoryTheory.Factorisation.π`	—	—
`h_π_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Factorisation.mid` `h` `CategoryTheory.Factorisation.π`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `h_π`
`ι_h` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Factorisation.mid` `CategoryTheory.Factorisation.ι` `h`	—	—
`ι_h_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Factorisation.mid` `CategoryTheory.Factorisation.ι` `h`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι_h`

---

← Back to Index