Commit 2025-03-20 22:37 de8381da

View on Github →

feat(AlgebraicTopology): endow SSet with notions of cofibrations and fibrations (#21118) We define cofibrations and fibrations in the category of simplicial sets. Kan complexes are redefined (through an abbreviation) as fibrant objects in this category.

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/SimplicialSet/CategoryWithFibrations.lean

added def SSet.modelCategoryQuillen.I

added theorem SSet.modelCategoryQuillen.I_le_monomorphisms

added def SSet.modelCategoryQuillen.J

added theorem SSet.modelCategoryQuillen.J_le_monomorphisms

added theorem SSet.modelCategoryQuillen.boundary_ι_mem_I

added theorem SSet.modelCategoryQuillen.cofibration_iff

added theorem SSet.modelCategoryQuillen.cofibration_of_mono

added theorem SSet.modelCategoryQuillen.cofibrations_eq

added theorem SSet.modelCategoryQuillen.fibration_iff

added theorem SSet.modelCategoryQuillen.fibrations_eq

added theorem SSet.modelCategoryQuillen.horn_ι_mem_J

Modified Mathlib/AlgebraicTopology/SimplicialSet/KanComplex.lean

added theorem SSet.KanComplex.hornFilling

Modified Mathlib/AlgebraicTopology/SimplicialSet/Subcomplex.lean