Commit 2025-11-09 14:03 48aa5529

View on Github →

feat(AlgebraicTopology): basic API for subcomplexes of simplicial sets (#31122) This PR adds basic API for subcomplexes of simplicial sets: range, image, preimage, etc. From https://github.com/joelriou/topcat-model-category

Estimated changes

Modified Mathlib/AlgebraicTopology/SimplicialSet/Subcomplex.lean

added def SSet.Subcomplex.eqToIso

added def SSet.Subcomplex.fromPreimage

added theorem SSet.Subcomplex.fromPreimage_ι

added theorem SSet.Subcomplex.homOfLE_app_val

added theorem SSet.Subcomplex.homOfLE_comp

added theorem SSet.Subcomplex.homOfLE_refl

added theorem SSet.Subcomplex.homOfLE_ι

added def SSet.Subcomplex.image

added theorem SSet.Subcomplex.image_comp

added theorem SSet.Subcomplex.image_eq_range

added theorem SSet.Subcomplex.image_iSup

added theorem SSet.Subcomplex.image_id

added theorem SSet.Subcomplex.image_le_iff

added theorem SSet.Subcomplex.image_le_range

added theorem SSet.Subcomplex.image_monotone

added theorem SSet.Subcomplex.image_ofSimplex

added theorem SSet.Subcomplex.image_preimage_le

added theorem SSet.Subcomplex.image_top

added def SSet.Subcomplex.isInitialBot

added def SSet.Subcomplex.lift

added theorem SSet.Subcomplex.lift_app_coe

added theorem SSet.Subcomplex.lift_ι

added def SSet.Subcomplex.preimage

added theorem SSet.Subcomplex.preimage_eq_top_iff

added theorem SSet.Subcomplex.preimage_iInf

added theorem SSet.Subcomplex.preimage_iSup

added theorem SSet.Subcomplex.preimage_max

added theorem SSet.Subcomplex.preimage_min

added theorem SSet.Subcomplex.preimage_range

added theorem SSet.Subcomplex.range_comp

added theorem SSet.Subcomplex.range_eq_top

added theorem SSet.Subcomplex.range_eq_top_iff

added def SSet.Subcomplex.toImage

added theorem SSet.Subcomplex.toImage_ι

added def SSet.Subcomplex.toSSetFunctor

added def SSet.Subcomplex.topIso

added theorem SSet.Subcomplex.topIso_hom

added theorem SSet.Subcomplex.topIso_inv_ι