Documentation
Mathlib
.
AlgebraicTopology
.
ModelCategory
.
Opposite
Search
return to top
source
Imports
Init
Mathlib.AlgebraicTopology.ModelCategory.Basic
Imported by
HomotopicalAlgebra
.
instHasTwoOutOfThreePropertyOppositeWeakEquivalences
HomotopicalAlgebra
.
instIsStableUnderRetractsOppositeWeakEquivalences
HomotopicalAlgebra
.
instIsStableUnderRetractsOppositeFibrationsOfCofibrations
HomotopicalAlgebra
.
instIsStableUnderRetractsOppositeCofibrationsOfFibrations
HomotopicalAlgebra
.
instHasFactorizationOppositeCofibrationsTrivialFibrationsOfTrivialCofibrationsFibrations
HomotopicalAlgebra
.
instHasFactorizationOppositeTrivialCofibrationsFibrationsOfCofibrationsTrivialFibrations
HomotopicalAlgebra
.
instModelCategoryOpposite
The opposite of a model category structure
#
source
instance
HomotopicalAlgebra
.
instHasTwoOutOfThreePropertyOppositeWeakEquivalences
(
C
:
Type
u)
[
CategoryTheory.Category.{v, u}
C
]
[
ModelCategory
C
]
[
(
weakEquivalences
C
)
.
HasTwoOutOfThreeProperty
]
:
(
weakEquivalences
C
ᵒᵖ
)
.
HasTwoOutOfThreeProperty
source
instance
HomotopicalAlgebra
.
instIsStableUnderRetractsOppositeWeakEquivalences
(
C
:
Type
u)
[
CategoryTheory.Category.{v, u}
C
]
[
ModelCategory
C
]
[
(
weakEquivalences
C
)
.
IsStableUnderRetracts
]
:
(
weakEquivalences
C
ᵒᵖ
)
.
IsStableUnderRetracts
source
instance
HomotopicalAlgebra
.
instIsStableUnderRetractsOppositeFibrationsOfCofibrations
(
C
:
Type
u)
[
CategoryTheory.Category.{v, u}
C
]
[
ModelCategory
C
]
[
(
cofibrations
C
)
.
IsStableUnderRetracts
]
:
(
fibrations
C
ᵒᵖ
)
.
IsStableUnderRetracts
source
instance
HomotopicalAlgebra
.
instIsStableUnderRetractsOppositeCofibrationsOfFibrations
(
C
:
Type
u)
[
CategoryTheory.Category.{v, u}
C
]
[
ModelCategory
C
]
[
(
fibrations
C
)
.
IsStableUnderRetracts
]
:
(
cofibrations
C
ᵒᵖ
)
.
IsStableUnderRetracts
source
instance
HomotopicalAlgebra
.
instHasFactorizationOppositeCofibrationsTrivialFibrationsOfTrivialCofibrationsFibrations
(
C
:
Type
u)
[
CategoryTheory.Category.{v, u}
C
]
[
ModelCategory
C
]
[
(
trivialCofibrations
C
)
.
HasFactorization
(
fibrations
C
)
]
:
(
cofibrations
C
ᵒᵖ
)
.
HasFactorization
(
trivialFibrations
C
ᵒᵖ
)
source
instance
HomotopicalAlgebra
.
instHasFactorizationOppositeTrivialCofibrationsFibrationsOfCofibrationsTrivialFibrations
(
C
:
Type
u)
[
CategoryTheory.Category.{v, u}
C
]
[
ModelCategory
C
]
[
(
cofibrations
C
)
.
HasFactorization
(
trivialFibrations
C
)
]
:
(
trivialCofibrations
C
ᵒᵖ
)
.
HasFactorization
(
fibrations
C
ᵒᵖ
)
source
instance
HomotopicalAlgebra
.
instModelCategoryOpposite
(
C
:
Type
u)
[
CategoryTheory.Category.{v, u}
C
]
[
ModelCategory
C
]
:
ModelCategory
C
ᵒᵖ
Equations
One or more equations did not get rendered due to their size.