Small Chains Homology Injectivity #
theorem
SphereOddDegree.exists_d_eq_iCycles_of_homologyπ_zero
{R : Type}
[CommRing R]
(K : ChainComplex (ModuleCat R) ℕ)
(n : ℕ)
(W : ↑(HomologicalComplex.cycles K n))
(h : (ModuleCat.Hom.hom (HomologicalComplex.homologyπ K n)) W = 0)
:
∃ (b : ↑(K.X (n + 1))), (ModuleCat.Hom.hom (K.d (n + 1) n)) b = (ModuleCat.Hom.hom (HomologicalComplex.iCycles K n)) W
theorem
SphereOddDegree.homologyπ_zero_of_iCycles_eq_d
{R : Type}
[CommRing R]
(K : ChainComplex (ModuleCat R) ℕ)
(n : ℕ)
(W : ↑(HomologicalComplex.cycles K n))
(b : ↑(K.X (n + 1)))
(h : (ModuleCat.Hom.hom (HomologicalComplex.iCycles K n)) W = (ModuleCat.Hom.hom (K.d (n + 1) n)) b)
:
theorem
SphereOddDegree.iterHomotopyBoundaryTerm_eq_zero_of_full_cycle
(R : Type)
[CommRing R]
(X : TopCat)
(N n : ℕ)
(z : ↑(AffineBarycentricSubdivision.singularChainGroup R X n))
(hz :
(ModuleCat.Hom.hom ((AffineBarycentricSubdivision.singularChainComplex R X).d n ((ComplexShape.down ℕ).next n))) z = 0)
:
theorem
SphereOddDegree.exists_small_boundary_witness
{X : TopCat}
(𝒰 : OpenCoverData X)
(R : Type)
[CommRing R]
(n : ℕ)
(b : ↑(AffineBarycentricSubdivision.singularChainGroup R X (n + 1)))
(hsmall : (ModuleCat.Hom.hom (AffineBarycentricSubdivision.singularBoundary R X n)) b ∈ smallChainSubmodule R X 𝒰 n)
:
∃ bChain ∈ smallChainSubmodule R X 𝒰 (n + 1),
(ModuleCat.Hom.hom (AffineBarycentricSubdivision.singularBoundary R X n)) bChain = (ModuleCat.Hom.hom (AffineBarycentricSubdivision.singularBoundary R X n)) b
theorem
SphereOddDegree.smallChainsInclusion_injective_on_homology
(R : Type)
[CommRing R]
(X : TopCat)
(𝒰 : OpenCoverData X)
(n : ℕ)
: