Documentation Verification Report

EpiMono

📁 Source: Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean

Statistics

Metric	Count
Definitions `P_δ`, `P_σ`, `splitEpiσ`, `splitMonoδ`	4
Theorems `δ`, `σ`, `eq_or_len_le_of_P_δ`, `exists_P_σ_P_δ_factorization`, `instHasFactorizationP_σP_δ`, `instIsSplitEpiσ`, `instIsSplitMonoδ`, `isSplitEpi_P_σ`, `isSplitEpi_toSimplexCategory_map_of_P_σ`, `isSplitMono_P_δ`, `isSplitMono_toSimplexCategory_map_of_P_δ`	11
Total	15

SimplexCategoryGenRel

Definitions

Name	Category	Theorems
`P_δ` 📖	CompOp	2 math math: `P_δ.δ`, `instHasFactorizationP_σP_δ`
`P_σ` 📖	CompOp	2 math math: `P_σ.σ`, `instHasFactorizationP_σP_δ`
`splitEpiσ` 📖	CompOp	—
`splitMonoδ` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_or_len_le_of_P_δ` 📖	mathematical	`P_δ`	`CategoryTheory.eqToHom` `SimplexCategoryGenRel` `CategoryTheory.Category.toCategoryStruct` `instCategorySimplexCategoryGenRel` `len`	—	`IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instZeroLEOneClass`
`exists_P_σ_P_δ_factorization` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `SimplexCategoryGenRel` `CategoryTheory.Category.toCategoryStruct` `instCategorySimplexCategoryGenRel`	—	`hom_induction` `CategoryTheory.MorphismProperty.id_mem` `CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities` `CategoryTheory.MorphismProperty.instIsMultiplicativeMultiplicativeClosure` `CategoryTheory.Category.comp_id` `CategoryTheory.MorphismProperty.comp_mem` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `P_δ.δ` `CategoryTheory.Category.assoc` `P_σ.σ` `Mathlib.Tactic.Reassoc.eq_whisker'`
`instHasFactorizationP_σP_δ` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasFactorization` `SimplexCategoryGenRel` `instCategorySimplexCategoryGenRel` `P_σ` `P_δ`	—	`exists_P_σ_P_δ_factorization`
`instIsSplitEpiσ` 📖	mathematical	—	`CategoryTheory.IsSplitEpi` `SimplexCategoryGenRel` `instCategorySimplexCategoryGenRel` `σ`	—	`CategoryTheory.IsSplitEpi.mk'`
`instIsSplitMonoδ` 📖	mathematical	—	`CategoryTheory.IsSplitMono` `SimplexCategoryGenRel` `instCategorySimplexCategoryGenRel` `δ`	—	`CategoryTheory.IsSplitMono.mk'`
`isSplitEpi_P_σ` 📖	mathematical	`P_σ`	`CategoryTheory.IsSplitEpi` `SimplexCategoryGenRel` `instCategorySimplexCategoryGenRel`	—	`instIsSplitEpiσ` `CategoryTheory.IsSplitEpi.of_iso` `CategoryTheory.IsIso.id` `CategoryTheory.instIsSplitEpiComp`
`isSplitEpi_toSimplexCategory_map_of_P_σ` 📖	mathematical	`P_σ`	`CategoryTheory.IsSplitEpi` `SimplexCategory` `SimplexCategory.smallCategory` `CategoryTheory.Functor.obj` `SimplexCategoryGenRel` `instCategorySimplexCategoryGenRel` `toSimplexCategory` `CategoryTheory.Functor.map`	—	`CategoryTheory.IsSplitEpi.exists_splitEpi` `isSplitEpi_P_σ`
`isSplitMono_P_δ` 📖	mathematical	`P_δ`	`CategoryTheory.IsSplitMono` `SimplexCategoryGenRel` `instCategorySimplexCategoryGenRel`	—	`instIsSplitMonoδ` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.IsIso.id` `CategoryTheory.instIsSplitMonoComp`
`isSplitMono_toSimplexCategory_map_of_P_δ` 📖	mathematical	`P_δ`	`CategoryTheory.IsSplitMono` `SimplexCategory` `SimplexCategory.smallCategory` `CategoryTheory.Functor.obj` `SimplexCategoryGenRel` `instCategorySimplexCategoryGenRel` `toSimplexCategory` `CategoryTheory.Functor.map`	—	`CategoryTheory.IsSplitMono.exists_splitMono` `isSplitMono_P_δ`

SimplexCategoryGenRel.P_δ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`δ` 📖	mathematical	—	`SimplexCategoryGenRel.P_δ` `SimplexCategoryGenRel.δ`	—	—

SimplexCategoryGenRel.P_σ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`σ` 📖	mathematical	—	`SimplexCategoryGenRel.P_σ` `SimplexCategoryGenRel.σ`	—	—

---

← Back to Index