Documentation Verification Report

Factorisation

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

Statistics

Metric	Count
Definitions `Factorisation`, `comp`, `h`, `id`, `IsInitial_initial`, `IsTerminal_terminal`, `forget`, `initial`, `initialHom`, `instCategory`, `instUniqueHomInitial`, `instUniqueHomTerminal`, `mid`, `terminal`, `terminalHom`, `ι`, `π`	17
Theorems `comp_h`, `ext`, `ext_iff`, `h_π`, `id_h`, `ι_h`, `forget_map`, `forget_obj`, `initialHom_h`, `initial_mid`, `initial_ι`, `initial_π`, `instHasInitial`, `instHasTerminal`, `terminalHom_h`, `terminal_mid`, `terminal_ι`, `terminal_π`, `ι_π`	19
Total	36

CategoryTheory

Definitions

Name	Category	Theorems
`Factorisation` 📖	CompData	4 math math: `Factorisation.forget_map`, `Factorisation.forget_obj`, `Factorisation.instHasInitial`, `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	4 math math: `forget_map`, `forget_obj`, `instHasInitial`, `instHasTerminal`
`instUniqueHomInitial` 📖	CompOp	—
`instUniqueHomTerminal` 📖	CompOp	—
`mid` 📖	CompOp	8 math math: `forget_obj`, `Hom.id_h`, `Hom.ι_h`, `initial_mid`, `Hom.h_π`, `ι_π`, `Hom.comp_h`, `terminal_mid`
`terminal` 📖	CompOp	4 math math: `terminalHom_h`, `terminal_π`, `terminal_ι`, `terminal_mid`
`terminalHom` 📖	CompOp	1 math math: `terminalHom_h`
`ι` 📖	CompOp	5 math math: `initial_ι`, `Hom.ι_h`, `terminal_ι`, `ι_π`, `initialHom_h`
`π` 📖	CompOp	5 math math: `terminalHom_h`, `initial_π`, `terminal_π`, `Hom.h_π`, `ι_π`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forget_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Factorisation` `instCategory` `forget` `Hom.h`	—	—
`forget_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Factorisation` `instCategory` `forget` `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` `ι` `π`	—	—

CategoryTheory.Factorisation.Hom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	1 math math: `comp_h`
`h` 📖	CompOp	8 math math: `CategoryTheory.Factorisation.forget_map`, `id_h`, `CategoryTheory.Factorisation.terminalHom_h`, `ι_h`, `ext_iff`, `h_π`, `comp_h`, `CategoryTheory.Factorisation.initialHom_h`
`id` 📖	CompOp	1 math math: `id_h`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_h` 📖	mathematical	—	`h` `comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Factorisation.mid`	—	—
`ext` 📖	—	`h`	—	—	—
`ext_iff` 📖	mathematical	—	`h`	—	`ext`
`h_π` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Factorisation.mid` `h` `CategoryTheory.Factorisation.π`	—	—
`id_h` 📖	mathematical	—	`h` `id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Factorisation.mid`	—	—
`ι_h` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Factorisation.mid` `CategoryTheory.Factorisation.ι` `h`	—	—

---

← Back to Index