A CW complex relative to a subcomplex

Let E be a subcomplex of a relative CW complex (C, D). Mathlib makes E itself a CW complex relative to D (Topology.RelCWComplex.Subcomplex.instRelCWComplex), with the cells of C that lie in E. This file supplies the complementary structure: C is a CW complex relative to E, whose n-cells are the n-cells of C that do not lie in E, with the same characteristic maps (Topology.RelCWComplex.Subcomplex.relCWComplex). Together the two structures split the cells of C along E; this is how cellular invariants of the pair (C, E), such as relative cellular homology and the relative Euler characteristic, are computed from those of C and E.

The structure is not an instance: the base of a relative CW complex is an outParam, so C cannot carry one instance for each of its subcomplexes.

A subcomplex F contained in another subcomplex E uses a subset of the cells of E (Topology.RelCWComplex.Subcomplex.le_iff_I_subset), so it is a subcomplex of the CW complex E (Topology.RelCWComplex.Subcomplex.ofLE). Combined with the relative structure, this makes E a CW complex relative to F, and so lets cellular arguments run along a filtration of C by subcomplexes.

Main definitions and results

• Topology.RelCWComplex.Subcomplex.relCWComplex: the CW structure on C relative to a subcomplex E.
• Topology.RelCWComplex.Subcomplex.relCWComplexCellEquiv: its n-cells are the n-cells of C not in E.
• Topology.RelCWComplex.Subcomplex.finite_relCWComplex: it is finite when C is.
• Topology.RelCWComplex.Subcomplex.le_iff_I_subset: one subcomplex lies in another exactly when its cells do.
• Topology.RelCWComplex.Subcomplex.ofLE: a subcomplex F ≤ E, as a subcomplex of E.
• Topology.RelCWComplex.coe_skeletonLT_skeletonLT: the skeleta of a skeleton of C are skeleta of C.

References

• A. Hatcher, Algebraic Topology, Chapter 0 and Section 2.2, for CW pairs (X, A) with A a subcomplex.

@[instance_reducible]

def Topology.RelCWComplex.Subcomplex.relCWComplex {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) : RelCWComplex C ↑E

A relative CW complex (C, D) is a CW complex relative to any subcomplex E: its n-cells are the n-cells of C that do not lie in E, with the characteristic maps of C.

noncomputable def Topology.RelCWComplex.Subcomplex.relCWComplexCellEquiv {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) (n : ℕ) : cell C n ≃ ↑(E.I n)ᶜ

The n-cells of C relative to a subcomplex E are the n-cells of C not in E.

@[simp]

theorem Topology.RelCWComplex.Subcomplex.map_relCWComplex {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) (n : ℕ) (i : cell C n) : map n i = map n ↑((E.relCWComplexCellEquiv n) i)

The characteristic maps of C relative to E are characteristic maps of C.

@[simp]

theorem Topology.RelCWComplex.Subcomplex.openCell_relCWComplex {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) (n : ℕ) (i : cell C n) : openCell n i = openCell n ↑((E.relCWComplexCellEquiv n) i)

The open cells of C relative to E are open cells of C.

@[simp]

theorem Topology.RelCWComplex.Subcomplex.closedCell_relCWComplex {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) (n : ℕ) (i : cell C n) : closedCell n i = closedCell n ↑((E.relCWComplexCellEquiv n) i)

The closed cells of C relative to E are closed cells of C.

@[simp]

theorem Topology.RelCWComplex.Subcomplex.cellFrontier_relCWComplex {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) (n : ℕ) (i : cell C n) : cellFrontier n i = cellFrontier n ↑((E.relCWComplexCellEquiv n) i)

The boundaries of the cells of C relative to E are boundaries of cells of C.

theorem Topology.RelCWComplex.Subcomplex.finiteDimensional_relCWComplex {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D : Set X} [RelCWComplex C D] [FiniteDimensional C] (E : Subcomplex C) : FiniteDimensional C

The CW structure on C relative to a subcomplex is finite dimensional when C is.

theorem Topology.RelCWComplex.Subcomplex.finiteType_relCWComplex {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D : Set X} [RelCWComplex C D] [FiniteType C] (E : Subcomplex C) : FiniteType C

The CW structure on C relative to a subcomplex is of finite type when C is.

theorem Topology.RelCWComplex.Subcomplex.finite_relCWComplex {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D : Set X} [RelCWComplex C D] [Finite C] (E : Subcomplex C) : Finite C

The CW structure on C relative to a subcomplex is finite when C is.

theorem Topology.RelCWComplex.Subcomplex.le_iff_I_subset {X : Type u_1} [TopologicalSpace X] {C D : Set X} [RelCWComplex C D] {F E : Subcomplex C} : F ≤ E ↔ ∀ (n : ℕ), F.I n ⊆ E.I n

One subcomplex lies in another exactly when its cells are among the cells of the other.

def Topology.RelCWComplex.Subcomplex.ofLE {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D : Set X} [RelCWComplex C D] {F E : Subcomplex C} (h : F ≤ E) : Subcomplex ↑E

A subcomplex F of C contained in a subcomplex E, as a subcomplex of the CW complex E. Its cells are the cells of E that are cells of F.

@[simp]

theorem Topology.RelCWComplex.Subcomplex.coe_ofLE {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D : Set X} [RelCWComplex C D] {F E : Subcomplex C} (h : F ≤ E) : ↑(ofLE h) = ↑F

As a set, ofLE h is the subcomplex F.

@[simp]

theorem Topology.RelCWComplex.Subcomplex.ofLE_I {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D : Set X} [RelCWComplex C D] {F E : Subcomplex C} (h : F ≤ E) (n : ℕ) : (ofLE h).I n = Subtype.val ⁻¹' F.I n

The n-cells of ofLE h are the n-cells of E that are n-cells of F.

@[simp]

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

For n ≤ m, the subcomplex skeletonLT C m, viewed as a relative CW complex in its own right, has the same skeletonLT _ n as C: both are the union of the base D with the cells of dimension strictly less than n.