Local homology along open embeddings

A continuous map j : M → N with j ⁻¹' T ⊆ S induces a map Hₖ(M, M ∖ S) ⟶ Hₖ(N, N ∖ T) of local homology groups (TauCeti.localHomologyMap). When j is an open embedding, T is closed and contained in the image of j, and S = j ⁻¹' T, this map is an isomorphism (TauCeti.isIso_localHomologyMap): by excision, local homology along T may be computed in the open neighbourhood j(M) of T, which j identifies with M. In particular an open embedding into a T₁ space identifies the local homology of M at x with that of N at j x (TauCeti.localHomologyIsoOfIsOpenEmbedding).

For Hausdorff spaces M and N modelled on the same finite-dimensional real normed space, these isomorphisms intertwine the transport of local homology along paths (TauCeti.localHomologyTransport_comp_localHomologyIsoOfIsOpenEmbedding_hom): the local homology system of M is the pullback along j of the local homology system of N. This holds because a chart of M, read on the open subset j(M) of N, is a chart of N, and transport is determined by its behaviour along paths inside compact convex sets of charts (TauCeti.eq_localHomologyTransport). In top degree with integral coefficients it is the naturality of the orientation local system under open embeddings, through which orientations restrict to open subsets and are compared along homeomorphisms.

Main definitions

• TauCeti.localHomologyIsoOfIsOpenEmbedding: for an open embedding j, the isomorphism Hₖ(M, M ∖ {x}) ≅ Hₖ(N, N ∖ {j x}).

Main results

• TauCeti.isIso_localHomologyMap: excision along an open embedding.
• TauCeti.localHomologyIsoOfIsOpenEmbedding_inv_comp_localHomologyMap: the map induced by an open embedding undoes the inverse of this isomorphism.
• TauCeti.localHomologyIsoOfIsOpenEmbedding_id, TauCeti.localHomologyIsoOfIsOpenEmbedding_trans: these isomorphisms are functorial.
• TauCeti.localHomologyTransport_comp_localHomologyIsoOfIsOpenEmbedding_hom: open embeddings intertwine the transport of local homology.

References

• A. Hatcher, Algebraic Topology, Section 3.3: local homology, computed by excision in a neighbourhood, and its transport along paths through balls in charts.

theorem TauCeti.isIso_localHomologyMap {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M N : Type w} [TopologicalSpace M] [TopologicalSpace N] (j : C(M, N)) (hj : Topology.IsOpenEmbedding ⇑j) {S : Set M} {T : Set N} (h : ⇑j ⁻¹' T = S) (hT : IsClosed T) (hTj : T ⊆ Set.range ⇑j) (k : ℕ) : CategoryTheory.IsIso (localHomologyMap R j ⋯ k)

Excision along an open embedding. If j is an open embedding, T is closed and lies in the image of j, and S = j ⁻¹' T, then j induces an isomorphism Hₖ(M, M ∖ S) ≅ Hₖ(N, N ∖ T).

noncomputable def TauCeti.localHomologyIsoOfIsOpenEmbedding {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M N : Type w} [TopologicalSpace M] [TopologicalSpace N] [T1Space N] {j : M → N} (hj : Topology.IsOpenEmbedding j) (x : M) (k : ℕ) : localHomology R {x} k ≅ localHomology R {j x} k

An open embedding j : M → N into a T₁ space identifies the local homology of M at x with the local homology of N at j x.

@[simp]

theorem TauCeti.localHomologyIsoOfIsOpenEmbedding_hom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M N : Type w} [TopologicalSpace M] [TopologicalSpace N] [T1Space N] {j : M → N} (hj : Topology.IsOpenEmbedding j) (x : M) (k : ℕ) : (localHomologyIsoOfIsOpenEmbedding R hj x k).hom = localHomologyMap R { toFun := j, continuous_toFun := ⋯ } ⋯ k

@[simp]

theorem TauCeti.localHomologyIsoOfIsOpenEmbedding_inv_comp_localHomologyMap {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M N : Type w} [TopologicalSpace M] [TopologicalSpace N] [T1Space N] {j : M → N} (hj : Topology.IsOpenEmbedding j) (x : M) (h : j ⁻¹' {j x} ⊆ {x}) (k : ℕ) : CategoryTheory.CategoryStruct.comp (localHomologyIsoOfIsOpenEmbedding R hj x k).inv (localHomologyMap R { toFun := j, continuous_toFun := ⋯ } h k) = CategoryTheory.CategoryStruct.id (localHomology R {j x} k)

The map of local homology induced by an open embedding undoes the inverse of localHomologyIsoOfIsOpenEmbedding.

@[simp]

theorem TauCeti.localHomologyIsoOfIsOpenEmbedding_inv_comp_localHomologyMap_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M N : Type w} [TopologicalSpace M] [TopologicalSpace N] [T1Space N] {j : M → N} (hj : Topology.IsOpenEmbedding j) (x : M) (h : j ⁻¹' {j x} ⊆ {x}) (k : ℕ) {Z : A} (h✝ : localHomology R {j x} k ⟶ Z) : CategoryTheory.CategoryStruct.comp (localHomologyIsoOfIsOpenEmbedding R hj x k).inv (CategoryTheory.CategoryStruct.comp (localHomologyMap R { toFun := j, continuous_toFun := ⋯ } h k) h✝) = h✝

The map of local homology induced by an open embedding undoes the inverse of localHomologyIsoOfIsOpenEmbedding.

@[simp]

theorem TauCeti.localHomologyIsoOfIsOpenEmbedding_inv_comp_localHomologyMap_apply {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M N : Type w} [TopologicalSpace M] [TopologicalSpace N] [T1Space N] {j : M → N} (hj : Topology.IsOpenEmbedding j) (x : M) (h : j ⁻¹' {j x} ⊆ {x}) (k : ℕ) {F : A → A → Type uF} {carrier : A → Type w_1} {instFunLike : (X Y : A) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory A F] (x✝ : carrier (localHomology R {j x} k)) : (CategoryTheory.ConcreteCategory.hom (localHomologyMap R { toFun := j, continuous_toFun := ⋯ } h k)) ((CategoryTheory.ConcreteCategory.hom (localHomologyIsoOfIsOpenEmbedding R hj x k).inv) x✝) = x✝

The map of local homology induced by an open embedding undoes the inverse of localHomologyIsoOfIsOpenEmbedding.

@[simp]

theorem TauCeti.localHomologyIsoOfIsOpenEmbedding_id {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M : Type w} [TopologicalSpace M] [T1Space M] (x : M) (k : ℕ) : localHomologyIsoOfIsOpenEmbedding R ⋯ x k = CategoryTheory.Iso.refl (localHomology R {x} k)

The isomorphism of local homology induced by the identity is the identity.

@[simp]

theorem TauCeti.localHomologyIsoOfIsOpenEmbedding_trans {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M N P : Type w} [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace P] [T1Space N] [T1Space P] {j : M → N} {j' : N → P} (hj : Topology.IsOpenEmbedding j) (hj' : Topology.IsOpenEmbedding j') (x : M) (k : ℕ) : localHomologyIsoOfIsOpenEmbedding R hj x k ≪≫ localHomologyIsoOfIsOpenEmbedding R hj' (j x) k = localHomologyIsoOfIsOpenEmbedding R ⋯ x k

The isomorphisms of local homology induced by open embeddings are functorial.

theorem TauCeti.localHomologyTransport_comp_localHomologyIsoOfIsOpenEmbedding_hom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M N : Type w} [TopologicalSpace M] [TopologicalSpace N] [T2Space N] {E : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E N] {j : M → N} [T2Space M] [ChartedSpace E M] (hj : Topology.IsOpenEmbedding j) (k : ℕ) {x y : FundamentalGroupoid M} (f : x ⟶ y) : CategoryTheory.CategoryStruct.comp (localHomologyTransport R M E k f) (localHomologyIsoOfIsOpenEmbedding R hj y.as k).hom = CategoryTheory.CategoryStruct.comp (localHomologyIsoOfIsOpenEmbedding R hj x.as k).hom (localHomologyTransport R N E k ((FundamentalGroupoid.map { toFun := j, continuous_toFun := ⋯ }).map f))

Open embeddings intertwine the transport of local homology. For an open embedding j : M → N of Hausdorff spaces modelled on the same finite-dimensional real normed space, the isomorphisms Hₖ(M, M ∖ {x}) ≅ Hₖ(N, N ∖ {j x}) induced by j carry the transport of local homology of M along a path class to the transport of local homology of N along its image.

theorem TauCeti.localHomologyTransport_comp_localHomologyIsoOfIsOpenEmbedding_hom_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M N : Type w} [TopologicalSpace M] [TopologicalSpace N] [T2Space N] {E : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E N] {j : M → N} [T2Space M] [ChartedSpace E M] (hj : Topology.IsOpenEmbedding j) (k : ℕ) {x y : FundamentalGroupoid M} (f : x ⟶ y) {Z : A} (h : localHomology R {j y.as} k ⟶ Z) : CategoryTheory.CategoryStruct.comp (localHomologyTransport R M E k f) (CategoryTheory.CategoryStruct.comp (localHomologyIsoOfIsOpenEmbedding R hj y.as k).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (localHomologyIsoOfIsOpenEmbedding R hj x.as k).hom (localHomologyTransport R N E k ((FundamentalGroupoid.map { toFun := j, continuous_toFun := ⋯ }).map f))) h

Open embeddings intertwine the transport of local homology. For an open embedding j : M → N of Hausdorff spaces modelled on the same finite-dimensional real normed space, the isomorphisms Hₖ(M, M ∖ {x}) ≅ Hₖ(N, N ∖ {j x}) induced by j carry the transport of local homology of M along a path class to the transport of local homology of N along its image.