Documentation Verification Report

Opposite

📁 Source: Mathlib/AlgebraicTopology/ModelCategory/Opposite.lean

Statistics

Metric	Count
Definitions `instModelCategoryOpposite`	1
Theorems `instHasFactorizationOppositeCofibrationsTrivialFibrationsOfTrivialCofibrationsFibrations`, `instHasFactorizationOppositeTrivialCofibrationsFibrationsOfCofibrationsTrivialFibrations`, `instHasTwoOutOfThreePropertyOppositeWeakEquivalences`, `instIsStableUnderRetractsOppositeCofibrationsOfFibrations`, `instIsStableUnderRetractsOppositeFibrationsOfCofibrations`, `instIsStableUnderRetractsOppositeWeakEquivalences`	6
Total	7

HomotopicalAlgebra

Definitions

Name	Category	Theorems
`instModelCategoryOpposite` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasFactorizationOppositeCofibrationsTrivialFibrationsOfTrivialCofibrationsFibrations` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasFactorization` `Opposite` `CategoryTheory.Category.opposite` `cofibrations` `instCategoryWithCofibrationsOpposite` `ModelCategory.categoryWithFibrations` `trivialFibrations` `instCategoryWithFibrationsOpposite` `ModelCategory.categoryWithCofibrations` `instCategoryWithWeakEquivalencesOpposite` `ModelCategory.categoryWithWeakEquivalences`	—	`cofibrations_op` `trivialFibrations_op` `CategoryTheory.MorphismProperty.instHasFactorizationOppositeOp`
`instHasFactorizationOppositeTrivialCofibrationsFibrationsOfCofibrationsTrivialFibrations` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasFactorization` `Opposite` `CategoryTheory.Category.opposite` `trivialCofibrations` `instCategoryWithCofibrationsOpposite` `ModelCategory.categoryWithFibrations` `instCategoryWithWeakEquivalencesOpposite` `ModelCategory.categoryWithWeakEquivalences` `fibrations` `instCategoryWithFibrationsOpposite` `ModelCategory.categoryWithCofibrations`	—	`trivialCofibrations_op` `fibrations_op` `CategoryTheory.MorphismProperty.instHasFactorizationOppositeOp`
`instHasTwoOutOfThreePropertyOppositeWeakEquivalences` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty` `Opposite` `CategoryTheory.Category.opposite` `weakEquivalences` `instCategoryWithWeakEquivalencesOpposite` `ModelCategory.categoryWithWeakEquivalences`	—	`weakEquivalences_op` `CategoryTheory.MorphismProperty.instHasTwoOutOfThreePropertyOppositeOp`
`instIsStableUnderRetractsOppositeCofibrationsOfFibrations` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderRetracts` `Opposite` `CategoryTheory.Category.opposite` `cofibrations` `instCategoryWithCofibrationsOpposite` `ModelCategory.categoryWithFibrations`	—	`cofibrations_op` `CategoryTheory.MorphismProperty.instIsStableUnderRetractsOppositeOp`
`instIsStableUnderRetractsOppositeFibrationsOfCofibrations` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderRetracts` `Opposite` `CategoryTheory.Category.opposite` `fibrations` `instCategoryWithFibrationsOpposite` `ModelCategory.categoryWithCofibrations`	—	`fibrations_op` `CategoryTheory.MorphismProperty.instIsStableUnderRetractsOppositeOp`
`instIsStableUnderRetractsOppositeWeakEquivalences` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderRetracts` `Opposite` `CategoryTheory.Category.opposite` `weakEquivalences` `instCategoryWithWeakEquivalencesOpposite` `ModelCategory.categoryWithWeakEquivalences`	—	`weakEquivalences_op` `CategoryTheory.MorphismProperty.instIsStableUnderRetractsOppositeOp`

---

← Back to Index