The local homology system of a manifold

Let M be a Hausdorff space modelled on a finite-dimensional real normed space E, that is, a topological manifold without boundary. This file assembles the local homology groups Hₖ(M, M ∖ {x}) into a functor out of the fundamental groupoid of M, TauCeti.localHomologySystem R M E k. For k = dim E and integer coefficients this is the orientation local system of M: a local orientation at x is a generator of Hₙ(M, M ∖ {x}; ℤ), and the functor transports local orientations along paths. With A = ModuleCat S for a ring S it is a TauCeti.LocalCoefficientSystem.

The transport is determined by compact convex sets in charts. Let φ : M → E be an open partial homeomorphism and let K ⊆ φ.target be compact and convex. For every x with φ x ∈ K, the restriction Hₖ(M, M ∖ φ.symm '' K) ⟶ Hₖ(M, M ∖ {x}) is an isomorphism (TauCeti.isIso_localHomologyRestriction_symm_image). The transport along a path inside φ.symm '' K is the unique map compatible with these restrictions at its two endpoints (TauCeti.localHomologyRestriction_comp_localHomologyTransport), and this property together with compatibility with composition characterizes the transport (TauCeti.eq_localHomologyTransport).

Main definitions and results

• TauCeti.localHomology R S k: the relative singular homology Hₖ(M, M ∖ S).
• TauCeti.localHomologyRestriction: for S ⊆ T, the map Hₖ(M, M ∖ T) ⟶ Hₖ(M, M ∖ S) induced by the identity of M.
• TauCeti.localHomologyMap: for a continuous map j : M → N with j ⁻¹' T ⊆ S, the map Hₖ(M, M ∖ S) ⟶ Hₖ(N, N ∖ T) induced by j. It is functorial, is the restriction map for j the identity, and is compatible with restriction on both sides.
• TauCeti.isZero_localHomology_empty: Hₖ(M, M) = 0.
• TauCeti.isIso_localHomologyRestriction_symm_image: the restriction from a compact set in a chart, star-convex about one of its points, to that point is an isomorphism.
• TauCeti.localHomologyTransport: the transport of local homology along a path class.
• TauCeti.localHomologySystem: the local homology groups as a functor out of the fundamental groupoid, with these transport maps.
• TauCeti.localHomologyRestriction_comp_localHomologyTransport: the transport along a path inside a compact convex set in a chart.
• TauCeti.eq_localHomologyTransport: the transport is the only family of maps compatible with composition that has this property.

Implementation notes

On each open convex patch of a chart there is a functor sending a path to the comparison of its endpoints through the closure of the patch. Two patches give the same comparison near each point of their overlap, since both factor through a small ball in one chart. So the local functors agree on overlaps, and they glue (TauCeti.FundamentalGroupoid.glue) to a functor out of the fundamental groupoid of M.

References

• A. Hatcher, Algebraic Topology, Section 3.3, the local homology groups Hₙ(M | x), local orientations, and the comparison through Hₙ(M | B) for balls B in charts, which Hatcher uses to topologize the orientation covering M_R.

@[reducible, inline]

noncomputable abbrev TauCeti.localHomology {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M : Type w} [TopologicalSpace M] (S : Set M) (k : ℕ) : A

The relative singular homology Hₖ(M, M ∖ S) of M modulo the complement of S. For S = {x} it is the local homology of M at x.

noncomputable def TauCeti.localHomologyRestriction {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M : Type w} [TopologicalSpace M] {S T : Set M} (h : S ⊆ T) (k : ℕ) : localHomology R T k ⟶ localHomology R S k

For S ⊆ T, the map Hₖ(M, M ∖ T) ⟶ Hₖ(M, M ∖ S) on relative singular homology induced by the identity of M.

theorem TauCeti.localHomologyRestriction_def {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M : Type w} [TopologicalSpace M] {S T : Set M} (h : S ⊆ T) (k : ℕ) : localHomologyRestriction R h k = TopPair.singularHomologyMap (TopPair.ofSubsetMap (CategoryTheory.CategoryStruct.id ↧M) ⋯) R k

@[simp]

theorem TauCeti.localHomologyRestriction_refl {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M : Type w} [TopologicalSpace M] (S : Set M) (k : ℕ) : localHomologyRestriction R ⋯ k = CategoryTheory.CategoryStruct.id (localHomology R S k)

@[simp]

theorem TauCeti.localHomologyRestriction_comp {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M : Type w} [TopologicalSpace M] {S T W : Set M} (h₁ : S ⊆ T) (h₂ : T ⊆ W) (k : ℕ) : CategoryTheory.CategoryStruct.comp (localHomologyRestriction R h₂ k) (localHomologyRestriction R h₁ k) = localHomologyRestriction R ⋯ k

@[simp]

theorem TauCeti.localHomologyRestriction_comp_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M : Type w} [TopologicalSpace M] {S T W : Set M} (h₁ : S ⊆ T) (h₂ : T ⊆ W) (k : ℕ) {Z : A} (h : localHomology R S k ⟶ Z) : CategoryTheory.CategoryStruct.comp (localHomologyRestriction R h₂ k) (CategoryTheory.CategoryStruct.comp (localHomologyRestriction R h₁ k) h) = CategoryTheory.CategoryStruct.comp (localHomologyRestriction R ⋯ k) h

@[simp]

theorem TauCeti.localHomologyRestriction_comp_apply {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M : Type w} [TopologicalSpace M] {S T W : Set M} (h₁ : S ⊆ T) (h₂ : T ⊆ W) (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 W k)) : (CategoryTheory.ConcreteCategory.hom (localHomologyRestriction R h₁ k)) ((CategoryTheory.ConcreteCategory.hom (localHomologyRestriction R h₂ k)) x) = (CategoryTheory.ConcreteCategory.hom (localHomologyRestriction R ⋯ k)) x

theorem TauCeti.isZero_localHomology_empty {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M : Type w} [TopologicalSpace M] (k : ℕ) : CategoryTheory.Limits.IsZero (localHomology R ∅ k)

Local homology along the empty set vanishes: Hₖ(M, M) = 0.

noncomputable def TauCeti.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)) {S : Set M} {T : Set N} (h : ⇑j ⁻¹' T ⊆ S) (k : ℕ) : localHomology R S k ⟶ localHomology R T k

For a continuous map j : M → N and sets S ⊆ M, T ⊆ N with j ⁻¹' T ⊆ S, the map Hₖ(M, M ∖ S) ⟶ Hₖ(N, N ∖ T) of local homology induced by the map of pairs j : (M, M ∖ S) ⟶ (N, N ∖ T).

theorem TauCeti.localHomologyMap_def {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)) {S : Set M} {T : Set N} (h : ⇑j ⁻¹' T ⊆ S) (k : ℕ) : localHomologyMap R j h k = TopPair.singularHomologyMap (TopPair.ofSubsetMap (TopCat.ofHom j) ⋯) R k

theorem TauCeti.localHomologyMap_congr {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₁ j₂ : C(M, N)} (hj : j₁ = j₂) {S : Set M} {T : Set N} (h : ⇑j₁ ⁻¹' T ⊆ S) (k : ℕ) : localHomologyMap R j₁ h k = localHomologyMap R j₂ ⋯ k

Equal continuous maps induce equal maps of local homology, with the preimage hypothesis transported along the equality.

@[simp]

theorem TauCeti.localHomologyMap_id {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M : Type w} [TopologicalSpace M] {S T : Set M} (h : ⇑(ContinuousMap.id M) ⁻¹' T ⊆ S) (k : ℕ) : localHomologyMap R (ContinuousMap.id M) h k = localHomologyRestriction R h k

The map of local homology induced by the identity is the restriction map.

@[simp]

theorem TauCeti.localHomologyMap_comp {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] (j : C(M, N)) (j' : C(N, P)) {S : Set M} {T : Set N} {W : Set P} (h : ⇑j ⁻¹' T ⊆ S) (h' : ⇑j' ⁻¹' W ⊆ T) (k : ℕ) : CategoryTheory.CategoryStruct.comp (localHomologyMap R j h k) (localHomologyMap R j' h' k) = localHomologyMap R (j'.comp j) ⋯ k

The maps of local homology are functorial.

@[simp]

theorem TauCeti.localHomologyMap_comp_assoc {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] (j : C(M, N)) (j' : C(N, P)) {S : Set M} {T : Set N} {W : Set P} (h : ⇑j ⁻¹' T ⊆ S) (h' : ⇑j' ⁻¹' W ⊆ T) (k : ℕ) {Z : A} (h✝ : localHomology R W k ⟶ Z) : CategoryTheory.CategoryStruct.comp (localHomologyMap R j h k) (CategoryTheory.CategoryStruct.comp (localHomologyMap R j' h' k) h✝) = CategoryTheory.CategoryStruct.comp (localHomologyMap R (j'.comp j) ⋯ k) h✝

The maps of local homology are functorial.

@[simp]

theorem TauCeti.localHomologyRestriction_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] (j : C(M, N)) {S S' : Set M} {T : Set N} (hS : S ⊆ S') (h : ⇑j ⁻¹' T ⊆ S) (k : ℕ) : CategoryTheory.CategoryStruct.comp (localHomologyRestriction R hS k) (localHomologyMap R j h k) = localHomologyMap R j ⋯ k

Restricting before the map of local homology is the map from the larger set.

@[simp]

theorem TauCeti.localHomologyRestriction_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] (j : C(M, N)) {S S' : Set M} {T : Set N} (hS : S ⊆ S') (h : ⇑j ⁻¹' T ⊆ S) (k : ℕ) {Z : A} (h✝ : localHomology R T k ⟶ Z) : CategoryTheory.CategoryStruct.comp (localHomologyRestriction R hS k) (CategoryTheory.CategoryStruct.comp (localHomologyMap R j h k) h✝) = CategoryTheory.CategoryStruct.comp (localHomologyMap R j ⋯ k) h✝

Restricting before the map of local homology is the map from the larger set.

@[simp]

theorem TauCeti.localHomologyMap_comp_localHomologyRestriction {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)) {S : Set M} {T T' : Set N} (hT : T ⊆ T') (h : ⇑j ⁻¹' T' ⊆ S) (k : ℕ) : CategoryTheory.CategoryStruct.comp (localHomologyMap R j h k) (localHomologyRestriction R hT k) = localHomologyMap R j ⋯ k

Restricting after the map of local homology is the map to the smaller set.

@[simp]

theorem TauCeti.localHomologyMap_comp_localHomologyRestriction_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] (j : C(M, N)) {S : Set M} {T T' : Set N} (hT : T ⊆ T') (h : ⇑j ⁻¹' T' ⊆ S) (k : ℕ) {Z : A} (h✝ : localHomology R T k ⟶ Z) : CategoryTheory.CategoryStruct.comp (localHomologyMap R j h k) (CategoryTheory.CategoryStruct.comp (localHomologyRestriction R hT k) h✝) = CategoryTheory.CategoryStruct.comp (localHomologyMap R j ⋯ k) h✝

Restricting after the map of local homology is the map to the smaller set.

theorem TauCeti.localHomologyMap_eq_of_homotopy {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₀ j₁ : C(M, N)} (F : j₀.Homotopy j₁) {S : Set M} {T : Set N} (hF : ∀ (τ : ↑unitInterval), ∀ y ∉ S, F (τ, y) ∉ T) (h₀ : ⇑j₀ ⁻¹' T ⊆ S) (h₁ : ⇑j₁ ⁻¹' T ⊆ S) (k : ℕ) : localHomologyMap R j₀ h₀ k = localHomologyMap R j₁ h₁ k

Homotopy invariance of the maps of local homology. Maps j₀, j₁ : M → N joined by a homotopy that never sends a point outside S into T induce the same map Hₖ(M, M ∖ S) ⟶ Hₖ(N, N ∖ T).

theorem TauCeti.isIso_localHomologyRestriction_symm_image {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M : Type w} [TopologicalSpace M] {E : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [T2Space M] (φ : OpenPartialHomeomorph M E) {K : Set E} {x : M} (hK : StarConvex ℝ (↑φ x) K) (hKc : IsCompact K) (hKφ : K ⊆ φ.target) (hx : x ∈ φ.source) (hxK : ↑φ x ∈ K) (k : ℕ) : CategoryTheory.IsIso (localHomologyRestriction R ⋯ k)

Local homology is constant along a compact star-convex set in a chart. If K ⊆ φ.target is compact and star-convex about φ x ∈ K, then the restriction Hₖ(M, M ∖ φ.symm '' K) ⟶ Hₖ(M, M ∖ {x}) is an isomorphism.

theorem TauCeti.exists_isCompact_mem_nhds_isIso_localHomologyRestriction {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M : Type w} [TopologicalSpace M] {E : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [T2Space M] [ChartedSpace E M] [FiniteDimensional ℝ E] (x : M) (k : ℕ) : ∃ B ∈ nhds x, IsCompact B ∧ ∀ (y : M) (hy : y ∈ B), CategoryTheory.IsIso (localHomologyRestriction R ⋯ k)

Every point of a manifold has a compact neighbourhood along which local homology is constant. If M is a Hausdorff space modelled on a finite-dimensional real normed space, every x ∈ M has a compact neighbourhood B, the image under a chart of a closed ball, such that the restriction Hₖ(M, M ∖ B) ⟶ Hₖ(M, M ∖ {y}) is an isomorphism for every y ∈ B.

noncomputable def TauCeti.localHomologyTransport {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (M : Type w) [TopologicalSpace M] (E : Type w) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [T2Space M] [ChartedSpace E M] (k : ℕ) {x y : FundamentalGroupoid M} (f : x ⟶ y) : localHomology R {x.as} k ⟶ localHomology R {y.as} k

The transport Hₖ(M, M ∖ {x}) ⟶ Hₖ(M, M ∖ {y}) of local homology along a path class from x to y, for a Hausdorff space M modelled on a finite-dimensional real normed space E. Along a path inside a compact convex set of a chart it is described by TauCeti.localHomologyRestriction_comp_localHomologyTransport.

@[simp]

theorem TauCeti.localHomologyTransport_id {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (M : Type w) [TopologicalSpace M] (E : Type w) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [T2Space M] [ChartedSpace E M] (k : ℕ) (x : FundamentalGroupoid M) : localHomologyTransport R M E k (CategoryTheory.CategoryStruct.id x) = CategoryTheory.CategoryStruct.id (localHomology R {x.as} k)

@[simp]

theorem TauCeti.localHomologyTransport_comp {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (M : Type w) [TopologicalSpace M] (E : Type w) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [T2Space M] [ChartedSpace E M] (k : ℕ) {x y z : FundamentalGroupoid M} (f : x ⟶ y) (g : y ⟶ z) : localHomologyTransport R M E k (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (localHomologyTransport R M E k f) (localHomologyTransport R M E k g)

noncomputable def TauCeti.localHomologySystem {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (M : Type w) [TopologicalSpace M] (E : Type w) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [T2Space M] [ChartedSpace E M] (k : ℕ) : CategoryTheory.Functor (FundamentalGroupoid M) A

The local homology system. For a Hausdorff space M modelled on a finite-dimensional real normed space E, the local homology groups Hₖ(M, M ∖ {x}) form a functor out of the fundamental groupoid of M, with the transport maps TauCeti.localHomologyTransport. For k = dim E and integer coefficients it is the orientation local system of M.

@[simp]

theorem TauCeti.localHomologySystem_obj {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (M : Type w) [TopologicalSpace M] (E : Type w) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [T2Space M] [ChartedSpace E M] (k : ℕ) (x : FundamentalGroupoid M) : (localHomologySystem R M E k).obj x = localHomology R {x.as} k

@[simp]

theorem TauCeti.localHomologySystem_map {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (M : Type w) [TopologicalSpace M] (E : Type w) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [T2Space M] [ChartedSpace E M] (k : ℕ) {X✝ Y✝ : FundamentalGroupoid M} (f : X✝ ⟶ Y✝) : (localHomologySystem R M E k).map f = localHomologyTransport R M E k f

theorem TauCeti.localHomologyRestriction_comp_localHomologyTransport {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M : Type w} [TopologicalSpace M] {E : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [T2Space M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) {K : Set E} (hK : Convex ℝ K) (hKc : IsCompact K) (hKφ : K ⊆ φ.target) {x y : M} (γ : Path x y) (hγ : ∀ (t : ↑unitInterval), γ t ∈ ↑φ.symm '' K) (k : ℕ) : CategoryTheory.CategoryStruct.comp (localHomologyRestriction R ⋯ k) (localHomologyTransport R M E k (Path.Homotopic.Quotient.mk γ)) = localHomologyRestriction R ⋯ k

Transport of local homology along a path in a chart. Let K ⊆ φ.target be compact and convex, and let γ be a path from x to y inside φ.symm '' K. Then the transport along γ is compatible with the restrictions Hₖ(M, M ∖ φ.symm '' K) ⟶ Hₖ(M, M ∖ {x}) and Hₖ(M, M ∖ φ.symm '' K) ⟶ Hₖ(M, M ∖ {y}). Since the first of these is an isomorphism (TauCeti.isIso_localHomologyRestriction_symm_image), this determines the transport.

theorem TauCeti.eq_localHomologyTransport {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M : Type w} [TopologicalSpace M] {E : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [T2Space M] [ChartedSpace E M] (k : ℕ) (t : {x y : FundamentalGroupoid M} → (x ⟶ y) → (localHomology R {x.as} k ⟶ localHomology R {y.as} k)) (ht : ∀ {x y z : FundamentalGroupoid M} (f : x ⟶ y) (g : y ⟶ z), t (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (t f) (t g)) (hchart : ∀ (φ : OpenPartialHomeomorph M E) {K : Set E}, Convex ℝ K → IsCompact K → K ⊆ φ.target → ∀ {x y : M} (γ : Path x y) (hγ : ∀ (s : ↑unitInterval), γ s ∈ ↑φ.symm '' K), CategoryTheory.CategoryStruct.comp (localHomologyRestriction R ⋯ k) (t (Path.Homotopic.Quotient.mk γ)) = localHomologyRestriction R ⋯ k) {x y : FundamentalGroupoid M} (f : x ⟶ y) : t f = localHomologyTransport R M E k f

Uniqueness of the transport. A family of maps Hₖ(M, M ∖ {x}) ⟶ Hₖ(M, M ∖ {y}) indexed by path classes from x to y, compatible with composition and satisfying the conclusion of TauCeti.localHomologyRestriction_comp_localHomologyTransport along paths inside compact convex sets of charts, is the transport TauCeti.localHomologyTransport.

@[simp]

theorem TauCeti.localHomologyRestriction_univ_comp_localHomologyTransport {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M : Type w} [TopologicalSpace M] {E : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [T2Space M] [ChartedSpace E M] (k : ℕ) {x y : FundamentalGroupoid M} (f : x ⟶ y) : CategoryTheory.CategoryStruct.comp (localHomologyRestriction R ⋯ k) (localHomologyTransport R M E k f) = localHomologyRestriction R ⋯ k

Restrictions of a global class are parallel. The restrictions Hₖ(M, M ∖ M) ⟶ Hₖ(M, M ∖ {x}) to the points of M are compatible with the transport of local homology along every path class, in every degree.

@[simp]

theorem TauCeti.localHomologyRestriction_univ_comp_localHomologyTransport_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {M : Type w} [TopologicalSpace M] {E : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [T2Space M] [ChartedSpace E M] (k : ℕ) {x y : FundamentalGroupoid M} (f : x ⟶ y) {Z : A} (h : localHomology R {y.as} k ⟶ Z) : CategoryTheory.CategoryStruct.comp (localHomologyRestriction R ⋯ k) (CategoryTheory.CategoryStruct.comp (localHomologyTransport R M E k f) h) = CategoryTheory.CategoryStruct.comp (localHomologyRestriction R ⋯ k) h

Restrictions of a global class are parallel. The restrictions Hₖ(M, M ∖ M) ⟶ Hₖ(M, M ∖ {x}) to the points of M are compatible with the transport of local homology along every path class, in every degree.