Homology cobordisms

Let R be a ring. An R-homology cobordism between two manifolds Y₀ and Y₁ is a compact manifold W whose boundary is the disjoint union of copies of Y₀ and Y₁, such that both inclusions induce isomorphisms on singular homology with coefficients in R. Thus W looks like the product Y₀ × [0, 1] to R-homology. Homology cobordisms of integral homology 3-spheres are the ambient spaces of homology concordance of knots, and the homology cobordism group of homology spheres is built from them.

The boundary of W is not given its own manifold structure here. Instead the two ends are smooth embeddings ι₀ : Y₀ → W and ι₁ : Y₁ → W of manifolds modelled on I into the manifold W modelled on J, with disjoint images whose union is the manifold boundary J.boundary W (TauCeti.IsHomologyCobordism R I J n ι₀ ι₁). No orientations are involved: an integral homology cobordism between integral homology spheres is automatically orientable, since its first homology vanishes.

The cylinder Y × [a, b] over a compact boundaryless manifold Y, modelled on I.prod (𝓡∂ 1), is a homology cobordism between two copies of Y, embedded as its bottom and top (TauCeti.isHomologyCobordism_cylinder), for every coefficient ring.

Main definitions

• TauCeti.IsHomologyCobordism R I J n ι₀ ι₁: ι₀ and ι₁ exhibit W as an R-homology cobordism between Y₀ and Y₁.
• TauCeti.IsHomologyCobordism.singularHomologyIso: the isomorphism Hₖ(Y₀; R) ≅ Hₖ(Y₁; R) that a homology cobordism induces.

Main results

• TauCeti.IsHomologyCobordism.symm: a homology cobordism read backwards.
• TauCeti.isHomologyCobordism_cylinder: a cylinder over a compact boundaryless manifold is a homology cobordism between its ends.

Implementation notes

All three spaces live in one universe with the coefficient ring, because singular homology is taken in ModuleCat.{u} R of topological spaces in TopCat.{u}.

References

• A. S. Levine, Nonsurjective satellite operators and piecewise-linear concordance, Forum Math. Sigma 4 (2016), e34, Remark 1.5, for homology cobordisms between homology spheres and the homology concordance of knots in them.

structure TauCeti.IsHomologyCobordism (R : Type u) [Ring R] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_4} [TopologicalSpace G] (J : ModelWithCorners ℝ F G) (n : WithTop ℕ∞) {Y₀ Y₁ W : Type u} [TopologicalSpace Y₀] [ChartedSpace H Y₀] [TopologicalSpace Y₁] [ChartedSpace H Y₁] [TopologicalSpace W] [ChartedSpace G W] (ι₀ : SmoothEmbedding I J n Y₀ W) (ι₁ : SmoothEmbedding I J n Y₁ W) : Prop

The smooth embeddings ι₀ : Y₀ → W and ι₁ : Y₁ → W exhibit W as an R-homology cobordism between Y₀ and Y₁: W is compact, the two embeddings have disjoint images whose union is the boundary of W, and each induces an isomorphism on singular homology with coefficients in R in every degree.

• compactSpace : CompactSpace W

  A cobordism is compact.

• disjoint_range : Disjoint (Set.range ⇑ι₀) (Set.range ⇑ι₁)

  The two ends are disjoint.

• range_union_range : Set.range ⇑ι₀ ∪ Set.range ⇑ι₁ = ModelWithCorners.boundary W

  The two ends make up the boundary.

• isIso_left (k : ℕ) : CategoryTheory.IsIso (((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) k).obj ↧R).map (TopCat.ofHom ι₀.toContinuousMap))

  The first end induces isomorphisms on singular homology.

• isIso_right (k : ℕ) : CategoryTheory.IsIso (((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) k).obj ↧R).map (TopCat.ofHom ι₁.toContinuousMap))

  The second end induces isomorphisms on singular homology.

theorem TauCeti.IsHomologyCobordism.symm {R : Type u} [Ring R] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_4} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {n : WithTop ℕ∞} {Y₀ Y₁ W : Type u} [TopologicalSpace Y₀] [ChartedSpace H Y₀] [TopologicalSpace Y₁] [ChartedSpace H Y₁] [TopologicalSpace W] [ChartedSpace G W] {ι₀ : SmoothEmbedding I J n Y₀ W} {ι₁ : SmoothEmbedding I J n Y₁ W} (h : IsHomologyCobordism R I J n ι₀ ι₁) : IsHomologyCobordism R I J n ι₁ ι₀

A homology cobordism from Y₀ to Y₁ is one from Y₁ to Y₀.

noncomputable def TauCeti.IsHomologyCobordism.singularHomologyIso {R : Type u} [Ring R] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_4} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {n : WithTop ℕ∞} {Y₀ Y₁ W : Type u} [TopologicalSpace Y₀] [ChartedSpace H Y₀] [TopologicalSpace Y₁] [ChartedSpace H Y₁] [TopologicalSpace W] [ChartedSpace G W] {ι₀ : SmoothEmbedding I J n Y₀ W} {ι₁ : SmoothEmbedding I J n Y₁ W} (h : IsHomologyCobordism R I J n ι₀ ι₁) (k : ℕ) : ((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) k).obj ↧R).obj ↧Y₀ ≅ ((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) k).obj ↧R).obj ↧Y₁

A homology cobordism between Y₀ and Y₁ identifies their singular homology: the isomorphism Hₖ(Y₀; R) ≅ Hₖ(W; R) ≅ Hₖ(Y₁; R) through the two ends.

@[simp]

theorem TauCeti.IsHomologyCobordism.singularHomologyIso_hom_comp {R : Type u} [Ring R] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_4} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {n : WithTop ℕ∞} {Y₀ Y₁ W : Type u} [TopologicalSpace Y₀] [ChartedSpace H Y₀] [TopologicalSpace Y₁] [ChartedSpace H Y₁] [TopologicalSpace W] [ChartedSpace G W] {ι₀ : SmoothEmbedding I J n Y₀ W} {ι₁ : SmoothEmbedding I J n Y₁ W} (h : IsHomologyCobordism R I J n ι₀ ι₁) (k : ℕ) : CategoryTheory.CategoryStruct.comp (h.singularHomologyIso k).hom (((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) k).obj ↧R).map (TopCat.ofHom ι₁.toContinuousMap)) = ((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) k).obj ↧R).map (TopCat.ofHom ι₀.toContinuousMap)

The isomorphism of a homology cobordism is compatible with the two ends: following it by the second end is the first end.

@[simp]

theorem TauCeti.IsHomologyCobordism.singularHomologyIso_hom_comp_assoc {R : Type u} [Ring R] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_4} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {n : WithTop ℕ∞} {Y₀ Y₁ W : Type u} [TopologicalSpace Y₀] [ChartedSpace H Y₀] [TopologicalSpace Y₁] [ChartedSpace H Y₁] [TopologicalSpace W] [ChartedSpace G W] {ι₀ : SmoothEmbedding I J n Y₀ W} {ι₁ : SmoothEmbedding I J n Y₁ W} (h : IsHomologyCobordism R I J n ι₀ ι₁) (k : ℕ) {Z : ModuleCat R} (h✝ : ((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) k).obj ↧R).obj ↧W ⟶ Z) : CategoryTheory.CategoryStruct.comp (h.singularHomologyIso k).hom (CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) k).obj ↧R).map (TopCat.ofHom ι₁.toContinuousMap)) h✝) = CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) k).obj ↧R).map (TopCat.ofHom ι₀.toContinuousMap)) h✝

The isomorphism of a homology cobordism is compatible with the two ends: following it by the second end is the first end.

@[simp]

theorem TauCeti.IsHomologyCobordism.singularHomologyIso_symm {R : Type u} [Ring R] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_4} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {n : WithTop ℕ∞} {Y₀ Y₁ W : Type u} [TopologicalSpace Y₀] [ChartedSpace H Y₀] [TopologicalSpace Y₁] [ChartedSpace H Y₁] [TopologicalSpace W] [ChartedSpace G W] {ι₀ : SmoothEmbedding I J n Y₀ W} {ι₁ : SmoothEmbedding I J n Y₁ W} (h : IsHomologyCobordism R I J n ι₀ ι₁) (k : ℕ) : ⋯.singularHomologyIso k = (h.singularHomologyIso k).symm

Reading a homology cobordism backwards inverts its isomorphism.

The cylinder

theorem TauCeti.isHomologyCobordism_cylinder (R : Type u) [Ring R] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {a b : ℝ} [Fact (a < b)] {Y : Type u} [TopologicalSpace Y] [ChartedSpace H Y] [IsManifold I n Y] [I.Boundaryless] [CompactSpace Y] : IsHomologyCobordism R I (I.prod (modelWithCornersEuclideanHalfSpace 1)) n (SmoothEmbedding.cylinderBot I n a b Y) (SmoothEmbedding.cylinderTop I n a b Y)

The cylinder is a homology cobordism. For a compact boundaryless manifold Y, the cylinder Y × [a, b] is an R-homology cobordism between two copies of Y, embedded as its bottom and its top.