Documentation Verification Report

Over

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

Statistics

Metric	Count
Definitions `over`, `instCategoryWithCofibrationsOver`, `instCategoryWithFibrationsOver`, `instCategoryWithWeakEquivalencesOver`	4
Theorems `cofibrations_over_def`, `cofibrations_over_iff`, `fibrations_over_def`, `fibrations_over_iff`, `instCofibrationLeftDiscretePUnitOfOver`, `instFibrationLeftDiscretePUnitOfOver`, `instHasFactorizationOverCofibrationsTrivialFibrations`, `instHasFactorizationOverTrivialCofibrationsFibrations`, `instHasTwoOutOfThreePropertyOverWeakEquivalences`, `instIsStableUnderRetractsOverCofibrations`, `instIsStableUnderRetractsOverFibrations`, `instIsStableUnderRetractsOverWeakEquivalences`, `instWeakEquivalenceLeftDiscretePUnitOfOver`, `trivialCofibrations_over_eq`, `trivialFibrations_over_eq`, `weakEquivalences_over_def`, `weakEquivalences_over_iff`	17
Total	21

HomotopicalAlgebra

Definitions

Name	Category	Theorems
`instCategoryWithCofibrationsOver` 📖	CompOp	6 math math: `cofibrations_over_iff`, `instIsStableUnderRetractsOverCofibrations`, `trivialCofibrations_over_eq`, `cofibrations_over_def`, `instHasFactorizationOverTrivialCofibrationsFibrations`, `instHasFactorizationOverCofibrationsTrivialFibrations`
`instCategoryWithFibrationsOver` 📖	CompOp	6 math math: `instIsStableUnderRetractsOverFibrations`, `trivialFibrations_over_eq`, `fibrations_over_def`, `instHasFactorizationOverTrivialCofibrationsFibrations`, `instHasFactorizationOverCofibrationsTrivialFibrations`, `fibrations_over_iff`
`instCategoryWithWeakEquivalencesOver` 📖	CompOp	8 math math: `trivialFibrations_over_eq`, `trivialCofibrations_over_eq`, `instHasFactorizationOverTrivialCofibrationsFibrations`, `instHasTwoOutOfThreePropertyOverWeakEquivalences`, `weakEquivalences_over_iff`, `instHasFactorizationOverCofibrationsTrivialFibrations`, `instIsStableUnderRetractsOverWeakEquivalences`, `weakEquivalences_over_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cofibrations_over_def` 📖	mathematical	—	`cofibrations` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `instCategoryWithCofibrationsOver` `CategoryTheory.MorphismProperty.over`	—	—
`cofibrations_over_iff` 📖	mathematical	—	`Cofibration` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `instCategoryWithCofibrationsOver` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.CommaMorphism.left`	—	—
`fibrations_over_def` 📖	mathematical	—	`fibrations` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `instCategoryWithFibrationsOver` `CategoryTheory.MorphismProperty.over`	—	—
`fibrations_over_iff` 📖	mathematical	—	`Fibration` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `instCategoryWithFibrationsOver` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.CommaMorphism.left`	—	—
`instCofibrationLeftDiscretePUnitOfOver` 📖	mathematical	—	`Cofibration` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.CommaMorphism.left`	—	`cofibrations_over_iff`
`instFibrationLeftDiscretePUnitOfOver` 📖	mathematical	—	`Fibration` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.CommaMorphism.left`	—	`fibrations_over_iff`
`instHasFactorizationOverCofibrationsTrivialFibrations` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasFactorization` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `cofibrations` `instCategoryWithCofibrationsOver` `trivialFibrations` `instCategoryWithFibrationsOver` `instCategoryWithWeakEquivalencesOver`	—	`cofibrations_over_def` `trivialFibrations_over_eq` `CategoryTheory.MorphismProperty.HasFactorization.over`
`instHasFactorizationOverTrivialCofibrationsFibrations` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasFactorization` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `trivialCofibrations` `instCategoryWithCofibrationsOver` `instCategoryWithWeakEquivalencesOver` `fibrations` `instCategoryWithFibrationsOver`	—	`fibrations_over_def` `trivialCofibrations_over_eq` `CategoryTheory.MorphismProperty.HasFactorization.over`
`instHasTwoOutOfThreePropertyOverWeakEquivalences` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `weakEquivalences` `instCategoryWithWeakEquivalencesOver`	—	`weakEquivalences_over_def` `CategoryTheory.MorphismProperty.over_eq_inverseImage` `CategoryTheory.MorphismProperty.instHasTwoOutOfThreePropertyInverseImage`
`instIsStableUnderRetractsOverCofibrations` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderRetracts` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `cofibrations` `instCategoryWithCofibrationsOver`	—	`cofibrations_over_def` `CategoryTheory.MorphismProperty.over_eq_inverseImage` `CategoryTheory.MorphismProperty.instIsStableUnderRetractsInverseImage`
`instIsStableUnderRetractsOverFibrations` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderRetracts` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `fibrations` `instCategoryWithFibrationsOver`	—	`fibrations_over_def` `CategoryTheory.MorphismProperty.over_eq_inverseImage` `CategoryTheory.MorphismProperty.instIsStableUnderRetractsInverseImage`
`instIsStableUnderRetractsOverWeakEquivalences` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderRetracts` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `weakEquivalences` `instCategoryWithWeakEquivalencesOver`	—	`weakEquivalences_over_def` `CategoryTheory.MorphismProperty.over_eq_inverseImage` `CategoryTheory.MorphismProperty.instIsStableUnderRetractsInverseImage`
`instWeakEquivalenceLeftDiscretePUnitOfOver` 📖	mathematical	—	`WeakEquivalence` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.CommaMorphism.left`	—	`weakEquivalences_over_iff`
`trivialCofibrations_over_eq` 📖	mathematical	—	`trivialCofibrations` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `instCategoryWithCofibrationsOver` `instCategoryWithWeakEquivalencesOver` `CategoryTheory.MorphismProperty.over`	—	—
`trivialFibrations_over_eq` 📖	mathematical	—	`trivialFibrations` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `instCategoryWithFibrationsOver` `instCategoryWithWeakEquivalencesOver` `CategoryTheory.MorphismProperty.over`	—	—
`weakEquivalences_over_def` 📖	mathematical	—	`weakEquivalences` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `instCategoryWithWeakEquivalencesOver` `CategoryTheory.MorphismProperty.over`	—	—
`weakEquivalences_over_iff` 📖	mathematical	—	`WeakEquivalence` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `instCategoryWithWeakEquivalencesOver` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.CommaMorphism.left`	—	—

HomotopicalAlgebra.ModelCategory

Definitions

Name	Category	Theorems
`over` 📖	CompOp	—

---

← Back to Index