Topological pairs of nested subsets, and maps between pairs of subsets

A continuous map g : X ⟶ Y carrying a subset B ⊆ X into a subset B' ⊆ Y induces a map of topological pairs TopPair.ofSubsetMap g hB : (X, B) ⟶ (Y, B'), where the pairs are TopPair.ofSubset B and TopPair.ofSubset B', and a homotopy that keeps B inside B' at every time induces a homotopy of maps of pairs TopPair.ofSubsetHomotopy.

Nested subsets s ⊆ t of a topological space form the topological pair TopPair.ofInclusion : (t, s), whose embedding is Set.inclusion. TopPair.ofSubset is the special case t = X; the general form is the one a filtration of a space, such as the skeletal filtration of a CW complex, produces. A continuous map t → t' carrying s into s' induces a map of such pairs TopPair.ofInclusionMap, and a homotopy that keeps s inside s' at every time induces a homotopy of maps of pairs TopPair.ofInclusionHomotopy.

A map of pairs which is an isomorphism of the ambient spaces and is surjective on the subspaces is an isomorphism of pairs (TopPair.isIso_of_isIso_fst_of_surjective_snd): the inverse on the subspaces is continuous because subspaces are embedded.

The disjoint union TopPair.sigma P = (Σ i, Xᵢ, Σ i, Aᵢ) of a family of pairs P i = (Xᵢ, Aᵢ), with the inclusions TopPair.sigmaι P i of the summands, is the coproduct of the family in TopPair (TopPair.sigmaCofanIsColimit). Relative singular homology is additive along it.

@[reducible, inline]

abbrev TopPair.ofInclusion {X : TopCat} {s t : Set ↑X} (h : s ⊆ t) : TopPair

The topological pair (t, s) determined by nested subsets s ⊆ t of a topological space, with the inclusion of s into t as its embedding.

Equations

• TopPair.ofInclusion h = TopPair.of (TopCat.ofHom (ContinuousMap.inclusion h)) ⋯

def TopPair.ofSubsetMap {X Y : TopCat} (g : X ⟶ Y) {B : Set ↑X} {B' : Set ↑Y} (hB : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom g)) B B') : ofSubset B ⟶ ofSubset B'

A continuous map g : X ⟶ Y carrying B into B' induces a map of pairs (X, B) ⟶ (Y, B').

Equations

• TopPair.ofSubsetMap g hB = TopPair.ofHom g (TopCat.ofHom { toFun := Set.MapsTo.restrict (⇑(CategoryTheory.ConcreteCategory.hom g)) B B' hB, continuous_toFun := ⋯ }) ⋯

@[simp]

theorem TopPair.ofSubsetMap_fst_apply {X Y : TopCat} (g : X ⟶ Y) {B : Set ↑X} {B' : Set ↑Y} (hB : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom g)) B B') (x : ↑fst) : (CategoryTheory.ConcreteCategory.hom (Hom.fst (ofSubsetMap g hB))) x = (CategoryTheory.ConcreteCategory.hom g) x

@[simp]

theorem TopPair.ofSubsetMap_snd_apply {X Y : TopCat} (g : X ⟶ Y) {B : Set ↑X} {B' : Set ↑Y} (hB : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom g)) B B') (x : ↑snd) : ↑((CategoryTheory.ConcreteCategory.hom (Hom.snd (ofSubsetMap g hB))) x) = (CategoryTheory.ConcreteCategory.hom g) ↑x

@[simp]

theorem TopPair.ofSubsetMap_id {X : TopCat} {B : Set ↑X} (h : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X))) B B) : ofSubsetMap (CategoryTheory.CategoryStruct.id X) h = CategoryTheory.CategoryStruct.id (ofSubset B)

theorem TopPair.ofSubsetMap_comp {X Y Z : TopCat} (g : X ⟶ Y) (g' : Y ⟶ Z) {B : Set ↑X} {B' : Set ↑Y} {B'' : Set ↑Z} (hB : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom g)) B B') (hB' : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom g')) B' B'') (h : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp g g'))) B B'') : ofSubsetMap (CategoryTheory.CategoryStruct.comp g g') h = CategoryTheory.CategoryStruct.comp (ofSubsetMap g hB) (ofSubsetMap g' hB')

theorem TopPair.ofSubsetMap_comp_assoc {X Y Z : TopCat} (g : X ⟶ Y) (g' : Y ⟶ Z) {B : Set ↑X} {B' : Set ↑Y} {B'' : Set ↑Z} (hB : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom g)) B B') (hB' : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom g')) B' B'') (h : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp g g'))) B B'') {Z✝ : TopPair} (h✝ : ofSubset B'' ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (ofSubsetMap (CategoryTheory.CategoryStruct.comp g g') h) h✝ = CategoryTheory.CategoryStruct.comp (ofSubsetMap g hB) (CategoryTheory.CategoryStruct.comp (ofSubsetMap g' hB') h✝)

def TopPair.ofSubsetHomotopy {X Y : TopCat} {B : Set ↑X} {B' : Set ↑Y} {g₀ g₁ : X ⟶ Y} (F : (TopCat.Hom.hom g₀).Homotopy (TopCat.Hom.hom g₁)) (hF : ∀ (τ : ↑unitInterval), ∀ x ∈ B, F (τ, x) ∈ B') : Homotopy (ofSubsetMap g₀ ⋯) (ofSubsetMap g₁ ⋯)

A homotopy between maps X ⟶ Y which keeps B inside B' at every time induces a homotopy between the induced maps of pairs (X, B) ⟶ (Y, B').

Equations

• One or more equations did not get rendered due to their size.

def TopPair.ofInclusionMap {X Y : TopCat} {s t : Set ↑X} {s' t' : Set ↑Y} (hst : s ⊆ t) (hst' : s' ⊆ t') (g : C(↑t, ↑t')) (hg : ∀ (x : ↑t), ↑x ∈ s → ↑(g x) ∈ s') : ofInclusion hst ⟶ ofInclusion hst'

A continuous map g : t → t' carrying s into s' induces a map of pairs (t, s) ⟶ (t', s').

Equations

• TopPair.ofInclusionMap hst hst' g hg = TopPair.ofHom (TopCat.ofHom g) (TopCat.ofHom { toFun := fun (x : ↑s) => ⟨↑(g ⟨↑x, ⋯⟩), ⋯⟩, continuous_toFun := ⋯ }) ⋯

@[simp]

theorem TopPair.ofInclusionMap_fst_apply {X Y : TopCat} {s t : Set ↑X} {s' t' : Set ↑Y} {hst : s ⊆ t} {hst' : s' ⊆ t'} (g : C(↑t, ↑t')) (hg : ∀ (x : ↑t), ↑x ∈ s → ↑(g x) ∈ s') (x : ↑t) : (CategoryTheory.ConcreteCategory.hom (Hom.fst (ofInclusionMap hst hst' g hg))) x = g x

@[simp]

theorem TopPair.ofInclusionMap_snd_apply {X Y : TopCat} {s t : Set ↑X} {s' t' : Set ↑Y} {hst : s ⊆ t} {hst' : s' ⊆ t'} (g : C(↑t, ↑t')) (hg : ∀ (x : ↑t), ↑x ∈ s → ↑(g x) ∈ s') (x : ↑s) : ↑((CategoryTheory.ConcreteCategory.hom (Hom.snd (ofInclusionMap hst hst' g hg))) x) = ↑(g ⟨↑x, ⋯⟩)

@[simp]

theorem TopPair.ofInclusionMap_id {X : TopCat} {s t : Set ↑X} {hst : s ⊆ t} : ofInclusionMap hst hst (ContinuousMap.id ↑t) ⋯ = CategoryTheory.CategoryStruct.id (ofInclusion hst)

theorem TopPair.ofInclusionMap_comp {X Y Z : TopCat} {s t : Set ↑X} {s' t' : Set ↑Y} {s'' t'' : Set ↑Z} {hst : s ⊆ t} {hst' : s' ⊆ t'} (hst'' : s'' ⊆ t'') (g : C(↑t, ↑t')) (g' : C(↑t', ↑t'')) (hg : ∀ (x : ↑t), ↑x ∈ s → ↑(g x) ∈ s') (hg' : ∀ (x : ↑t'), ↑x ∈ s' → ↑(g' x) ∈ s'') : ofInclusionMap hst hst'' (g'.comp g) ⋯ = CategoryTheory.CategoryStruct.comp (ofInclusionMap hst hst' g hg) (ofInclusionMap hst' hst'' g' hg')

theorem TopPair.ofInclusionMap_comp_assoc {X Y Z : TopCat} {s t : Set ↑X} {s' t' : Set ↑Y} {s'' t'' : Set ↑Z} {hst : s ⊆ t} {hst' : s' ⊆ t'} (hst'' : s'' ⊆ t'') (g : C(↑t, ↑t')) (g' : C(↑t', ↑t'')) (hg : ∀ (x : ↑t), ↑x ∈ s → ↑(g x) ∈ s') (hg' : ∀ (x : ↑t'), ↑x ∈ s' → ↑(g' x) ∈ s'') {Z✝ : TopPair} (h : ofInclusion hst'' ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (ofInclusionMap hst hst'' (g'.comp g) ⋯) h = CategoryTheory.CategoryStruct.comp (ofInclusionMap hst hst' g hg) (CategoryTheory.CategoryStruct.comp (ofInclusionMap hst' hst'' g' hg') h)

def TopPair.ofInclusionHomotopy {X Y : TopCat} {s t : Set ↑X} {s' t' : Set ↑Y} {hst : s ⊆ t} {hst' : s' ⊆ t'} {g₀ g₁ : C(↑t, ↑t')} (F : g₀.Homotopy g₁) (hF : ∀ (τ : ↑unitInterval) (x : ↑t), ↑x ∈ s → ↑(F (τ, x)) ∈ s') : Homotopy (ofInclusionMap hst hst' g₀ ⋯) (ofInclusionMap hst hst' g₁ ⋯)

A homotopy between maps t → t' which keeps s inside s' at every time induces a homotopy between the induced maps of pairs (t, s) ⟶ (t', s').

Equations

• One or more equations did not get rendered due to their size.

theorem TopPair.isIso_of_isIso_fst_of_surjective_snd {P Q : TopPair} (f : P ⟶ Q) [CategoryTheory.IsIso (Hom.fst f)] (hf : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Hom.snd f))) : CategoryTheory.IsIso f

A map of topological pairs which is an isomorphism of the ambient spaces and is surjective on the subspaces is an isomorphism of pairs. The inverse on the subspaces is continuous because the subspace of the source is embedded in its ambient space.

@[reducible, inline]

abbrev TopPair.sigma {ι : Type u} (P : ι → TopPair) : TopPair

The disjoint union ∐ᵢ (Xᵢ, Aᵢ) = (Σ i, Xᵢ, Σ i, Aᵢ) of a family of topological pairs, the coproduct of the family in TopPair (TopPair.sigmaCofanIsColimit).

Equations

• TopPair.sigma P = TopPair.of (TopCat.ofHom { toFun := Sigma.map id fun (i : ι) => ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map), continuous_toFun := ⋯ }) ⋯

@[reducible, inline]

abbrev TopPair.sigmaι {ι : Type u} (P : ι → TopPair) (i : ι) : P i ⟶ sigma P

The inclusion (Xᵢ, Aᵢ) ⟶ ∐ᵢ (Xᵢ, Aᵢ) of a summand into the disjoint union of a family of topological pairs.

Equations

• TopPair.sigmaι P i = TopPair.ofHom (TopCat.sigmaι (fun (i : ι) => TopPair.fst) i) (TopCat.sigmaι (fun (i : ι) => TopPair.snd) i) ⋯

@[reducible, inline]

abbrev TopPair.sigmaCofan {ι : Type u} (P : ι → TopPair) : CategoryTheory.Limits.Cofan P

The cofan of a family of topological pairs given by their disjoint union.

Equations

• TopPair.sigmaCofan P = CategoryTheory.Limits.Cofan.mk (TopPair.sigma P) (TopPair.sigmaι P)

def TopPair.sigmaCofanIsColimit {ι : Type u} (P : ι → TopPair) : CategoryTheory.Limits.IsColimit (sigmaCofan P)

The disjoint union of a family of topological pairs is their coproduct in TopPair.

Equations

• One or more equations did not get rendered due to their size.