Commit 2025-11-09 13:26 e1899662

View on Github →

feat(AlgebraicTopology): the opposite of a model category structure (#31095) In this PR, we show that if C is a model category, then so is Cᵒᵖ.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicTopology/ModelCategory/CategoryWithCofibrations.lean

added theorem HomotopicalAlgebra.cofibration_op_iff

added theorem HomotopicalAlgebra.cofibration_unop_iff

added theorem HomotopicalAlgebra.cofibrations_eq_unop

added theorem HomotopicalAlgebra.cofibrations_op

added theorem HomotopicalAlgebra.fibration_op_iff

added theorem HomotopicalAlgebra.fibration_unop_iff

added theorem HomotopicalAlgebra.fibrations_eq_unop

added theorem HomotopicalAlgebra.fibrations_op

added theorem HomotopicalAlgebra.trivialCofibrations_eq_unop

added theorem HomotopicalAlgebra.trivialCofibrations_op

added theorem HomotopicalAlgebra.trivialFibrations_eq_unop

added theorem HomotopicalAlgebra.trivialFibrations_op

added theorem HomotopicalAlgebra.weakEquivalences_eq_unop

added theorem HomotopicalAlgebra.weakEquivalences_op

added theorem HomotopicalAlgebra.weakEquivalences_op_iff

added theorem HomotopicalAlgebra.weakEquivalences_unop_iff

Created Mathlib/AlgebraicTopology/ModelCategory/Opposite.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Composition.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Factorization.lean

added def CategoryTheory.MorphismProperty.MapFactorizationData.op

Modified Mathlib/CategoryTheory/MorphismProperty/Retract.lean

Modified Mathlib/CategoryTheory/Retract.lean

added def CategoryTheory.RetractArrow.op

added def CategoryTheory.RetractArrow.unop