Commit 2025-02-08 15:33 60416231

View on Github →

feat: definition and basic lemmas about CW-complexes (#19760) This PR defines (relative) CW-complexes in the original way Whitehead defined them: As a collection of cells that is closure finite and has weak topology. It additionally proves basic properties about them. See this discussion on Zulip about the two possible definitions. Co-authered-by: Floris van Doorn fpvdoorn@gmail.com

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/Topology/CWComplex.lean to Mathlib/Topology/CWComplex/Abstract/Basic.lean

deleted structure CWComplex

added structure CategoryTheory.CWComplex

added def CategoryTheory.RelativeCWComplex.AttachCells

added def CategoryTheory.RelativeCWComplex.AttachGeneralizedCells.inclusion

added structure CategoryTheory.RelativeCWComplex.AttachGeneralizedCells

added def CategoryTheory.RelativeCWComplex.skInclusion

added def CategoryTheory.RelativeCWComplex.sphereInclusion

added def CategoryTheory.RelativeCWComplex.toTopCat

added structure CategoryTheory.RelativeCWComplex

deleted def RelativeCWComplex.AttachCells

deleted def RelativeCWComplex.AttachGeneralizedCells.inclusion

deleted structure RelativeCWComplex.AttachGeneralizedCells

deleted def RelativeCWComplex.skInclusion

deleted def RelativeCWComplex.sphereInclusion

deleted def RelativeCWComplex.toTopCat

deleted structure RelativeCWComplex

Created Mathlib/Topology/CWComplex/Classical/Basic.lean

added theorem Topology.CWComplex.cellFrontier_subset_finite_closedCell

added theorem Topology.CWComplex.closed

added theorem Topology.CWComplex.mapsto

added def Topology.CWComplex.mk.{u}

added theorem Topology.CWComplex.skeletonLT_zero_eq_empty

added theorem Topology.CWComplex.union

added theorem Topology.RelCWComplex.base_subset_complex

added theorem Topology.RelCWComplex.base_subset_skeleton

added theorem Topology.RelCWComplex.base_subset_skeletonLT

added def Topology.RelCWComplex.cellFrontier

added theorem Topology.RelCWComplex.cellFrontier_subset_base_union_finite_closedCell

added theorem Topology.RelCWComplex.cellFrontier_subset_closedCell

added theorem Topology.RelCWComplex.cellFrontier_subset_skeleton

added theorem Topology.RelCWComplex.cellFrontier_subset_skeletonLT

added theorem Topology.RelCWComplex.cellFrontier_union_openCell_eq_closedCell

added theorem Topology.RelCWComplex.cellFrontier_zero_eq_empty

added theorem Topology.RelCWComplex.closed

added def Topology.RelCWComplex.closedCell

added theorem Topology.RelCWComplex.closedCell_subset_complex

added theorem Topology.RelCWComplex.closedCell_subset_skeleton

added theorem Topology.RelCWComplex.closedCell_subset_skeletonLT

added theorem Topology.RelCWComplex.closedCell_zero_eq_singleton

added theorem Topology.RelCWComplex.closure_openCell_eq_closedCell

added theorem Topology.RelCWComplex.disjointBase

added theorem Topology.RelCWComplex.disjoint_openCell_of_ne

added theorem Topology.RelCWComplex.iUnion_cellFrontier_subset_skeleton

added theorem Topology.RelCWComplex.iUnion_cellFrontier_subset_skeletonLT

added theorem Topology.RelCWComplex.isClosed_cellFrontier

added theorem Topology.RelCWComplex.isClosed_closedCell

added theorem Topology.RelCWComplex.isCompact_cellFrontier

added theorem Topology.RelCWComplex.isCompact_closedCell

added theorem Topology.RelCWComplex.map_zero_mem_closedCell

added theorem Topology.RelCWComplex.map_zero_mem_openCell

added def Topology.RelCWComplex.openCell

added theorem Topology.RelCWComplex.openCell_subset_closedCell

added theorem Topology.RelCWComplex.openCell_subset_complex

added theorem Topology.RelCWComplex.openCell_subset_skeleton

added theorem Topology.RelCWComplex.openCell_subset_skeletonLT

added theorem Topology.RelCWComplex.openCell_zero_eq_singleton

added theorem Topology.RelCWComplex.pairwiseDisjoint

added def Topology.RelCWComplex.skeleton

added def Topology.RelCWComplex.skeletonLT

added theorem Topology.RelCWComplex.skeletonLT_mono

added theorem Topology.RelCWComplex.skeletonLT_subset_complex

added theorem Topology.RelCWComplex.skeletonLT_top

added theorem Topology.RelCWComplex.skeletonLT_zero_eq_base

added theorem Topology.RelCWComplex.skeleton_mono

added theorem Topology.RelCWComplex.skeleton_subset_complex

added theorem Topology.RelCWComplex.skeleton_top

added theorem Topology.RelCWComplex.union

Modified docs/references.bib