Documentation Verification Report

CategoryWithFibrations

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/CategoryWithFibrations.lean

Statistics

Metric	Count
Definitions `CategoryWithFibrations`, `I`, `J`, `instCategoryWithCofibrations`, `instCategoryWithFibrations`	5
Theorems `I_le_monomorphisms`, `J_le_monomorphisms`, `boundary_ι_mem_I`, `cofibration_iff`, `cofibration_of_mono`, `cofibrations_eq`, `fibration_iff`, `fibrations_eq`, `horn_ι_mem_J`, `instHasLiftingPropertyιHornHAddNatOfNatOfFibration`, `mono_of_cofibration`	11
Total	16

HomotopicalAlgebra

Definitions

Name	Category	Theorems
`CategoryWithFibrations` 📖	CompData	—

SSet.modelCategoryQuillen

Definitions

Name	Category	Theorems
`I` 📖	CompOp	2 math math: `I_le_monomorphisms`, `boundary_ι_mem_I`
`J` 📖	CompOp	4 math math: `fibrations_eq`, `horn_ι_mem_J`, `J_le_monomorphisms`, `fibration_iff`
`instCategoryWithCofibrations` 📖	CompOp	3 math math: `cofibrations_eq`, `cofibration_of_mono`, `cofibration_iff`
`instCategoryWithFibrations` 📖	CompOp	2 math math: `fibrations_eq`, `fibration_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`I_le_monomorphisms` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `SSet` `CategoryTheory.Category.toCategoryStruct` `SSet.largeCategory` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `I` `CategoryTheory.MorphismProperty.monomorphisms`	—	`CategoryTheory.MorphismProperty.monomorphisms.infer_property` `SSet.Subcomplex.instMonoι`
`J_le_monomorphisms` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `SSet` `CategoryTheory.Category.toCategoryStruct` `SSet.largeCategory` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `J` `CategoryTheory.MorphismProperty.monomorphisms`	—	`CategoryTheory.MorphismProperty.monomorphisms.infer_property` `SSet.Subcomplex.instMonoι`
`boundary_ι_mem_I` 📖	mathematical	—	`I` `SSet.Subcomplex.toSSet` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet` `SSet.largeCategory` `SSet.stdSimplex` `SSet.boundary` `SSet.Subcomplex.ι`	—	—
`cofibration_iff` 📖	mathematical	—	`HomotopicalAlgebra.Cofibration` `SSet` `SSet.largeCategory` `instCategoryWithCofibrations` `CategoryTheory.Mono`	—	`HomotopicalAlgebra.cofibration_iff`
`cofibration_of_mono` 📖	mathematical	—	`HomotopicalAlgebra.Cofibration` `SSet` `SSet.largeCategory` `instCategoryWithCofibrations`	—	`cofibration_iff`
`cofibrations_eq` 📖	mathematical	—	`HomotopicalAlgebra.cofibrations` `SSet` `SSet.largeCategory` `instCategoryWithCofibrations` `CategoryTheory.MorphismProperty.monomorphisms`	—	—
`fibration_iff` 📖	mathematical	—	`HomotopicalAlgebra.Fibration` `SSet` `SSet.largeCategory` `instCategoryWithFibrations` `CategoryTheory.MorphismProperty.rlp` `J`	—	`HomotopicalAlgebra.fibration_iff`
`fibrations_eq` 📖	mathematical	—	`HomotopicalAlgebra.fibrations` `SSet` `SSet.largeCategory` `instCategoryWithFibrations` `CategoryTheory.MorphismProperty.rlp` `J`	—	—
`horn_ι_mem_J` 📖	mathematical	—	`J` `SSet.Subcomplex.toSSet` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet` `SSet.largeCategory` `SSet.stdSimplex` `SSet.horn` `SSet.Subcomplex.ι`	—	—
`instHasLiftingPropertyιHornHAddNatOfNatOfFibration` 📖	mathematical	—	`CategoryTheory.HasLiftingProperty` `SSet` `SSet.largeCategory` `SSet.Subcomplex.toSSet` `CategoryTheory.Functor.obj` `SimplexCategory` `SimplexCategory.smallCategory` `SSet.stdSimplex` `SSet.horn` `SSet.Subcomplex.ι`	—	`fibration_iff` `horn_ι_mem_J`
`mono_of_cofibration` 📖	mathematical	—	`CategoryTheory.Mono` `SSet` `SSet.largeCategory`	—	`cofibration_iff`

---

← Back to Index