Topological Pairs

In this file we introduce TopPair, the category of topological pairs. It is defined as the category of arrows in TopCat which are topological embeddings.

We provide the inclusion and diagonal functors TopCat ⥤ TopPair and show that they are left and right adjoint to the first projection functor, respectively.

We also define for two morphisms of topological pairs f, g : X ⟶ Y the structure Homotopy f g of homotopies between them.

@[reducible, inline]

abbrev TopPair : Type (u_1 + 1)

A pair of topological spaces consists of an embedding f : A ⟶ X in TopCat.

Equations

• TopPair = TopCat.isEmbedding.Arrow ⊤ ⊤

@[reducible, inline]

abbrev TopPair.fst {X : TopPair} : TopCat

The first space of the pair

Equations

• TopPair.fst = X.right

@[reducible, inline]

abbrev TopPair.snd {X : TopPair} : TopCat

The second space of the pair

Equations

• TopPair.snd = X.left

@[reducible, inline]

abbrev TopPair.map {X : TopPair} : snd ⟶ fst

The embedding of the second into the first space

Equations

• TopPair.map = X.hom

theorem TopPair.isEmbedding_map (X : TopPair) : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom map)

@[reducible, inline]

abbrev TopPair.of {A X : TopCat} (f : A ⟶ X) (h : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : TopPair

Construct a topological pair from its components.

Equations

• TopPair.of f h = CategoryTheory.MorphismProperty.Arrow.mk f h

@[reducible, inline]

abbrev TopPair.ofSubset {X : TopCat} (A : Set ↑X) : TopPair

Constructor for a topological pair (X, A) where A ⊆ X.

Equations

• TopPair.ofSubset A = TopPair.of { hom' := { toFun := Subtype.val, continuous_toFun := ⋯ } } ⋯

@[reducible, inline]

abbrev TopPair.ofTopCat (X : TopCat) : TopPair

Constructs the topological pair (X, ∅) from X : TopCat.

Equations

• TopPair.ofTopCat X = TopPair.of (TopCat.isInitialPEmpty.to X) ⋯

@[reducible, inline]

abbrev TopPair.ofHom {X Y : TopPair} (f : fst ⟶ fst) (g : snd ⟶ snd) (w : CategoryTheory.CategoryStruct.comp g map = CategoryTheory.CategoryStruct.comp map f := by cat_disch) : X ⟶ Y

Construct a morphism in TopPair from its components.

Equations

• TopPair.ofHom f g w = CategoryTheory.MorphismProperty.Arrow.homMk g f w ⋯ ⋯

@[reducible, inline]

abbrev TopPair.Hom.fst {X Y : TopPair} (f : X ⟶ Y) : TopPair.fst ⟶ TopPair.fst

The map between the first spaces

Equations

• TopPair.Hom.fst f = (CategoryTheory.MorphismProperty.Comma.Hom.hom f).right

@[reducible, inline]

abbrev TopPair.Hom.snd {X Y : TopPair} (f : X ⟶ Y) : TopPair.snd ⟶ TopPair.snd

The map between the second spaces

Equations

• TopPair.Hom.snd f = (CategoryTheory.MorphismProperty.Comma.Hom.hom f).left

theorem TopPair.Hom.w {X Y : TopPair} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (snd f) map = CategoryTheory.CategoryStruct.comp map (fst f)

theorem TopPair.Hom.w_assoc {X Y : TopPair} (f : X ⟶ Y) {Z : TopCat} (h : TopPair.fst ⟶ Z) : CategoryTheory.CategoryStruct.comp (snd f) (CategoryTheory.CategoryStruct.comp map h) = CategoryTheory.CategoryStruct.comp map (CategoryTheory.CategoryStruct.comp (fst f) h)

theorem TopPair.Hom.w_apply {X Y : TopPair} (f : X ⟶ Y) (x : ↑TopPair.snd) : (CategoryTheory.ConcreteCategory.hom map) ((CategoryTheory.ConcreteCategory.hom (snd f)) x) = (CategoryTheory.ConcreteCategory.hom (fst f)) ((CategoryTheory.ConcreteCategory.hom map) x)

@[reducible, inline]

abbrev TopPair.proj₁ : CategoryTheory.Functor TopPair TopCat

The functor from topological pairs to topological spaces that forgets the second space, i.e. the projection to the first space.

Equations

• TopPair.proj₁ = (CategoryTheory.MorphismProperty.Arrow.forget TopCat.isEmbedding ⊤ ⊤).comp CategoryTheory.Arrow.rightFunc

@[reducible, inline]

abbrev TopPair.proj₂ : CategoryTheory.Functor TopPair TopCat

The functor from topological pairs to topological spaces that forgets the first space, i.e. the projection to the second space.

Equations

• TopPair.proj₂ = (CategoryTheory.MorphismProperty.Arrow.forget TopCat.isEmbedding ⊤ ⊤).comp CategoryTheory.Arrow.leftFunc

def TopPair.incl : CategoryTheory.Functor TopCat TopPair

The inclusion functor from topological spaces to topological pairs that sends a space X to (X, ∅).

Equations

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

@[simp]

theorem TopPair.incl_map {X✝ Y✝ : TopCat} (f : X✝ ⟶ Y✝) : incl.map f = ofHom f (CategoryTheory.CategoryStruct.id snd) ⋯

@[simp]

theorem TopPair.incl_obj (X : TopCat) : incl.obj X = ofTopCat X

@[reducible, inline]

abbrev TopPair.diag : CategoryTheory.Functor TopCat TopPair

The functor from topological spaces to topological pairs that sends a space X to the identity morphism on X.

Equations

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

def TopPair.inclAdjProj₁ : incl ⊣ proj₁

The inclusion functor is left adjoint to the projection to the first component.

Equations

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

@[simp]

theorem TopPair.inclAdjProj₁_counit_app (X : TopPair) : inclAdjProj₁.counit.app X = ofHom (CategoryTheory.CategoryStruct.id fst) (TopCat.isInitialPEmpty.to snd) ⋯

@[simp]

theorem TopPair.inclAdjProj₁_unit_app (X : TopCat) : inclAdjProj₁.unit.app X = CategoryTheory.CategoryStruct.id X

def TopPair.proj₁AdjDiag : proj₁ ⊣ diag

The projection functor to the first component is left adjoint to the diagonal functor.

Equations

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

@[simp]

theorem TopPair.proj₁AdjDiag_counit_app (X : TopCat) : proj₁AdjDiag.counit.app X = CategoryTheory.CategoryStruct.id X

@[simp]

theorem TopPair.proj₁AdjDiag_unit_app (X : TopPair) : proj₁AdjDiag.unit.app X = ofHom (CategoryTheory.CategoryStruct.id fst) map ⋯

@[reducible, inline]

abbrev TopPair.j (X : TopPair) : incl.obj fst ⟶ X

The unique morphism (X, ∅) ⟶ (X, A) that is the identity on X.

Equations

• X.j = TopPair.ofHom (CategoryTheory.CategoryStruct.id TopPair.fst) (TopCat.isInitialPEmpty.to TopPair.snd) ⋯

structure TopPair.Homotopy {X Y : TopPair} (f g : X ⟶ Y) : Type u

A homotopy of maps between topological pairs is a homotopy on the first space and a homotopy on the second space that fit in a commutative square with the maps of the pairs.

• fst : TopCat.Homotopy (Hom.fst f) (Hom.fst g)

  The homotopy on the first space.

• snd : TopCat.Homotopy (Hom.snd f) (Hom.snd g)

  The homotopy on the second space.

• w : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight map TopCat.I) self.fst.h = CategoryTheory.CategoryStruct.comp self.snd.h map

  The proof that the homotopies fit into a commutative square with the maps of the pairs.

theorem TopPair.Homotopy.ext {X Y : TopPair} {f g : X ⟶ Y} {x y : Homotopy f g} (fst : x.fst = y.fst) (snd : x.snd = y.snd) : x = y

theorem TopPair.Homotopy.ext_iff {X Y : TopPair} {f g : X ⟶ Y} {x y : Homotopy f g} : x = y ↔ x.fst = y.fst ∧ x.snd = y.snd

theorem TopPair.Homotopy.w_assoc {X Y : TopPair} {f g : X ⟶ Y} (self : Homotopy f g) {Z : TopCat} (h : TopPair.fst ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight map TopCat.I) (CategoryTheory.CategoryStruct.comp self.fst.h h) = CategoryTheory.CategoryStruct.comp self.snd.h (CategoryTheory.CategoryStruct.comp map h)

The proof that the homotopies fit into a commutative square with the maps of the pairs.

theorem TopPair.Homotopy.w_apply {X Y : TopPair} {f g : X ⟶ Y} (self : Homotopy f g) (x : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj TopPair.snd TopCat.I)) : self.fst (TopCat.I.homeomorph x.2, (CategoryTheory.ConcreteCategory.hom map) x.1) = (CategoryTheory.ConcreteCategory.hom map) (self.snd (TopCat.I.homeomorph x.2, x.1))

The proof that the homotopies fit into a commutative square with the maps of the pairs.

theorem TopPair.Homotopy.w_apply' {X Y : TopPair} {f g : X ⟶ Y} (H : Homotopy f g) (x : ↑TopPair.snd) (t : ↑unitInterval) : H.fst (t, (CategoryTheory.ConcreteCategory.hom map) x) = (CategoryTheory.ConcreteCategory.hom map) (H.snd (t, x))

def TopPair.Homotopy.refl {X Y : TopPair} (f : X ⟶ Y) : Homotopy f f

Given a morphism f of topological pairs, we can define a Homotopy f f by TopCat.Homotopy.refl on the first and second components.

Equations

• TopPair.Homotopy.refl f = { fst := TopCat.Homotopy.refl (TopPair.Hom.fst f), snd := TopCat.Homotopy.refl (TopPair.Hom.snd f), w := ⋯ }

@[simp]

theorem TopPair.Homotopy.refl_fst {X Y : TopPair} (f : X ⟶ Y) : (refl f).fst = TopCat.Homotopy.refl (Hom.fst f)

@[simp]

theorem TopPair.Homotopy.refl_snd {X Y : TopPair} (f : X ⟶ Y) : (refl f).snd = TopCat.Homotopy.refl (Hom.snd f)

@[implicit_reducible]

instance TopPair.Homotopy.instInhabitedId {X : TopPair} : Inhabited (Homotopy (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))

Equations

• TopPair.Homotopy.instInhabitedId = { default := TopPair.Homotopy.refl (CategoryTheory.CategoryStruct.id X) }

def TopPair.Homotopy.symm {X Y : TopPair} {f₀ f₁ : X ⟶ Y} (F : Homotopy f₀ f₁) : Homotopy f₁ f₀

Given a Homotopy f₀ f₁, we can define a Homotopy f₁ f₀ by TopCat.Homotopy.symm on the first and second components.

Equations

• F.symm = { fst := F.fst.symm, snd := F.snd.symm, w := ⋯ }

@[simp]

theorem TopPair.Homotopy.symm_fst {X Y : TopPair} {f₀ f₁ : X ⟶ Y} (F : Homotopy f₀ f₁) : F.symm.fst = F.fst.symm

@[simp]

theorem TopPair.Homotopy.symm_snd {X Y : TopPair} {f₀ f₁ : X ⟶ Y} (F : Homotopy f₀ f₁) : F.symm.snd = F.snd.symm

@[simp]

theorem TopPair.Homotopy.symm_symm {X Y : TopPair} {f₀ f₁ : X ⟶ Y} (F : Homotopy f₀ f₁) : F.symm.symm = F

theorem TopPair.Homotopy.symm_bijective {X Y : TopPair} {f₀ f₁ : X ⟶ Y} : Function.Bijective symm

noncomputable def TopPair.Homotopy.trans {X Y : TopPair} {f₀ f₁ f₂ : X ⟶ Y} (F : Homotopy f₀ f₁) (G : Homotopy f₁ f₂) : Homotopy f₀ f₂

Given Homotopy f₀ f₁ and Homotopy f₁ f₂, we can define a Homotopy f₀ f₂ by TopCat.Homotopy.trans on the first and second components.

Equations

• F.trans G = { fst := F.fst.trans G.fst, snd := F.snd.trans G.snd, w := ⋯ }

@[simp]

theorem TopPair.Homotopy.trans_fst {X Y : TopPair} {f₀ f₁ f₂ : X ⟶ Y} (F : Homotopy f₀ f₁) (G : Homotopy f₁ f₂) : (F.trans G).fst = F.fst.trans G.fst

@[simp]

theorem TopPair.Homotopy.trans_snd {X Y : TopPair} {f₀ f₁ f₂ : X ⟶ Y} (F : Homotopy f₀ f₁) (G : Homotopy f₁ f₂) : (F.trans G).snd = F.snd.trans G.snd

theorem TopPair.Homotopy.symm_trans {X Y : TopPair} {f₀ f₁ f₂ : X ⟶ Y} (F : Homotopy f₀ f₁) (G : Homotopy f₁ f₂) : (F.trans G).symm = G.symm.trans F.symm

def TopPair.Homotopy.comp {X Y Z : TopPair} {f₀ f₁ : X ⟶ Y} {g₀ g₁ : Y ⟶ Z} (G : Homotopy g₀ g₁) (F : Homotopy f₀ f₁) : Homotopy (CategoryTheory.CategoryStruct.comp f₀ g₀) (CategoryTheory.CategoryStruct.comp f₁ g₁)

If we have a Homotopy g₀ g₁ and a Homotopy f₀ f₁, we can define a Homotopy (f₀ ≫ g₀) (f₁ ≫ g₁) by TopCat.Homotopy.comp on the first and second components.

Equations

• G.comp F = { fst := G.fst.comp F.fst, snd := G.snd.comp F.snd, w := ⋯ }

@[simp]

theorem TopPair.Homotopy.comp_fst {X Y Z : TopPair} {f₀ f₁ : X ⟶ Y} {g₀ g₁ : Y ⟶ Z} (G : Homotopy g₀ g₁) (F : Homotopy f₀ f₁) : (G.comp F).fst = G.fst.comp F.fst

@[simp]

theorem TopPair.Homotopy.comp_snd {X Y Z : TopPair} {f₀ f₁ : X ⟶ Y} {g₀ g₁ : Y ⟶ Z} (G : Homotopy g₀ g₁) (F : Homotopy f₀ f₁) : (G.comp F).snd = G.snd.comp F.snd

def TopPair.Homotopic {X Y : TopPair} (f g : X ⟶ Y) : Prop

Two maps between topological pairs are homotopic if there is a homotopy between them.

Equations

• TopPair.Homotopic f g = Nonempty (TopPair.Homotopy f g)

theorem TopPair.Homotopic.equivalence {X Y : TopPair} : Equivalence Homotopic

Two maps of topological pairs being homotopic defines an equivalence relation.