CW complexes

This file defines (relative) CW complexes and proves basic properties about them using the classical approach of Whitehead.

A CW complex is a topological space that is made by gluing closed disks of different dimensions together.

Main definitions

• RelCWComplex C D: the class of CW structures on a subspace C relative to a base set D of a topological space X.
• CWComplex C: an abbreviation for RelCWComplex C ∅. The class of CW structures on a subspace C of the topological space X.
• openCell n: indexed family of all open cells of dimension n.
• closedCell n: indexed family of all closed cells of dimension n.
• cellFrontier n: indexed family of the boundaries of cells of dimension n.
• skeleton C n: the n-skeleton of the (relative) CW complex C.

Main statements

• iUnion_openCell_eq_skeleton: the skeletons can also be seen as a union of open cells.
• cellFrontier_subset_finite_openCell: the edge of a cell is contained in a finite union of open cells of a lower dimension.

Implementation notes

• We use the historical definition of CW complexes, due to Whitehead: a CW complex is a collection of cells with attaching maps - all cells are subspaces of one ambient topological space. This way, we avoid having to work with a lot of different topological spaces. On the other hand, it requires the union of all cells to be closed. If that is not the case, you need to consider that union as a subspace of itself.
• For a categorical approach that defines CW complexes via colimits and transfinite compositions, see Mathlib/Topology/CWComplex/Abstract/Basic.lean. The two approaches are equivalent but serve different purposes:
  • This approach is more convenient for concrete geometric arguments
  • The categorical approach is more suitable for abstract arguments and generalizations
• The definition RelCWComplex does not require X to be a Hausdorff space. A lot of the lemmas will however require this property.
• This definition is a class to ease working with different constructions and their properties. Overall this means that being a CW complex is treated more like a property than data.
• The natural number is explicit in openCell, closedCell and cellFrontier because cell n and cell m might be the same type in an explicit CW complex even when n and m are different.
• CWComplex is a separate class from RelCWComplex. This not only gives absolute CW complexes a better constructor but also aids typeclass inference: a construction on relative CW complexes may yield a base that for the special case of CW complexes is provably equal to the empty set but not definitionally so. In that case we define an instance specifically for absolute CW complexes and want this to be inferred over the relative version. Since the base is an outParam this is especially necessary since you cannot provide typeclass inference with a specified base. But having the type CWComplex be separate from RelCWComplex makes this specification possible.
• For a similar reason to the previous bullet point we make the instance CWComplex.instRelCWComplex have high priority. For example, when talking about the type of cells cell C of an absolute CW complex C, this actually refers to RelCWComplex.cell C through this instance. Again, we want typeclass inference to first consider absolute CW structures.
• For statements, the auxiliary construction skeletonLT is preferred over skeleton as it makes the base case of inductions easier. The statement about skeleton should then be derived from the one about skeletonLT.

References

• [A. Hatcher, Algebraic Topology][hatcher02]

class Topology.RelCWComplex {X : Type u} [TopologicalSpace X] (C : Set X) (D : outParam (Set X)) : Type (u + 1)

A CW complex of a topological space X relative to another subspace D is the data of its n-cells cell n i for each n : ℕ along with attaching maps that satisfy a number of properties with the most important being closure-finiteness (mapsTo) and weak topology (closed'). Note that this definition requires C and D to be closed subspaces. If C is not closed choose X to be C.

• cell (n : ℕ) : Type u

  The indexing type of the cells of dimension n.

• map (n : ℕ) (i : cell C n) : PartialEquiv (Fin n → ℝ) X

  The characteristic map of the n-cell given by the index i. This map is a bijection when restricting to ball 0 1, where we consider (Fin n → ℝ) endowed with the maximum metric.

• source_eq (n : ℕ) (i : cell C n) : (map n i).source = Metric.ball 0 1

  The source of every characteristic map of dimension n is (ball 0 1 : Set (Fin n → ℝ)).

• continuousOn (n : ℕ) (i : cell C n) : ContinuousOn (↑(map n i)) (Metric.closedBall 0 1)

  The characteristic maps are continuous when restricting to closedBall 0 1.

• continuousOn_symm (n : ℕ) (i : cell C n) : ContinuousOn (↑(map n i).symm) (map n i).target

  The inverse of the restriction to ball 0 1 is continuous on the image.

• pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun (ni : (n : ℕ) × cell C n) => ↑(map ni.fst ni.snd) '' Metric.ball 0 1

  The open cells are pairwise disjoint. Use RelCWComplex.pairwiseDisjoint or RelCWComplex.disjoint_openCell_of_ne instead.

• disjointBase' (n : ℕ) (i : cell C n) : Disjoint (↑(map n i) '' Metric.ball 0 1) D

  All open cells are disjoint with the base. Use RelCWComplex.disjointBase instead.

• mapsTo (n : ℕ) (i : cell C n) : ∃ (I : (m : ℕ) → Finset (cell C m)), Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' Metric.closedBall 0 1)

  The boundary of a cell is contained in the union of the base with a finite union of closed cells of a lower dimension. Use RelCWComplex.cellFrontier_subset_base_union_finite_closedCell instead.

• closed' (A : Set X) (hAC : A ⊆ C) : (∀ (n : ℕ) (j : cell C n), IsClosed (A ∩ ↑(map n j) '' Metric.closedBall 0 1)) ∧ IsClosed (A ∩ D) → IsClosed A

  A CW complex has weak topology, i.e. a set A in X is closed iff its intersection with every closed cell and D is closed. Use RelCWComplex.closed instead.

• isClosedBase : IsClosed D

  The base D is closed.

• union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell C n), ↑(map n j) '' Metric.closedBall 0 1 = C

  The union of all closed cells equals C. Use RelCWComplex.union instead.

class Topology.CWComplex {X : Type u} [TopologicalSpace X] (C : Set X) : Type (u + 1)

Characterizing when a subspace C of a topological space X is a CW complex. Note that this requires C to be closed. If C is not closed choose X to be C.

• cell (n : ℕ) : Type u

  The indexing type of the cells of dimension n.

• map (n : ℕ) (i : Topology.CWComplex.cell C n) : PartialEquiv (Fin n → ℝ) X

  The characteristic map of the n-cell given by the index i. This map is a bijection when restricting to ball 0 1, where we consider (Fin n → ℝ) endowed with the maximum metric.

• source_eq (n : ℕ) (i : Topology.CWComplex.cell C n) : (Topology.CWComplex.map n i).source = Metric.ball 0 1

  The source of every characteristic map of dimension n is (ball 0 1 : Set (Fin n → ℝ)).

• continuousOn (n : ℕ) (i : Topology.CWComplex.cell C n) : ContinuousOn (↑(Topology.CWComplex.map n i)) (Metric.closedBall 0 1)

  The characteristic maps are continuous when restricting to closedBall 0 1.

• continuousOn_symm (n : ℕ) (i : Topology.CWComplex.cell C n) : ContinuousOn (↑(Topology.CWComplex.map n i).symm) (Topology.CWComplex.map n i).target

  The inverse of the restriction to ball 0 1 is continuous on the image.

• pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun (ni : (n : ℕ) × Topology.CWComplex.cell C n) => ↑(Topology.CWComplex.map ni.fst ni.snd) '' Metric.ball 0 1

  The open cells are pairwise disjoint. Use CWComplex.pairwiseDisjoint or CWComplex.disjoint_openCell_of_ne instead.

• mapsTo' (n : ℕ) (i : Topology.CWComplex.cell C n) : ∃ (I : (m : ℕ) → Finset (Topology.CWComplex.cell C m)), Set.MapsTo (↑(Topology.CWComplex.map n i)) (Metric.sphere 0 1) (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(Topology.CWComplex.map m j) '' Metric.closedBall 0 1)

  The boundary of a cell is contained in a finite union of closed cells of a lower dimension. Use CWComplex.mapsTo or CWComplex.cellFrontier_subset_finite_closedCell instead.

• closed' (A : Set X) (hAC : A ⊆ C) : (∀ (n : ℕ) (j : Topology.CWComplex.cell C n), IsClosed (A ∩ ↑(Topology.CWComplex.map n j) '' Metric.closedBall 0 1)) → IsClosed A

  A CW complex has weak topology, i.e. a set A in X is closed iff its intersection with every closed cell is closed. Use CWComplex.closed instead.

• union' : ⋃ (n : ℕ), ⋃ (j : Topology.CWComplex.cell C n), ↑(Topology.CWComplex.map n j) '' Metric.closedBall 0 1 = C

  The union of all closed cells equals C. Use CWComplex.union instead.

@[instance 10000]

instance Topology.CWComplex.instRelCWComplex {X : Type u_1} [TopologicalSpace X] (C : Set X) [CWComplex C] : RelCWComplex C ∅

theorem Topology.CWComplex.cell_def {X : Type u_1} [TopologicalSpace X] (C : Set X) [CWComplex C] (n : ℕ) : cell C n = Topology.CWComplex.cell C n

theorem Topology.CWComplex.map_def {X : Type u_1} [TopologicalSpace X] (C : Set X) [CWComplex C] (n : ℕ) (i : Topology.CWComplex.cell C n) : map n i = Topology.CWComplex.map n i

def Topology.RelCWComplex.toCWComplex {X : Type u_1} [TopologicalSpace X] (C : Set X) [RelCWComplex C ∅] : CWComplex C

A relative CW complex with an empty base is an absolute CW complex.

theorem Topology.RelCWComplex.toCWComplex_cell {X : Type u_1} [TopologicalSpace X] (C : Set X) [RelCWComplex C ∅] (n : ℕ) : Topology.CWComplex.cell C n = cell C n

theorem Topology.RelCWComplex.toCWComplex_map {X : Type u_1} [TopologicalSpace X] (C : Set X) [RelCWComplex C ∅] (n : ℕ) (i : cell C n) : Topology.CWComplex.map n i = map n i

theorem Topology.RelCWComplex.toCWComplex_eq {X : Type u_1} [TopologicalSpace X] (C : Set X) [h : RelCWComplex C ∅] : CWComplex.instRelCWComplex C = h

def Topology.RelCWComplex.openCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (i : cell C n) : Set X

The open n-cell given by the index i. Use this instead of map n i '' ball 0 1 whenever possible.

def Topology.RelCWComplex.closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (i : cell C n) : Set X

The closed n-cell given by the index i. Use this instead of map n i '' closedBall 0 1 whenever possible.

def Topology.RelCWComplex.cellFrontier {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (i : cell C n) : Set X

The boundary of the n-cell given by the index i. Use this instead of map n i '' sphere 0 1 whenever possible.

theorem Topology.CWComplex.mapsTo {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] (n : ℕ) (i : cell C n) : ∃ (I : (m : ℕ) → Finset (cell C m)), Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' Metric.closedBall 0 1)

theorem Topology.RelCWComplex.pairwiseDisjoint {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] : Set.univ.PairwiseDisjoint fun (ni : (n : ℕ) × cell C n) => openCell ni.fst ni.snd

theorem Topology.RelCWComplex.disjointBase {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (i : cell C n) : Disjoint (openCell n i) D

theorem Topology.RelCWComplex.disjoint_openCell_of_ne {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {n m : ℕ} {i : cell C n} {j : cell C m} (ne : ⟨n, i⟩ ≠ ⟨m, j⟩) : Disjoint (openCell n i) (openCell m j)

theorem Topology.RelCWComplex.cellFrontier_subset_base_union_finite_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (i : cell C n) : ∃ (I : (m : ℕ) → Finset (cell C m)), cellFrontier n i ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

theorem Topology.CWComplex.cellFrontier_subset_finite_closedCell {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] (n : ℕ) (i : cell C n) : ∃ (I : (m : ℕ) → Finset (cell C m)), cellFrontier n i ⊆ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

theorem Topology.RelCWComplex.union {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] : D ∪ ⋃ (n : ℕ), ⋃ (j : cell C n), closedCell n j = C

theorem Topology.CWComplex.union {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] : ⋃ (n : ℕ), ⋃ (j : cell C n), closedCell n j = C

theorem Topology.RelCWComplex.openCell_subset_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (i : cell C n) : openCell n i ⊆ closedCell n i

theorem Topology.RelCWComplex.cellFrontier_subset_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (i : cell C n) : cellFrontier n i ⊆ closedCell n i

theorem Topology.RelCWComplex.cellFrontier_union_openCell_eq_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (i : cell C n) : cellFrontier n i ∪ openCell n i = closedCell n i

theorem Topology.RelCWComplex.map_zero_mem_openCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (i : cell C n) : ↑(map n i) 0 ∈ openCell n i

theorem Topology.RelCWComplex.map_zero_mem_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (i : cell C n) : ↑(map n i) 0 ∈ closedCell n i

theorem Topology.RelCWComplex.eq_of_eq_union_iUnion {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (I J : (n : ℕ) → Set (cell C n)) (hIJ : D ∪ ⋃ (n : ℕ), ⋃ (j : ↑(I n)), openCell n ↑j = D ∪ ⋃ (n : ℕ), ⋃ (j : ↑(J n)), openCell n ↑j) : I = J

theorem Topology.CWComplex.eq_of_eq_union_iUnion {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] (I J : (n : ℕ) → Set (cell C n)) (hIJ : ⋃ (n : ℕ), ⋃ (j : ↑(I n)), openCell n ↑j = ⋃ (n : ℕ), ⋃ (j : ↑(J n)), openCell n ↑j) : I = J

theorem Topology.RelCWComplex.isCompact_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {n : ℕ} {i : cell C n} : IsCompact (closedCell n i)

theorem Topology.RelCWComplex.isClosed_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] [T2Space X] {n : ℕ} {i : cell C n} : IsClosed (closedCell n i)

theorem Topology.RelCWComplex.isCompact_cellFrontier {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {n : ℕ} {i : cell C n} : IsCompact (cellFrontier n i)

theorem Topology.RelCWComplex.isClosed_cellFrontier {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] [T2Space X] {n : ℕ} {i : cell C n} : IsClosed (cellFrontier n i)

theorem Topology.RelCWComplex.closure_openCell_eq_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] [T2Space X] {n : ℕ} {j : cell C n} : closure (openCell n j) = closedCell n j

theorem Topology.RelCWComplex.closed {X : Type u_1} [t : TopologicalSpace X] (C : Set X) {D : Set X} [RelCWComplex C D] [T2Space X] (A : Set X) (asubc : A ⊆ C) : IsClosed A ↔ (∀ (n : ℕ) (j : cell C n), IsClosed (A ∩ closedCell n j)) ∧ IsClosed (A ∩ D)

theorem Topology.CWComplex.closed {X : Type u_1} [t : TopologicalSpace X] (C : Set X) [CWComplex C] [T2Space X] (A : Set X) (asubc : A ⊆ C) : IsClosed A ↔ ∀ (n : ℕ) (j : cell C n), IsClosed (A ∩ closedCell n j)

theorem Topology.RelCWComplex.closedCell_subset_complex {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (j : cell C n) : closedCell n j ⊆ C

theorem Topology.RelCWComplex.openCell_subset_complex {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (j : cell C n) : openCell n j ⊆ C

theorem Topology.RelCWComplex.cellFrontier_subset_complex {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (j : cell C n) : cellFrontier n j ⊆ C

theorem Topology.RelCWComplex.closedCell_zero_eq_singleton {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {j : cell C 0} : closedCell 0 j = {↑(map 0 j) ![]}

theorem Topology.RelCWComplex.openCell_zero_eq_singleton {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {j : cell C 0} : openCell 0 j = {↑(map 0 j) ![]}

theorem Topology.RelCWComplex.cellFrontier_zero_eq_empty {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {j : cell C 0} : cellFrontier 0 j = ∅

theorem Topology.RelCWComplex.base_subset_complex {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] : D ⊆ C

theorem Topology.RelCWComplex.isClosed {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] : IsClosed C

theorem Topology.RelCWComplex.union_iUnion_openCell_eq_complex {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] : D ∪ ⋃ (n : ℕ), ⋃ (j : cell C n), openCell n j = C

theorem Topology.CWComplex.iUnion_openCell_eq_complex {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] : ⋃ (n : ℕ), ⋃ (j : cell C n), openCell n j = C

theorem Topology.RelCWComplex.eq_of_not_disjoint_openCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {n : ℕ} {j : cell C n} {m : ℕ} {i : cell C m} (h : ¬Disjoint (openCell n j) (openCell m i)) : ⟨n, j⟩ = ⟨m, i⟩

The contrapositive of disjoint_openCell_of_ne.

theorem Topology.RelCWComplex.disjoint_base_iUnion_openCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] : Disjoint D (⋃ (n : ℕ), ⋃ (j : cell C n), openCell n j)

theorem Topology.RelCWComplex.isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] [T2Space X] {A : Set X} {n : ℕ} (hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed (A ∩ closedCell m j)) (j : cell C (n + 1)) (hD : IsClosed (A ∩ D)) : IsClosed (A ∩ cellFrontier (n + 1) j)

If for all m ≤ n and every i : cell C m the intersection A ∩ closedCell m j is closed and A ∩ D is closed then A ∩ cellFrontier (n + 1) j is closed for every j : cell C (n + 1).

theorem Topology.CWComplex.isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] [T2Space X] {A : Set X} {n : ℕ} (hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed (A ∩ closedCell m j)) (j : cell C (n + 1)) : IsClosed (A ∩ cellFrontier (n + 1) j)

theorem Topology.RelCWComplex.isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] [T2Space X] {A : Set X} (hAC : A ⊆ C) (hDA : IsClosed (A ∩ D)) (h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), IsClosed (A ∩ openCell n j) ∨ IsClosed (A ∩ closedCell n j)) : IsClosed A

If for every cell either A ∩ openCell n j or A ∩ closedCell n j is closed then A is closed.

theorem Topology.RelCWComplex.isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] [T2Space X] {A : Set X} (hAC : A ⊆ C) (hDA : IsClosed (A ∩ D)) (h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), Disjoint A (openCell n j) ∨ IsClosed (A ∩ closedCell n j)) : IsClosed A

If for every cell either A ∩ openCell n j is empty or A ∩ closedCell n j is closed then A is closed.

theorem Topology.CWComplex.isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] [T2Space X] {A : Set X} (hAC : A ⊆ C) (h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), IsClosed (A ∩ openCell n j) ∨ IsClosed (A ∩ closedCell n j)) : IsClosed A

If for every cell either A ∩ openCell n j or A ∩ closedCell n j is closed then A is closed.

theorem Topology.CWComplex.isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] [T2Space X] {A : Set X} (hAC : A ⊆ C) (h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), Disjoint A (openCell n j) ∨ IsClosed (A ∩ closedCell n j)) : IsClosed A

If for every cell either A ∩ openCell n j is empty or A ∩ closedCell n j is closed then A is closed.

theorem Topology.RelCWComplex.cellFrontier_subset_finite_openCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (n : ℕ) (i : cell C n) : ∃ (I : (m : ℕ) → Finset (cell C m)), cellFrontier n i ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, openCell m j

A version of cellFrontier_subset_base_union_finite_closedCell using open cells: The boundary of a cell is contained in a finite union of open cells of a lower dimension.

theorem Topology.CWComplex.cellFrontier_subset_finite_openCell {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] (n : ℕ) (i : cell C n) : ∃ (I : (m : ℕ) → Finset (cell C m)), cellFrontier n i ⊆ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, openCell m j

A version of cellFrontier_subset_finite_closedCell using open cells: The boundary of a cell is contained in a finite union of open cells of a lower dimension.

structure Topology.RelCWComplex.Subcomplex {X : Type u_1} [t : TopologicalSpace X] (C : Set X) {D : Set X} [RelCWComplex C D] : Type u_1

A subcomplex is a closed subspace of a CW complex that is the union of open cells of the CW complex.

• carrier : Set X

  The underlying set of the subcomplex.

• I (n : ℕ) : Set (cell C n)

  The indexing set of cells of the subcomplex.

• closed' : IsClosed self.carrier

  A subcomplex is closed.

• union' : D ∪ ⋃ (n : ℕ), ⋃ (j : ↑(self.I n)), openCell n ↑j = self.carrier

  The union of all open cells of the subcomplex equals the subcomplex.

instance Topology.RelCWComplex.Subcomplex.instSetLike {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] : SetLike (Subcomplex C) X

instance Topology.RelCWComplex.Subcomplex.instPartialOrder {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] : PartialOrder (Subcomplex C)

theorem Topology.RelCWComplex.Subcomplex.mem_carrier {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {E : Subcomplex C} {x : X} : x ∈ E.carrier ↔ x ∈ ↑E

theorem Topology.RelCWComplex.Subcomplex.coe_eq_carrier {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {E : Subcomplex C} : ↑E = E.carrier

theorem Topology.RelCWComplex.Subcomplex.ext {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {E F : Subcomplex C} (h : ∀ (x : X), x ∈ E ↔ x ∈ F) : E = F

theorem Topology.RelCWComplex.Subcomplex.ext_iff {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {E F : Subcomplex C} : E = F ↔ ∀ (x : X), x ∈ E ↔ x ∈ F

theorem Topology.RelCWComplex.Subcomplex.eq_iff {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (E F : Subcomplex C) : E = F ↔ ↑E = ↑F

def Topology.RelCWComplex.Subcomplex.copy {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) (F : Set X) (hF : F = ↑E) (J : (n : ℕ) → Set (cell C n)) (hJ : J = E.I) : Subcomplex C

Copy of a Subcomplex with a new carrier equal to the old one. Useful to fix definitional equalities.

@[simp]

theorem Topology.RelCWComplex.Subcomplex.coe_copy {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) (F : Set X) (hF : F = ↑E) (J : (n : ℕ) → Set (cell C n)) (hJ : J = E.I) : ↑(E.copy F hF J hJ) = F

theorem Topology.RelCWComplex.Subcomplex.copy_eq {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) (F : Set X) (hF : F = ↑E) (J : (n : ℕ) → Set (cell C n)) (hJ : J = E.I) : E.copy F hF J hJ = E

theorem Topology.RelCWComplex.Subcomplex.union {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) : D ∪ ⋃ (n : ℕ), ⋃ (j : ↑(E.I n)), openCell n ↑j = ↑E

theorem Topology.RelCWComplex.Subcomplex.closed {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) : IsClosed ↑E

theorem Topology.CWComplex.Subcomplex.union {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [CWComplex C] {E : Subcomplex C} : ⋃ (n : ℕ), ⋃ (j : ↑(E.I n)), openCell n ↑j = ↑E

def Topology.RelCWComplex.Subcomplex.mk' {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (E : Set X) (I : (n : ℕ) → Set (cell C n)) (closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E) (union : D ∪ ⋃ (n : ℕ), ⋃ (j : ↑(I n)), openCell n ↑j = E) : Subcomplex C

An alternative version of Subcomplex.mk: Instead of requiring that E is closed it requires that for every cell of the subcomplex the corresponding closed cell is a subset of E.

theorem Topology.RelCWComplex.Subcomplex.coe_mk' {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (E : Set X) (I : (n : ℕ) → Set (cell C n)) (closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E) (union : D ∪ ⋃ (n : ℕ), ⋃ (j : ↑(I n)), openCell n ↑j = E) : ↑(mk' C E I closedCell_subset union) = E

theorem Topology.RelCWComplex.Subcomplex.mk'_I {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (E : Set X) (I : (n : ℕ) → Set (cell C n)) (closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E) (union : D ∪ ⋃ (n : ℕ), ⋃ (j : ↑(I n)), openCell n ↑j = E) (n : ℕ) : (mk' C E I closedCell_subset union).I n = I n

def Topology.CWComplex.Subcomplex.mk' {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) [CWComplex C] (E : Set X) (I : (n : ℕ) → Set (cell C n)) (closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E) (union : ⋃ (n : ℕ), ⋃ (j : ↑(I n)), openCell n ↑j = E) : Subcomplex C

An alternative version of Subcomplex.mk: Instead of requiring that E is closed it requires that for every cell of the subcomplex the corresponding closed cell is a subset of E.

theorem Topology.CWComplex.Subcomplex.coe_mk' {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) [CWComplex C] (E : Set X) (I : (n : ℕ) → Set (cell C n)) (closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E) (union : ⋃ (n : ℕ), ⋃ (j : ↑(I n)), openCell n ↑j = E) : ↑(mk' C E I closedCell_subset union) = E

theorem Topology.CWComplex.Subcomplex.mk'_I {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) [CWComplex C] (E : Set X) (I : (n : ℕ) → Set (cell C n)) (closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E) (union : ⋃ (n : ℕ), ⋃ (j : ↑(I n)), openCell n ↑j = E) (n : ℕ) : (mk' C E I closedCell_subset union).I n = I n

def Topology.RelCWComplex.Subcomplex.mk'' {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (E : Set X) (I : (n : ℕ) → Set (cell C n)) [RelCWComplex E D] (union : D ∪ ⋃ (n : ℕ), ⋃ (j : ↑(I n)), openCell n ↑j = E) : Subcomplex C

An alternative version of Subcomplex.mk: Instead of requiring that E is closed it requires that E is a CW-complex.

theorem Topology.RelCWComplex.Subcomplex.coe_mk'' {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (E : Set X) (I : (n : ℕ) → Set (cell C n)) [RelCWComplex E D] (union : D ∪ ⋃ (n : ℕ), ⋃ (j : ↑(I n)), openCell n ↑j = E) : ↑(mk'' C E I union) = E

theorem Topology.RelCWComplex.Subcomplex.mk''_I {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (E : Set X) (I : (n : ℕ) → Set (cell C n)) [RelCWComplex E D] (union : D ∪ ⋃ (n : ℕ), ⋃ (j : ↑(I n)), openCell n ↑j = E) (n : ℕ) : (mk'' C E I union).I n = I n

def Topology.CWComplex.Subcomplex.mk'' {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) [h : CWComplex C] (E : Set X) (I : (n : ℕ) → Set (cell C n)) [CWComplex E] (union : ⋃ (n : ℕ), ⋃ (j : ↑(I n)), openCell n ↑j = E) : Subcomplex C

An alternative version of Subcomplex.mk: Instead of requiring that E is closed it requires that E is a CW-complex.

theorem Topology.CWComplex.Subcomplex.coe_mk'' {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) [h : CWComplex C] (E : Set X) (I : (n : ℕ) → Set (cell C n)) [CWComplex E] (union : ⋃ (n : ℕ), ⋃ (j : ↑(I n)), openCell n ↑j = E) : ↑(mk'' C E I union) = E

theorem Topology.CWComplex.Subcomplex.mk''_I {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) [h : CWComplex C] (E : Set X) (I : (n : ℕ) → Set (cell C n)) [CWComplex E] (union : ⋃ (n : ℕ), ⋃ (j : ↑(I n)), openCell n ↑j = E) (n : ℕ) : (mk'' C E I union).I n = I n

theorem Topology.RelCWComplex.Subcomplex.subset_complex {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) : ↑E ⊆ C

theorem Topology.RelCWComplex.Subcomplex.base_subset {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) : D ⊆ ↑E

@[irreducible]

def Topology.RelCWComplex.skeletonLT {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (n : ℕ∞) : Subcomplex C

A non-standard definition of the n-skeleton of a CW complex for n ∈ ℕ ∪ {∞}. This allows the base case of induction to be about the base instead of being about the union of the base and some points. The standard skeleton is defined in terms of skeletonLT. skeletonLT is preferred in statements. You should then derive the statement about skeleton.

theorem Topology.RelCWComplex.coe_skeletonLT {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (n : ℕ∞) : ↑(skeletonLT C n) = D ∪ ⋃ (m : ℕ), ⋃ (_ : ↑m < n), ⋃ (j : cell C m), closedCell m j

theorem Topology.RelCWComplex.skeletonLT_I {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (n : ℕ∞) (l : ℕ) : (skeletonLT C n).I l = {x : cell C l | ↑l < n}

@[reducible, inline]

abbrev Topology.RelCWComplex.skeleton {X : Type u_1} [t : TopologicalSpace X] [T2Space X] (C : Set X) {D : Set X} [RelCWComplex C D] (n : ℕ∞) : Subcomplex C

The n-skeleton of a CW complex, for n ∈ ℕ ∪ {∞}. For statements use skeletonLT instead and then derive the statement about skeleton.

theorem Topology.RelCWComplex.skeletonLT_zero_eq_base {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] : ↑(skeletonLT C 0) = D

theorem Topology.CWComplex.skeletonLT_zero_eq_empty {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [CWComplex C] : ↑(skeletonLT C 0) = ∅

@[simp]

theorem Topology.RelCWComplex.skeletonLT_top {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] : ↑(skeletonLT C ⊤) = C

@[simp]

theorem Topology.RelCWComplex.skeleton_top {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] : ↑(skeleton C ⊤) = C

theorem Topology.RelCWComplex.skeletonLT_mono {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] {n m : ℕ∞} (h : m ≤ n) : ↑(skeletonLT C m) ⊆ ↑(skeletonLT C n)

theorem Topology.RelCWComplex.skeletonLT_monotone {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] : Monotone (skeletonLT C)

theorem Topology.RelCWComplex.skeleton_mono {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] {n m : ℕ∞} (h : m ≤ n) : ↑(skeleton C m) ⊆ ↑(skeleton C n)

theorem Topology.RelCWComplex.skeleton_monotone {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] : Monotone (skeleton C)

theorem Topology.RelCWComplex.closedCell_subset_skeletonLT {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (n : ℕ) (j : cell C n) : closedCell n j ⊆ ↑(skeletonLT C (↑n + 1))

theorem Topology.RelCWComplex.closedCell_subset_skeleton {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (n : ℕ) (j : cell C n) : closedCell n j ⊆ ↑(skeleton C ↑n)

theorem Topology.RelCWComplex.openCell_subset_skeletonLT {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (n : ℕ) (j : cell C n) : openCell n j ⊆ ↑(skeletonLT C (↑n + 1))

theorem Topology.RelCWComplex.openCell_subset_skeleton {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (n : ℕ) (j : cell C n) : openCell n j ⊆ ↑(skeleton C ↑n)

theorem Topology.RelCWComplex.cellFrontier_subset_skeletonLT {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (n : ℕ) (j : cell C n) : cellFrontier n j ⊆ ↑(skeletonLT C ↑n)

theorem Topology.RelCWComplex.cellFrontier_subset_skeleton {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (n : ℕ) (j : cell C (n + 1)) : cellFrontier (n + 1) j ⊆ ↑(skeleton C ↑n)

theorem Topology.RelCWComplex.iUnion_cellFrontier_subset_skeletonLT {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (l : ℕ) : ⋃ (j : cell C l), cellFrontier l j ⊆ ↑(skeletonLT C ↑l)

theorem Topology.RelCWComplex.iUnion_cellFrontier_subset_skeleton {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (l : ℕ) : ⋃ (j : cell C l), cellFrontier l j ⊆ ↑(skeleton C ↑l)

theorem Topology.RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (n : ℕ) : ↑(skeletonLT C ↑n) ∪ ⋃ (j : cell C n), closedCell n j = ↑(skeletonLT C (↑n + 1))

theorem Topology.RelCWComplex.skeleton_union_iUnion_closedCell_eq_skeleton_succ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (n : ℕ) : ↑(skeleton C ↑n) ∪ ⋃ (j : cell C (n + 1)), closedCell (n + 1) j = ↑(skeleton C (↑n + 1))

theorem Topology.RelCWComplex.iUnion_openCell_eq_skeletonLT {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (n : ℕ∞) : D ∪ ⋃ (m : ℕ), ⋃ (_ : ↑m < n), ⋃ (j : cell C m), openCell m j = ↑(skeletonLT C n)

A version of the definition of skeletonLT with open cells.

theorem Topology.CWComplex.iUnion_openCell_eq_skeletonLT {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [CWComplex C] (n : ℕ∞) : ⋃ (m : ℕ), ⋃ (_ : ↑m < n), ⋃ (j : cell C m), openCell m j = ↑(skeletonLT C n)

theorem Topology.RelCWComplex.iUnion_openCell_eq_skeleton {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] (n : ℕ∞) : D ∪ ⋃ (m : ℕ), ⋃ (_ : ↑m < n + 1), ⋃ (j : cell C m), openCell m j = ↑(skeleton C n)

theorem Topology.CWComplex.iUnion_openCell_eq_skeleton {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [CWComplex C] (n : ℕ∞) : ⋃ (m : ℕ), ⋃ (_ : ↑m < n + 1), ⋃ (j : cell C m), openCell m j = ↑(skeleton C n)

theorem Topology.RelCWComplex.iUnion_skeletonLT_eq_complex {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] : ⋃ (n : ℕ), ↑(skeletonLT C ↑n) = C

theorem Topology.RelCWComplex.iUnion_skeleton_eq_complex {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] : ⋃ (n : ℕ), ↑(skeleton C ↑n) = C

theorem Topology.RelCWComplex.mem_skeletonLT_iff {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] {n : ℕ∞} {x : X} : x ∈ skeletonLT C n ↔ x ∈ D ∨ ∃ (m : ℕ) (_ : ↑m < n) (j : cell C m), x ∈ openCell m j

theorem Topology.CWComplex.mem_skeletonLT_iff {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [CWComplex C] {n : ℕ∞} {x : X} : x ∈ skeletonLT C n ↔ ∃ (m : ℕ) (_ : ↑m < n) (j : cell C m), x ∈ openCell m j

theorem Topology.RelCWComplex.mem_skeleton_iff {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] {n : ℕ∞} {x : X} : x ∈ skeleton C n ↔ x ∈ D ∨ ∃ (m : ℕ) (_ : ↑m ≤ n) (j : cell C m), x ∈ openCell m j

theorem Topology.CWComplex.exists_mem_openCell_of_mem_skeleton {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [T2Space X] [CWComplex C] {n : ℕ∞} {x : X} : x ∈ skeleton C n ↔ ∃ (m : ℕ) (_ : ↑m ≤ n) (j : cell C m), x ∈ openCell m j

theorem Topology.RelCWComplex.disjoint_skeletonLT_openCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] {n : ℕ∞} {m : ℕ} {j : cell C m} (hnm : n ≤ ↑m) : Disjoint (↑(skeletonLT C n)) (openCell m j)

A skeleton and an open cell of a higher dimension are disjoint.

theorem Topology.RelCWComplex.disjoint_skeleton_openCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] {n : ℕ∞} {m : ℕ} {j : cell C m} (nlem : n < ↑m) : Disjoint (↑(skeleton C n)) (openCell m j)

A skeleton and an open cell of a higher dimension are disjoint.

theorem Topology.RelCWComplex.skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] {n : ℕ∞} {m : ℕ} {j : cell C m} (hnm : n ≤ ↑m) : ↑(skeletonLT C n) ∩ closedCell m j = ↑(skeletonLT C n) ∩ cellFrontier m j

A skeleton intersected with a closed cell of a higher dimension is the skeleton intersected with the boundary of the cell.

theorem Topology.RelCWComplex.skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] {n : ℕ∞} {m : ℕ} {j : cell C m} (hnm : n < ↑m) : ↑(skeleton C n) ∩ closedCell m j = ↑(skeleton C n) ∩ cellFrontier m j

Version of skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier using skeleton.

theorem Topology.RelCWComplex.disjoint_interior_base_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] {n : ℕ} {j : cell C n} : Disjoint (interior D) (closedCell n j)

theorem Topology.RelCWComplex.disjoint_interior_base_iUnion_closedCell {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [T2Space X] [RelCWComplex C D] : Disjoint (interior D) (⋃ (n : ℕ), ⋃ (j : cell C n), closedCell n j)