Triples of topological spaces

A triple (X, A, B) of topological spaces consists of subspaces B ⊆ A ⊆ X, recorded here as a pair of composable embeddings B ⟶ A ⟶ X in TopCat. Triples carry the long exact sequence of a triple in relative homology, exactly as pairs carry the long exact sequence of a pair; this file supplies that carrier together with the three pairs (A, B), (X, B) and (X, A) it determines and the two maps of pairs relating them.

Like TopPair, TauCeti.TopTriple is a full subcategory of a category of diagrams in TopCat, so a morphism of triples is a triple of continuous maps commuting with the two embeddings. All three pair constructions are therefore functorial, and the two maps of pairs between them are natural.

Nested subsets s ⊆ t ⊆ u of a topological space give the triple TopTriple.ofInclusions, whose three pairs are the pairs TopPair.ofInclusion of the three inclusions among them.

@[reducible, inline]

abbrev TauCeti.TopTriple : Type (u + 1)

A triple of topological spaces B ⊆ A ⊆ X, recorded as a pair of composable embeddings B ⟶ A ⟶ X in TopCat.

Equations

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

@[reducible, inline]

abbrev TauCeti.TopTriple.fst (T : TopTriple) : TopCat

The ambient space X of a triple (X, A, B).

Equations

• T.fst = T.obj.obj 2

@[reducible, inline]

abbrev TauCeti.TopTriple.snd (T : TopTriple) : TopCat

The middle space A of a triple (X, A, B).

Equations

• T.snd = T.obj.obj 1

@[reducible, inline]

abbrev TauCeti.TopTriple.thd (T : TopTriple) : TopCat

The smallest space B of a triple (X, A, B).

Equations

• T.thd = T.obj.obj 0

@[reducible, inline]

abbrev TauCeti.TopTriple.innerMap (T : TopTriple) : T.thd ⟶ T.snd

The embedding B ⟶ A of a triple (X, A, B).

Equations

• T.innerMap = T.obj.map' 0 1 TauCeti.TopTriple._proof_1 TauCeti.TopTriple._proof_3

@[reducible, inline]

abbrev TauCeti.TopTriple.outerMap (T : TopTriple) : T.snd ⟶ T.fst

The embedding A ⟶ X of a triple (X, A, B).

Equations

• T.outerMap = T.obj.map' 1 2 TauCeti.TopTriple._proof_3 TauCeti.TopTriple._proof_4

@[reducible, inline]

abbrev TauCeti.TopTriple.totalMap (T : TopTriple) : T.thd ⟶ T.fst

The embedding B ⟶ X of a triple (X, A, B).

Equations

• T.totalMap = T.obj.map' 0 2 TauCeti.TopTriple.totalMap._proof_1 TauCeti.TopTriple._proof_4

theorem TauCeti.TopTriple.innerMap_comp_outerMap (T : TopTriple) : CategoryTheory.CategoryStruct.comp T.innerMap T.outerMap = T.totalMap

theorem TauCeti.TopTriple.innerMap_comp_outerMap_assoc (T : TopTriple) {Z : TopCat} (h : T.fst ⟶ Z) : CategoryTheory.CategoryStruct.comp T.innerMap (CategoryTheory.CategoryStruct.comp T.outerMap h) = CategoryTheory.CategoryStruct.comp T.totalMap h

theorem TauCeti.TopTriple.innerMap_comp_outerMap_apply (T : TopTriple) (x : ↑T.thd) : (CategoryTheory.ConcreteCategory.hom T.outerMap) ((CategoryTheory.ConcreteCategory.hom T.innerMap) x) = (CategoryTheory.ConcreteCategory.hom T.totalMap) x

theorem TauCeti.TopTriple.isEmbedding_innerMap (T : TopTriple) : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom T.innerMap)

theorem TauCeti.TopTriple.isEmbedding_outerMap (T : TopTriple) : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom T.outerMap)

theorem TauCeti.TopTriple.isEmbedding_totalMap (T : TopTriple) : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom T.totalMap)

@[reducible, inline]

abbrev TauCeti.TopTriple.of {B A X : TopCat} (i : B ⟶ A) (j : A ⟶ X) (hi : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom i)) (hj : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom j)) : TopTriple

Construct a triple of topological spaces from two composable embeddings.

Equations

• TauCeti.TopTriple.of i j hi hj = { obj := CategoryTheory.ComposableArrows.mk₂ i j, property := ⋯ }

@[simp]

theorem TauCeti.TopTriple.of_innerMap {B A X : TopCat} (i : B ⟶ A) (j : A ⟶ X) (hi : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom i)) (hj : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom j)) : (of i j hi hj).innerMap = i

@[simp]

theorem TauCeti.TopTriple.of_outerMap {B A X : TopCat} (i : B ⟶ A) (j : A ⟶ X) (hi : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom i)) (hj : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom j)) : (of i j hi hj).outerMap = j

@[simp]

theorem TauCeti.TopTriple.of_totalMap {B A X : TopCat} (i : B ⟶ A) (j : A ⟶ X) (hi : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom i)) (hj : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom j)) : (of i j hi hj).totalMap = CategoryTheory.CategoryStruct.comp i j

@[reducible, inline]

abbrev TauCeti.TopTriple.ofInclusions {X : TopCat} {s t u : Set ↑X} (hst : s ⊆ t) (htu : t ⊆ u) : TopTriple

The triple (u, t, s) determined by nested subsets s ⊆ t ⊆ u of a topological space, with the two inclusions as its embeddings.

Equations

• TauCeti.TopTriple.ofInclusions hst htu = TauCeti.TopTriple.of (TopCat.ofHom (ContinuousMap.inclusion hst)) (TopCat.ofHom (ContinuousMap.inclusion htu)) ⋯ ⋯

@[reducible, inline]

abbrev TauCeti.TopTriple.Hom (T T' : TopTriple) : Type u

Morphisms of triples of topological spaces.

Equations

• T.Hom T' = (T ⟶ T')

@[reducible, inline]

abbrev TauCeti.TopTriple.Hom.fst {T T' : TopTriple} (φ : T ⟶ T') : T.fst ⟶ T'.fst

The map between the ambient spaces induced by a morphism of triples.

Equations

• TauCeti.TopTriple.Hom.fst φ = φ.hom.app 2

@[reducible, inline]

abbrev TauCeti.TopTriple.Hom.snd {T T' : TopTriple} (φ : T ⟶ T') : T.snd ⟶ T'.snd

The map between the middle spaces induced by a morphism of triples.

Equations

• TauCeti.TopTriple.Hom.snd φ = φ.hom.app 1

@[reducible, inline]

abbrev TauCeti.TopTriple.Hom.thd {T T' : TopTriple} (φ : T ⟶ T') : T.thd ⟶ T'.thd

The map between the smallest spaces induced by a morphism of triples.

Equations

• TauCeti.TopTriple.Hom.thd φ = φ.hom.app 0

theorem TauCeti.TopTriple.Hom.thd_comp_innerMap {T T' : TopTriple} (φ : T ⟶ T') : CategoryTheory.CategoryStruct.comp (thd φ) T'.innerMap = CategoryTheory.CategoryStruct.comp T.innerMap (snd φ)

theorem TauCeti.TopTriple.Hom.thd_comp_innerMap_assoc {T T' : TopTriple} (φ : T ⟶ T') {Z : TopCat} (h : T'.snd ⟶ Z) : CategoryTheory.CategoryStruct.comp (thd φ) (CategoryTheory.CategoryStruct.comp T'.innerMap h) = CategoryTheory.CategoryStruct.comp T.innerMap (CategoryTheory.CategoryStruct.comp (snd φ) h)

theorem TauCeti.TopTriple.Hom.snd_comp_outerMap {T T' : TopTriple} (φ : T ⟶ T') : CategoryTheory.CategoryStruct.comp (snd φ) T'.outerMap = CategoryTheory.CategoryStruct.comp T.outerMap (fst φ)

theorem TauCeti.TopTriple.Hom.snd_comp_outerMap_assoc {T T' : TopTriple} (φ : T ⟶ T') {Z : TopCat} (h : T'.fst ⟶ Z) : CategoryTheory.CategoryStruct.comp (snd φ) (CategoryTheory.CategoryStruct.comp T'.outerMap h) = CategoryTheory.CategoryStruct.comp T.outerMap (CategoryTheory.CategoryStruct.comp (fst φ) h)

theorem TauCeti.TopTriple.Hom.ext {T T' : TopTriple} {φ ψ : T ⟶ T'} (h₀ : thd φ = thd ψ) (h₁ : snd φ = snd ψ) (h₂ : fst φ = fst ψ) : φ = ψ

theorem TauCeti.TopTriple.Hom.ext_iff {T T' : TopTriple} {φ ψ : T ⟶ T'} : φ = ψ ↔ thd φ = thd ψ ∧ snd φ = snd ψ ∧ fst φ = fst ψ

@[reducible, inline]

abbrev TauCeti.TopTriple.innerPair : CategoryTheory.Functor TopTriple TopPair

The pair (A, B) of a triple (X, A, B).

Equations

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

@[reducible, inline]

abbrev TauCeti.TopTriple.totalPair : CategoryTheory.Functor TopTriple TopPair

The pair (X, B) of a triple (X, A, B).

Equations

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

@[reducible, inline]

abbrev TauCeti.TopTriple.outerPair : CategoryTheory.Functor TopTriple TopPair

The pair (X, A) of a triple (X, A, B).

Equations

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

@[simp]

theorem TauCeti.TopTriple.innerPair_obj_map {T : TopTriple} : TopPair.map = T.innerMap

@[simp]

theorem TauCeti.TopTriple.totalPair_obj_map {T : TopTriple} : TopPair.map = T.totalMap

@[simp]

theorem TauCeti.TopTriple.outerPair_obj_map {T : TopTriple} : TopPair.map = T.outerMap

@[simp]

theorem TauCeti.TopTriple.innerPair_obj_ofInclusions {X : TopCat} {s t u : Set ↑X} (hst : s ⊆ t) (htu : t ⊆ u) : innerPair.obj (ofInclusions hst htu) = TopPair.ofInclusion hst

@[simp]

theorem TauCeti.TopTriple.totalPair_obj_ofInclusions {X : TopCat} {s t u : Set ↑X} (hst : s ⊆ t) (htu : t ⊆ u) : totalPair.obj (ofInclusions hst htu) = TopPair.ofInclusion ⋯

@[simp]

theorem TauCeti.TopTriple.outerPair_obj_ofInclusions {X : TopCat} {s t u : Set ↑X} (hst : s ⊆ t) (htu : t ⊆ u) : outerPair.obj (ofInclusions hst htu) = TopPair.ofInclusion htu

@[simp]

theorem TauCeti.TopTriple.innerPair_map_fst {T T' : TopTriple} (φ : T ⟶ T') : TopPair.Hom.fst (innerPair.map φ) = Hom.snd φ

@[simp]

theorem TauCeti.TopTriple.innerPair_map_snd {T T' : TopTriple} (φ : T ⟶ T') : TopPair.Hom.snd (innerPair.map φ) = Hom.thd φ

@[simp]

theorem TauCeti.TopTriple.totalPair_map_fst {T T' : TopTriple} (φ : T ⟶ T') : TopPair.Hom.fst (totalPair.map φ) = Hom.fst φ

@[simp]

theorem TauCeti.TopTriple.totalPair_map_snd {T T' : TopTriple} (φ : T ⟶ T') : TopPair.Hom.snd (totalPair.map φ) = Hom.thd φ

@[simp]

theorem TauCeti.TopTriple.outerPair_map_fst {T T' : TopTriple} (φ : T ⟶ T') : TopPair.Hom.fst (outerPair.map φ) = Hom.fst φ

@[simp]

theorem TauCeti.TopTriple.outerPair_map_snd {T T' : TopTriple} (φ : T ⟶ T') : TopPair.Hom.snd (outerPair.map φ) = Hom.snd φ

def TauCeti.TopTriple.innerToTotal : innerPair ⟶ totalPair

The map of pairs (A, B) ⟶ (X, B) determined by a triple (X, A, B).

Equations

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

def TauCeti.TopTriple.totalToOuter : totalPair ⟶ outerPair

The map of pairs (X, B) ⟶ (X, A) determined by a triple (X, A, B).

Equations

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

@[simp]

theorem TauCeti.TopTriple.innerToTotal_app_fst {T : TopTriple} : TopPair.Hom.fst (innerToTotal.app T) = T.outerMap

@[simp]

theorem TauCeti.TopTriple.innerToTotal_app_snd {T : TopTriple} : TopPair.Hom.snd (innerToTotal.app T) = CategoryTheory.CategoryStruct.id T.thd

@[simp]

theorem TauCeti.TopTriple.totalToOuter_app_fst {T : TopTriple} : TopPair.Hom.fst (totalToOuter.app T) = CategoryTheory.CategoryStruct.id T.fst

@[simp]

theorem TauCeti.TopTriple.totalToOuter_app_snd {T : TopTriple} : TopPair.Hom.snd (totalToOuter.app T) = T.innerMap