Hopf problem: homology theory · singular mayer vietoris

Supporting definitions and proofs for this stage of the six-sphere construction.

The set-based standard simplex

Mathlib's Convexity.StdSimplex replaced the set stdSimplex ℝ ι ⊆ ι → ℝ on 2026-08-29. The singular chains below manipulate simplex coordinates as functions, so this section keeps the set-based simplex together with the small API the development uses; FirstHurewicz.toSimplex bridges to the bundled simplices underlying Mathlib's singular simplicial set.

@[reducible, inline]

noncomputable abbrev Mathoverflow1973.FirstHurewicz.singularComplex (X : Type) [TopologicalSpace X] : ChainComplex (ModuleCat ℤ) ℕ

The integral singular chain complex of a topological space.

Equations

• Mathoverflow1973.FirstHurewicz.singularComplex X = (TopCat.toSSet.obj ↧X).chainComplex ↧ℤ

@[reducible, inline]

noncomputable abbrev Mathoverflow1973.FirstHurewicz.Chains (X : Type) [TopologicalSpace X] (n : ℕ) : ModuleCat ℤ

The degree-n group of integral singular chains.

Equations

• Mathoverflow1973.FirstHurewicz.Chains X n = (Mathoverflow1973.FirstHurewicz.singularComplex X).X n

@[reducible, inline]

noncomputable abbrev Mathoverflow1973.FirstHurewicz.SingularH1 (X : Type) [TopologicalSpace X] : ModuleCat ℤ

The first integral singular homology group.

Equations

• Mathoverflow1973.FirstHurewicz.SingularH1 X = HomologicalComplex.homology (Mathoverflow1973.FirstHurewicz.singularComplex X) 1

@[reducible, inline]

abbrev Mathoverflow1973.FirstHurewicz.ChainHomology.ShortCycle (S : CategoryTheory.ShortComplex (ModuleCat ℤ)) : Submodule ℤ ↑S.X₂

The kernel defining cycles in a short complex.

Equations

• Mathoverflow1973.FirstHurewicz.ChainHomology.ShortCycle S = (ModuleCat.Hom.hom S.g).ker

@[instance_reducible]

def Mathoverflow1973.FirstHurewicz.ChainHomology.shortCycleModule (S : CategoryTheory.ShortComplex (ModuleCat ℤ)) : Module ℤ ↥(ShortCycle S)

The natural integer-module structure on short-complex cycles.

Equations

• Mathoverflow1973.FirstHurewicz.ChainHomology.shortCycleModule S = (ModuleCat.Hom.hom S.g).ker.module

@[reducible, inline]

noncomputable abbrev Mathoverflow1973.FirstHurewicz.ChainHomology.Cycle1 (K : ChainComplex (ModuleCat ℤ) ℕ) : Submodule ℤ ↑(HomologicalComplex.sc K 1).X₂

The one-cycles of a chain complex.

Equations

• Mathoverflow1973.FirstHurewicz.ChainHomology.Cycle1 K = Mathoverflow1973.FirstHurewicz.ChainHomology.ShortCycle (HomologicalComplex.sc K 1)

noncomputable def Mathoverflow1973.FirstHurewicz.ChainHomology.cycleClass (K : ChainComplex (ModuleCat ℤ) ℕ) : ↥(Cycle1 K) →ₗ[ℤ] ↑(HomologicalComplex.homology K 1)

The linear map sending a one-cycle to its homology class.

Equations

• Mathoverflow1973.FirstHurewicz.ChainHomology.cycleClass K = Mathoverflow1973.FirstHurewicz.ChainHomology.shortCycleClass✝ (HomologicalComplex.sc K 1)

@[reducible, inline]

noncomputable abbrev Mathoverflow1973.FirstHurewicz.Cycles1 (X : Type) [TopologicalSpace X] : Submodule ℤ ↑(HomologicalComplex.sc (singularComplex X) 1).X₂

The group of singular one-cycles of a topological space.

Equations

• Mathoverflow1973.FirstHurewicz.Cycles1 X = Mathoverflow1973.FirstHurewicz.ChainHomology.Cycle1 (Mathoverflow1973.FirstHurewicz.singularComplex X)

@[instance_reducible]

noncomputable instance Mathoverflow1973.FirstHurewicz.cycles1Module (X : Type) [TopologicalSpace X] : Module ℤ ↥(Cycles1 X)

Equations

• Mathoverflow1973.FirstHurewicz.cycles1Module X = Mathoverflow1973.FirstHurewicz.ChainHomology.shortCycleModule (HomologicalComplex.sc (Mathoverflow1973.FirstHurewicz.singularComplex X) 1)

@[reducible, inline]

noncomputable abbrev Mathoverflow1973.FirstHurewicz.cycleClass (X : Type) [TopologicalSpace X] : ↥(Cycles1 X) →ₗ[ℤ] ↑(SingularH1 X)

The linear map from singular one-cycles to first homology.

Equations

• Mathoverflow1973.FirstHurewicz.cycleClass X = Mathoverflow1973.FirstHurewicz.ChainHomology.cycleClass (Mathoverflow1973.FirstHurewicz.singularComplex X)

@[reducible, inline]

noncomputable abbrev Mathoverflow1973.FirstHurewicz.singularChainMap {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : singularComplex X ⟶ singularComplex Y

The chain map on singular complexes induced by a continuous map.

Equations

• Mathoverflow1973.FirstHurewicz.singularChainMap f = SSet.chainComplexMap (TopCat.toSSet.map (TopCat.ofHom f)) ↧ℤ

@[reducible, inline]

noncomputable abbrev Mathoverflow1973.SingularMayerVietoris.homologyLinearMap {K L : ChainComplex (ModuleCat ℤ) ℕ} (f : K ⟶ L) (n : ℕ) : ↑(HomologicalComplex.homology K n) →ₗ[ℤ] ↑(HomologicalComplex.homology L n)

The linear map on homology induced by a chain map.

Equations

• Mathoverflow1973.SingularMayerVietoris.homologyLinearMap f n = ModuleCat.Hom.hom (HomologicalComplex.homologyMap f n)

@[reducible, inline]

noncomputable abbrev Mathoverflow1973.SingularMayerVietoris.SingularHomology (Y : Type) [TopologicalSpace Y] (n : ℕ) : ModuleCat ℤ

Integral singular homology in a specified degree.

Equations

• Mathoverflow1973.SingularMayerVietoris.SingularHomology Y n = HomologicalComplex.homology (Mathoverflow1973.FirstHurewicz.singularComplex Y) n

@[reducible, inline]

noncomputable abbrev Mathoverflow1973.SingularMayerVietoris.singularHomologyMap {Y Z : Type} [TopologicalSpace Y] [TopologicalSpace Z] (f : C(Y, Z)) (n : ℕ) : ↑(SingularHomology Y n) →ₗ[ℤ] ↑(SingularHomology Z n)

The map on singular homology induced by a continuous map.

Equations

• Mathoverflow1973.SingularMayerVietoris.singularHomologyMap f n = Mathoverflow1973.SingularMayerVietoris.homologyLinearMap (Mathoverflow1973.FirstHurewicz.singularChainMap f) n

@[reducible, inline]

abbrev Mathoverflow1973.SingularMayerVietoris.FormalChains (V : Type u_1) (n : ℕ) : Type u_1

Formal integer combinations of ordered n-tuples of vertices.

Equations

• Mathoverflow1973.SingularMayerVietoris.FormalChains V n = ((Fin n → V) →₀ ℤ)

def Mathoverflow1973.SingularMayerVietoris.formalChainsSupported {V : Type u_1} (S : Set V) (n : ℕ) : Submodule ℤ (FormalChains V n)

The submodule of formal chains whose vertices lie in a specified set.

Equations

• Mathoverflow1973.SingularMayerVietoris.formalChainsSupported S n = Finsupp.supported ℤ ℤ {v : Fin n → V | ∀ (i : Fin n), v i ∈ S}