Documentation

TauCeti.AlgebraicTopology.Singular.LocalHomology.TopHomology

The top homology of a compact manifold #

Let M be a Hausdorff space modelled on a real normed space E of finite dimension n, that is, a topological n-manifold without boundary. Restricting a class of Hₖ(M, M ∖ M) to the points of M gives a cone TauCeti.localHomologySystemCone over the local homology system x ↦ Hₖ(M, M ∖ {x}): the restrictions of a global class are compatible with the transport of local homology along paths (TauCeti.localHomologyRestriction_univ_comp_localHomologyTransport). The cone point Hₖ(M, M ∖ M) = Hₖ(M, ∅) is identified with Hₖ(M) by the ordinary-to-relative quotient map.

For M compact, with coefficients in a module, this cone is a limit cone in degree n (TauCeti.isLimitLocalHomologySystemCone): the top homology Hₙ(M) is the module of transport-invariant families of local homology classes, the global sections of the local homology system. This is Hatcher's description of Hₙ(M; R) by sections of the covering space M_R.

If M is moreover connected, a transport-invariant family is determined by its value at one point x. So the restriction Hₙ(M) ⟶ Hₙ(M, M ∖ {x}) is injective (TauCeti.localHomologySystemCone_π_app_injective). Its image consists of the local classes fixed by the transport along every loop at x (TauCeti.mem_range_localHomologySystemCone_π_app_iff), with no connectedness needed. In particular, for a compact simply connected manifold the restriction is an isomorphism (TauCeti.isIso_localHomologySystemCone_π_app), so that Hₙ(M; N) ≅ N for n > 0 (TauCeti.singularHomologyIsoOfSimplyConnectedSpace).

No orientability hypothesis is involved: orientability enters only through the action of loops at x on the local homology Hₙ(M, M ∖ {x}), which is trivial when M is simply connected.

Main results #

References #

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

The restrictions Hₖ(M, M ∖ M) ⟶ Hₖ(M, M ∖ {x}) to the points of M, as a cone over the local homology system. The cone point Hₖ(M, M ∖ M) = Hₖ(M, ∅) is the singular homology of M, through the ordinary-to-relative quotient map.

Instances For
    source
    @[simp]
    theorem TauCeti.localHomologySystemCone_pt {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (M E : Type w) [TopologicalSpace M] [T2Space M] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] (k : ℕ) :
    (localHomologySystemCone R M E k).pt = localHomology R Set.univ k
    source
    @[simp]
    theorem TauCeti.localHomologySystemCone_π_app {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (M E : Type w) [TopologicalSpace M] [T2Space M] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] (k : ℕ) (x : FundamentalGroupoid M) :
    (localHomologySystemCone R M E k).π.app x = localHomologyRestriction R ⋯ k
    source
    noncomputable def TauCeti.isLimitLocalHomologySystemCone {Λ : Type w} [Ring Λ] (N : ModuleCat Λ) (M E : Type w) [TopologicalSpace M] [T2Space M] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] [CompactSpace M] {n : ℕ} (hn : Module.finrank ℝ E = n) :
    CategoryTheory.Limits.IsLimit (localHomologySystemCone N M E n)

    The top homology of a compact manifold is the module of parallel families of local classes. For a compact Hausdorff space modelled on a real normed space of finite dimension n, the restrictions Hₙ(M, M ∖ M; N) ⟶ Hₙ(M, M ∖ {x}; N) exhibit Hₙ(M, M ∖ M; N) as the limit of the local homology system: every transport-invariant family of local classes is the family of restrictions of exactly one class.

    Instances For
      source
      theorem TauCeti.localHomologySystemCone_π_app_injective {Λ : Type w} [Ring Λ] (N : ModuleCat Λ) {M E : Type w} [TopologicalSpace M] [T2Space M] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] [CompactSpace M] [ConnectedSpace M] {n : ℕ} (hn : Module.finrank ℝ E = n) (x : FundamentalGroupoid M) :
      Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((localHomologySystemCone N M E n).π.app x))

      Restriction to a point is injective on the top homology of a compact connected manifold: a class of Hₙ(M, M ∖ M; N) is determined by its image in the local homology Hₙ(M, M ∖ {x}; N) at any single point.

      source
      theorem TauCeti.mem_range_localHomologySystemCone_π_app_iff {Λ : Type w} [Ring Λ] (N : ModuleCat Λ) {M E : Type w} [TopologicalSpace M] [T2Space M] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] [CompactSpace M] {n : ℕ} (hn : Module.finrank ℝ E = n) (x : FundamentalGroupoid M) (z : ↑(localHomology N {x.as} n)) :
      z ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom ((localHomologySystemCone N M E n).π.app x)) ↔ ∀ (g : x ⟶ x), (CategoryTheory.ConcreteCategory.hom (localHomologyTransport N M E n g)) z = z

      The image of the top homology of a compact manifold in local homology. A local class at x is the restriction of a class of Hₙ(M, M ∖ M; N) exactly when it is fixed by the transport of local homology along every loop at x. Connectedness is not needed: off the path component of x the family of local classes is extended by zero.

      source
      theorem TauCeti.isIso_localHomologySystemCone_π_app {Λ : Type w} [Ring Λ] (N : ModuleCat Λ) {M E : Type w} [TopologicalSpace M] [T2Space M] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] [CompactSpace M] [SimplyConnectedSpace M] {n : ℕ} (hn : Module.finrank ℝ E = n) (x : FundamentalGroupoid M) :
      CategoryTheory.IsIso ((localHomologySystemCone N M E n).π.app x)

      The top homology of a compact simply connected manifold is local homology at a point. For a compact simply connected Hausdorff space modelled on a real normed space of finite dimension n, the restriction Hₙ(M, M ∖ M; N) ⟶ Hₙ(M, M ∖ {x}; N) is an isomorphism.

      source
      noncomputable def TauCeti.singularHomologyIsoOfSimplyConnectedSpace {Λ : Type w} [Ring Λ] (N : ModuleCat Λ) {M E : Type w} [TopologicalSpace M] [T2Space M] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] [CompactSpace M] [SimplyConnectedSpace M] {n : ℕ} (hn : Module.finrank ℝ E = n + 1) (x : M) :
      (TopCat.toSSet.obj ↧M).homology N (n + 1) ≅ N

      The top homology of a compact simply connected manifold. For a compact simply connected Hausdorff space modelled on a real normed space of finite dimension n + 1, the singular homology Hₙ₊₁(M; N) is a copy of N. The isomorphism is the quotient map to Hₙ₊₁(M, M ∖ M; N), followed by restriction to the local homology at x and the chart computation of local homology there.

      Instances For
        source
        theorem TauCeti.singularHomologyIsoOfSimplyConnectedSpace_hom {Λ : Type w} [Ring Λ] (N : ModuleCat Λ) {M E : Type w} [TopologicalSpace M] [T2Space M] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [ChartedSpace E M] [CompactSpace M] [SimplyConnectedSpace M] {n : ℕ} (hn : Module.finrank ℝ E = n + 1) (x : M) :
        (singularHomologyIsoOfSimplyConnectedSpace N hn x).hom = CategoryTheory.CategoryStruct.comp ((TopPair.ofSubset Set.univᶜ).singularHomologyπ N (n + 1)) (CategoryTheory.CategoryStruct.comp (localHomologyRestriction N ⋯ (n + 1)) (singularHomologyComplSingletonIsoOfFinrankEq N (chartAt E x) ⋯ hn).hom)

        The isomorphism Hₙ₊₁(M; N) ≅ N of a compact simply connected manifold is the quotient map to relative homology, followed by restriction to the local homology at x and the chart computation of local homology.