Singular H0Path Connected

theorem SphereOddDegree.prev_zero : (ComplexShape.down ℕ).prev 0 = 1

theorem SphereOddDegree.aug_comp_boundary_eq_zero (Y : TopCat) : CategoryTheory.CategoryStruct.comp ((AffineBarycentricSubdivision.singularChainComplex ℤ Y).d 1 0) (aug Y) = 0

noncomputable def SphereOddDegree.H0aug (Y : TopCat) : HomologicalComplex.homology (AffineBarycentricSubdivision.singularChainComplex ℤ Y) 0 ⟶ ↧ℤ

The augmentation induced on zeroth singular homology.

Equations

• One or more equations did not get rendered due to their size.

theorem SphereOddDegree.aug_natural {Y Z : TopCat} (f : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (AffineBarycentricSubdivision.singularChainMap ℤ f 0) (aug Z) = aug Y

theorem SphereOddDegree.opcyclesMap_descOpcycles {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {K L : HomologicalComplex C (ComplexShape.down ℕ)} (φ : K ⟶ L) {A : C} (kL : L.X 0 ⟶ A) (kK : K.X 0 ⟶ A) (prev_zero : (ComplexShape.down ℕ).prev 0 = 1) (hkL : CategoryTheory.CategoryStruct.comp (L.d 1 0) kL = 0) (hkK : CategoryTheory.CategoryStruct.comp (K.d 1 0) kK = 0) (h_comm : CategoryTheory.CategoryStruct.comp (φ.f 0) kL = kK) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ 0) (L.descOpcycles kL 1 prev_zero hkL) = K.descOpcycles kK 1 prev_zero hkK

theorem SphereOddDegree.H0aug_natural {Y Z : TopCat} (f : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((singularHomologyℤ 0).map f) (H0aug Z) = H0aug Y

instance SphereOddDegree.isIso_homologyι_zero (Y : TopCat) : CategoryTheory.IsIso (HomologicalComplex.homologyι (AffineBarycentricSubdivision.singularChainComplex ℤ Y) 0)

theorem SphereOddDegree.descOpcycles_eval (Y : TopCat) (c : ↑(AffineBarycentricSubdivision.singularChainGroup ℤ Y 0)) : (ModuleCat.Hom.hom (aug Y)) c = (ModuleCat.Hom.hom (HomologicalComplex.descOpcycles (AffineBarycentricSubdivision.singularChainComplex ℤ Y) (aug Y) 1 prev_zero ⋯)) ((ModuleCat.Hom.hom (HomologicalComplex.pOpcycles (AffineBarycentricSubdivision.singularChainComplex ℤ Y) 0)) c)

theorem SphereOddDegree.d_one_comp_pOpcycles (K : HomologicalComplex (ModuleCat ℤ) (ComplexShape.down ℕ)) : CategoryTheory.CategoryStruct.comp (K.d 1 0) (K.pOpcycles 0) = 0

theorem SphereOddDegree.isIso_descOpcycles_aug (Y : TopCat) [Nonempty ↑Y] [PathConnectedSpace ↑Y] : CategoryTheory.IsIso (HomologicalComplex.descOpcycles (AffineBarycentricSubdivision.singularChainComplex ℤ Y) (aug Y) 1 prev_zero ⋯)

instance SphereOddDegree.isIso_H0aug (Y : TopCat) [Nonempty ↑Y] [PathConnectedSpace ↑Y] : CategoryTheory.IsIso (H0aug Y)

theorem SphereOddDegree.surjective_H0aug (Y : TopCat) [Nonempty ↑Y] : Function.Surjective ⇑(ModuleCat.Hom.hom (H0aug Y))

noncomputable def SphereOddDegree.subH0aug (X : TopCat) (S : Set ↑X) : HomologicalComplex.homology (subChainComplex ℤ X S) 0 ⟶ ↧ℤ

The zeroth-homology augmentation for chains supported in a subset.

Equations

• SphereOddDegree.subH0aug X S = CategoryTheory.CategoryStruct.comp (SphereOddDegree.subspaceHomologyIso S 0).hom (SphereOddDegree.H0aug ↧↑S)

instance SphereOddDegree.isIso_subH0aug (X : TopCat) (S : Set ↑X) [Nonempty ↑S] [PathConnectedSpace ↑S] : CategoryTheory.IsIso (subH0aug X S)

def SphereOddDegree.setInclusionTopCat (X : TopCat) (S T : Set ↑X) (h : S ⊆ T) : ↧↑S ⟶ ↧↑T

The continuous inclusion between nested subspaces, bundled in TopCat.

Equations

• SphereOddDegree.setInclusionTopCat X S T h = TopCat.ofHom { toFun := Set.inclusion h, continuous_toFun := ⋯ }

theorem SphereOddDegree.setInclusionTopCat_comp_sInclusion (X : TopCat) (S T : Set ↑X) (h : S ⊆ T) : CategoryTheory.CategoryStruct.comp (setInclusionTopCat X S T h) (sInclusion T) = sInclusion S

theorem SphereOddDegree.subChainCorestrict_inclusion_square (X : TopCat) (S T : Set ↑X) (h : S ⊆ T) : CategoryTheory.CategoryStruct.comp (subChainCorestrict ℤ X S) (subChainInclusion S T h) = CategoryTheory.CategoryStruct.comp (singularChainℤ.map (setInclusionTopCat X S T h)) (subChainCorestrict ℤ X T)

theorem SphereOddDegree.subH0aug_natural_inclusion (X : TopCat) (S T : Set ↑X) (h : S ⊆ T) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (subChainInclusion S T h) 0) (subH0aug X T) = subH0aug X S