The relative homology of a disk and its boundary

The relative singular homology of the n-disk modulo its boundary is one copy of the coefficient object in degree n and vanishes in every other degree.

The degree-zero relative homology of a positive-dimensional disk vanishes relative to its boundary. For the one-dimensional disk, both boundary points determine the same zeroth-homology class of the disk; in higher dimensions the boundary itself is path-connected. The lower bound is sharp: for n = 0, the disk is a point and its boundary is empty, so the degree-zero group is one copy of the coefficient object, identified by the augmentation.

In positive degrees, the disk is contractible, so the reduced connecting morphism of the pair identifies Hₖ₊₁(Dⁿ, Sⁿ⁻¹) with the reduced homology H~ₖ(Sⁿ⁻¹) of the boundary sphere, which is computed in TauCeti/AlgebraicTopology/Singular/Sphere.lean. The isomorphism Hₙ(Dⁿ, Sⁿ⁻¹) ≅ R in the top degree is this connecting morphism followed by the chosen generator of H~ₙ₋₁(Sⁿ⁻¹), so the connecting morphism carries the generator of the pair to the generator of the sphere.

Main results

• TauCeti.isZero_singularHomology_diskBoundaryPair_zero: H₀(Dⁿ, Sⁿ⁻¹) = 0 for n ≥ 1.
• TauCeti.isZero_singularHomology_diskBoundaryPair_of_ne: Hₖ(Dⁿ, Sⁿ⁻¹) = 0 for k ≠ n.
• TauCeti.singularHomologyDiskBoundaryPairIso: Hₙ(Dⁿ, Sⁿ⁻¹) ≅ R.

References

• A. Hatcher, Algebraic Topology, Section 2.1, Corollary 2.24 and Example 2.23.

theorem TauCeti.diskBoundary_singularHomologyMap_zero_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {n : ℕ} (hn : 2 ≤ n) : CategoryTheory.IsIso (((AlgebraicTopology.singularHomologyFunctor C 0).obj R).map (TopCat.diskBoundaryInclusion n))

The inclusion from the boundary of a disk of dimension at least two is an isomorphism on zeroth singular homology.

theorem TauCeti.isZero_singularHomology_diskBoundaryPair_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {n : ℕ} (hn : 1 ≤ n) : CategoryTheory.Limits.IsZero ((diskBoundaryPair n).singularHomology R 0)

The degree-zero relative homology of a positive-dimensional disk and its boundary vanishes.

noncomputable def TauCeti.singularHomologyDiskBoundaryPairZeroIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : ℕ) : (diskBoundaryPair 0).singularHomology R k ≅ ((AlgebraicTopology.singularHomologyFunctor C k).obj R).obj (TopCat.disk 0)

The relative homology of the pair of the 0-disk and its empty boundary is the ordinary homology of the point D⁰: the quotient map from ambient to relative singular homology is an isomorphism, and this is its inverse (TauCeti.singularHomologyDiskBoundaryPairZeroIso_inv).

Equations

• TauCeti.singularHomologyDiskBoundaryPairZeroIso R k = (CategoryTheory.asIso ((TauCeti.diskBoundaryPair 0).singularHomologyπ R k)).symm

@[simp]

theorem TauCeti.singularHomologyDiskBoundaryPairZeroIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : ℕ) : (singularHomologyDiskBoundaryPairZeroIso R k).hom = CategoryTheory.inv ((diskBoundaryPair 0).singularHomologyπ R k)

The comparison from the relative homology of the 0-disk pair to the ordinary homology of the point is the inverse of the quotient map.

@[simp]

theorem TauCeti.singularHomologyDiskBoundaryPairZeroIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : ℕ) : (singularHomologyDiskBoundaryPairZeroIso R k).inv = (diskBoundaryPair 0).singularHomologyπ R k

The comparison from the ordinary homology of the point to the relative homology of the 0-disk pair is the quotient map from ambient to relative singular homology.

theorem TauCeti.isZero_singularHomology_diskBoundaryPair_of_ne {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {n k : ℕ} (hk : k ≠ n) : CategoryTheory.Limits.IsZero ((diskBoundaryPair n).singularHomology R k)

The relative homology of a disk modulo its boundary vanishes outside its dimension: Hₖ(Dⁿ, Sⁿ⁻¹) = 0 for k ≠ n.

noncomputable def TauCeti.singularHomologyDiskBoundaryPairIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (n : ℕ) : (diskBoundaryPair n).singularHomology R n ≅ R

The relative homology of a disk modulo its boundary in its dimension: Hₙ(Dⁿ, Sⁿ⁻¹) ≅ R. For n = m + 1 it is the reduced connecting isomorphism onto H~ₘ(Sᵐ) followed by the chosen generator TauCeti.reducedSingularHomologyTopCatSphereIso of the sphere (TauCeti.singularHomologyDiskBoundaryPairIso_succ_hom); for n = 0 the pair is a point modulo the empty set and the isomorphism is the augmentation.

Equations

• One or more equations did not get rendered due to their size.
• TauCeti.singularHomologyDiskBoundaryPairIso R 0 = TauCeti.singularHomologyDiskBoundaryPairZeroIso R 0 ≪≫ CategoryTheory.asIso ((TopCat.disk 0).singularHomology₀ε R)

@[simp]

theorem TauCeti.singularHomologyDiskBoundaryPairIso_succ_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (m : ℕ) : (singularHomologyDiskBoundaryPairIso R (m + 1)).hom = CategoryTheory.CategoryStruct.comp ((diskBoundaryPair (m + 1)).reducedSingularHomologyδ R m) (reducedSingularHomologyTopCatSphereIso R m).hom

In positive dimension, the identification Hₘ₊₁(Dᵐ⁺¹, Sᵐ) ≅ R is the reduced connecting morphism of the pair followed by the chosen generator of H~ₘ(Sᵐ).

theorem TauCeti.singularHomologyDiskBoundaryPairIso_inv_comp_singularHomologyδ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (m : ℕ) : CategoryTheory.CategoryStruct.comp (singularHomologyDiskBoundaryPairIso R (m + 1)).inv ((diskBoundaryPair (m + 1)).singularHomologyδ R (m + 1) m ⋯) = CategoryTheory.CategoryStruct.comp (reducedSingularHomologyTopCatSphereIso R m).inv ((reducedSingularHomologyι R m).app (TopCat.diskBoundary (m + 1)))

The ordinary connecting morphism sends the disk generator to the boundary-sphere generator, viewed in unreduced homology. In dimension one this is the reduced class of the two endpoints.

theorem TauCeti.singularHomologyDiskBoundaryPairIso_inv_comp_singularHomologyδ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (m : ℕ) {Z : C} (h : (TopPair.toSSetPair.obj (diskBoundaryPair (m + 1))).left.homology R m ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularHomologyDiskBoundaryPairIso R (m + 1)).inv (CategoryTheory.CategoryStruct.comp ((diskBoundaryPair (m + 1)).singularHomologyδ R (m + 1) m ⋯) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (reducedSingularHomologyTopCatSphereIso R m).inv ((reducedSingularHomologyι R m).app (TopCat.diskBoundary (m + 1)))) h

The ordinary connecting morphism sends the disk generator to the boundary-sphere generator, viewed in unreduced homology. In dimension one this is the reduced class of the two endpoints.

@[simp]

theorem TauCeti.singularHomologyDiskBoundaryPairIso_zero_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) : (singularHomologyDiskBoundaryPairIso R 0).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv ((diskBoundaryPair 0).singularHomologyπ R 0)) ((TopCat.disk 0).singularHomology₀ε R)

In dimension zero, the identification H₀(D⁰, ∅) ≅ R is the inverse of the quotient map from the ordinary homology of the point followed by the augmentation.