Sub Chain Subspace Bridge

def SphereOddDegree.sInclusion {X : TopCat} (S : Set ↑X) : ↧↑S ⟶ X

The continuous inclusion of a subspace into the ambient space.

Equations

• SphereOddDegree.sInclusion S = TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ }

@[simp]

theorem SphereOddDegree.sInclusion_hom_apply {X : TopCat} (S : Set ↑X) (x : ↑S) : (CategoryTheory.ConcreteCategory.hom (sInclusion S)) x = ↑x

theorem SphereOddDegree.isSubordinate_pushSimplex_sInclusion {X : TopCat} (S : Set ↑X) (n : ℕ) (τ : singularSimplices (↧↑S) n) : IsSubordinate S (AffineBarycentricSubdivision.pushSimplex (sInclusion S) n τ)

theorem SphereOddDegree.pushSimplex_sInclusion_injective {X : TopCat} (S : Set ↑X) (n : ℕ) : Function.Injective (AffineBarycentricSubdivision.pushSimplex (sInclusion S) n)

theorem SphereOddDegree.exists_pushSimplex_of_subordinate {X : TopCat} (S : Set ↑X) (n : ℕ) {σ : singularSimplices X n} (hσ : IsSubordinate S σ) : ∃ (τ : singularSimplices (↧↑S) n), AffineBarycentricSubdivision.pushSimplex (sInclusion S) n τ = σ

theorem SphereOddDegree.singularChainMap_sInclusion_mem {R : Type} [CommRing R] {X : TopCat} (S : Set ↑X) (n : ℕ) (c : ↑(AffineBarycentricSubdivision.singularChainGroup R (↧↑S) n)) : (ModuleCat.Hom.hom (AffineBarycentricSubdivision.singularChainMap R (sInclusion S) n)) c ∈ subChainSubmodule R X S n

noncomputable def SphereOddDegree.subChainCorestrict (R : Type) [CommRing R] (X : TopCat) (S : Set ↑X) : ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj ↧R).obj ↧↑S ⟶ subChainComplex R X S

Corestrict the subspace singular-chain map to the subcomplex of supported chains.

Equations

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

noncomputable def SphereOddDegree.reindexChainMap (R : Type) [CommRing R] {X Y : TopCat} (n : ℕ) (g : singularSimplices Y n → singularSimplices X n) : AffineBarycentricSubdivision.singularChainGroup R Y n ⟶ AffineBarycentricSubdivision.singularChainGroup R X n

The linear chain map obtained by reindexing singular-simplex generators in one degree.

Equations

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

@[simp]

theorem SphereOddDegree.reindexChainMap_generator {R : Type} [CommRing R] {X Y : TopCat} (n : ℕ) (g : singularSimplices Y n → singularSimplices X n) (σ : singularSimplices Y n) : (ModuleCat.Hom.hom (reindexChainMap R n g)) (AffineBarycentricSubdivision.chainGenerator R Y n σ) = AffineBarycentricSubdivision.chainGenerator R X n (g σ)

theorem SphereOddDegree.reindexChainMap_comp_singularChainMap {R : Type} [CommRing R] {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) (g : singularSimplices Y n → singularSimplices X n) (hg : Function.LeftInverse g (AffineBarycentricSubdivision.pushSimplex f n)) : CategoryTheory.CategoryStruct.comp (AffineBarycentricSubdivision.singularChainMap R f n) (reindexChainMap R n g) = CategoryTheory.CategoryStruct.id (AffineBarycentricSubdivision.singularChainGroup R X n)

theorem SphereOddDegree.singularChainMap_injective_of_pushSimplex_injective {R : Type} [CommRing R] {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) (hf : Function.Injective (AffineBarycentricSubdivision.pushSimplex f n)) : Function.Injective ⇑(ModuleCat.Hom.hom (AffineBarycentricSubdivision.singularChainMap R f n))

theorem SphereOddDegree.subChainCorestrict_bijective {R : Type} [CommRing R] {X : TopCat} (S : Set ↑X) (n : ℕ) : Function.Bijective ⇑(ModuleCat.Hom.hom ((subChainCorestrict R X S).f n))

instance SphereOddDegree.subChainCorestrict_component_isIso {R : Type} [CommRing R] {X : TopCat} (S : Set ↑X) (n : ℕ) : CategoryTheory.IsIso ((subChainCorestrict R X S).f n)

instance SphereOddDegree.subChainCorestrict_isIso {R : Type} [CommRing R] {X : TopCat} (S : Set ↑X) : CategoryTheory.IsIso (subChainCorestrict R X S)

noncomputable def SphereOddDegree.subspaceHomologyIso {R : Type} [CommRing R] {X : TopCat} (S : Set ↑X) (n : ℕ) : HomologicalComplex.homology (subChainComplex R X S) n ≅ HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj ↧R).obj ↧↑S) n

Identify homology of supported chains with singular homology of the subspace.

Equations

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

noncomputable def SphereOddDegree.subspaceHomologyIsoℤ (X : TopCat) (S : Set ↑X) (n : ℕ) : HomologicalComplex.homology (subChainComplex ℤ X S) n ≅ (singularHomologyℤ n).obj ↧↑S

The subspace homology identification with integer coefficients.

Equations

• SphereOddDegree.subspaceHomologyIsoℤ X S n = SphereOddDegree.subspaceHomologyIso S n

theorem SphereOddDegree.isZero_subChainComplex_homology_of_contractible (X : TopCat) (S : Set ↑X) [ContractibleSpace ↑S] (n : ℕ) (hn : 1 ≤ n) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (subChainComplex ℤ X S) n)