Subordinate singular chains for a single subset

For a topological space X and a subset S ⊆ X, this file defines, in each degree n, the R-submodule

C_n^S(X; R) ⊆ C_n(X; R)

of singular chains generated by the basis chains chainGenerator R X n σ of the singular simplices σ whose image lies entirely in S (IsSubordinate S σ). These submodules assemble into a chain complex subChainComplex R X S, and we provide the inclusion chain maps between subordinate complexes for S ⊆ T, and into the small-chain complex when S is a member of an open cover.

This is the algebraic backbone of singular Mayer–Vietoris: for an open cover {U, V} of X, the complexes subChainComplex R X ↑U, subChainComplex R X ↑V and subChainComplex R X (↑U ∩ ↑V) are the singular chains supported in U, V and U ∩ V respectively.

1. Subordinate simplices

def SphereOddDegree.IsSubordinate {X : TopCat} (S : Set ↑X) {n : ℕ} (σ : singularSimplices X n) : Prop

A singular n-simplex σ is subordinate to the subset S ⊆ X if its image is contained in S.

Equations

• SphereOddDegree.IsSubordinate S σ = (Set.range ⇑(SphereOddDegree.mvSimplexMap σ) ⊆ S)

theorem SphereOddDegree.IsSubordinate.mono {X : TopCat} {S T : Set ↑X} {n : ℕ} {σ : singularSimplices X n} (hσ : IsSubordinate S σ) (h : S ⊆ T) : IsSubordinate T σ

Subordination is monotone in the set.

theorem SphereOddDegree.IsSubordinate.comp_of_range_subset {X : TopCat} {S : Set ↑X} {m n : ℕ} {σ : singularSimplices X n} {τ : singularSimplices X m} (φ : C(↑(AffineBarycentricSubdivision.Delta m), ↑(AffineBarycentricSubdivision.Delta n))) (hcomp : mvSimplexMap τ = (mvSimplexMap σ).comp φ) (hσ : IsSubordinate S σ) : IsSubordinate S τ

Subordination is inherited along a factorization of the underlying maps.

theorem SphereOddDegree.IsSubordinate.face {X : TopCat} {S : Set ↑X} {n : ℕ} {σ : singularSimplices X (n + 1)} (hσ : IsSubordinate S σ) (i : Fin (n + 2)) : IsSubordinate S (AlexanderWhitney.faceSimplex X n i σ)

Face stability. Every boundary face of a subordinate simplex is subordinate (a face has image contained in the image of the original simplex).

theorem SphereOddDegree.IsSubordinate.isSmallSimplex {X : TopCat} {𝒰 : OpenCoverData X} {S : Set ↑X} (hS : S ∈ 𝒰.sets) {n : ℕ} {σ : singularSimplices X n} (hσ : IsSubordinate S σ) : IsSmallSimplex 𝒰 σ

If σ is subordinate to a member S of an open cover 𝒰, then σ is 𝒰-small.

2. The subordinate-chain submodule

noncomputable def SphereOddDegree.subChainSubmodule (R : Type) [CommRing R] (X : TopCat) (S : Set ↑X) (n : ℕ) : Submodule R ↑(AffineBarycentricSubdivision.singularChainGroup R X n)

The R-submodule C_n^S(X; R) ⊆ C_n(X; R) of singular chains generated by the basis chains chainGenerator R X n σ for simplices σ subordinate to S.

Equations

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

theorem SphereOddDegree.chainGenerator_mem_subChainSubmodule {R : Type} [CommRing R] {X : TopCat} {S : Set ↑X} {n : ℕ} {σ : singularSimplices X n} (hσ : IsSubordinate S σ) : AffineBarycentricSubdivision.chainGenerator R X n σ ∈ subChainSubmodule R X S n

Each subordinate generator lies in the subordinate-chain submodule.

theorem SphereOddDegree.subChainSubmodule_induction {R : Type} [CommRing R] {X : TopCat} {S : Set ↑X} {n : ℕ} {p : ↑(AffineBarycentricSubdivision.singularChainGroup R X n) → Prop} (mem : ∀ (σ : singularSimplices X n), IsSubordinate S σ → p (AffineBarycentricSubdivision.chainGenerator R X n σ)) (zero : p 0) (add : ∀ (x y : ↑(AffineBarycentricSubdivision.singularChainGroup R X n)), p x → p y → p (x + y)) (smul : ∀ (a : R) (x : ↑(AffineBarycentricSubdivision.singularChainGroup R X n)), p x → p (a • x)) {c : ↑(AffineBarycentricSubdivision.singularChainGroup R X n)} (hc : c ∈ subChainSubmodule R X S n) : p c

Induction principle for the subordinate-chain submodule.

theorem SphereOddDegree.subChainSubmodule_mono {R : Type} [CommRing R] {X : TopCat} {S T : Set ↑X} (h : S ⊆ T) (n : ℕ) : subChainSubmodule R X S n ≤ subChainSubmodule R X T n

The subordinate-chain submodules are monotone in the set.

theorem SphereOddDegree.subChainSubmodule_le_smallChainSubmodule {R : Type} [CommRing R] {X : TopCat} {𝒰 : OpenCoverData X} {S : Set ↑X} (hS : S ∈ 𝒰.sets) (n : ℕ) : subChainSubmodule R X S n ≤ smallChainSubmodule R X 𝒰 n

If S is a member of the open cover 𝒰, the subordinate chains for S are contained in the 𝒰-small chains.

3. Boundary stability

theorem SphereOddDegree.singularBoundary_maps_subChainSubmodule {R : Type} [CommRing R] {X : TopCat} {S : Set ↑X} (n : ℕ) (c : ↑(AffineBarycentricSubdivision.singularChainGroup R X (n + 1))) : c ∈ subChainSubmodule R X S (n + 1) → (ModuleCat.Hom.hom (AffineBarycentricSubdivision.singularBoundary R X n)) c ∈ subChainSubmodule R X S n

Boundary stability. The singular boundary maps the submodule of subordinate (n+1)-chains into the submodule of subordinate n-chains.

4. The subordinate-chain complex

noncomputable def SphereOddDegree.subBoundary (R : Type) [CommRing R] (X : TopCat) (S : Set ↑X) (n : ℕ) : ↧↥(subChainSubmodule R X S (n + 1)) ⟶ ↧↥(subChainSubmodule R X S n)

The restriction of the singular boundary to the subordinate-chain submodules.

Equations

• SphereOddDegree.subBoundary R X S n = ModuleCat.ofHom ((ModuleCat.Hom.hom (SphereOddDegree.AffineBarycentricSubdivision.singularBoundary R X n)).restrict ⋯)

@[simp]

theorem SphereOddDegree.subBoundary_hom_apply {R : Type} [CommRing R] {X : TopCat} {S : Set ↑X} (n : ℕ) (c : ↥(subChainSubmodule R X S (n + 1))) : ↑((ModuleCat.Hom.hom (subBoundary R X S n)) c) = (ModuleCat.Hom.hom (AffineBarycentricSubdivision.singularBoundary R X n)) ↑c

theorem SphereOddDegree.subBoundary_comp_subBoundary {R : Type} [CommRing R] {X : TopCat} {S : Set ↑X} (n : ℕ) : CategoryTheory.CategoryStruct.comp (subBoundary R X S (n + 1)) (subBoundary R X S n) = 0

noncomputable def SphereOddDegree.subChainComplex (R : Type) [CommRing R] (X : TopCat) (S : Set ↑X) : ChainComplex (ModuleCat R) ℕ

The subordinate-chain complex C_*^S(X; R).

Equations

• SphereOddDegree.subChainComplex R X S = ChainComplex.of (fun (n : ℕ) => ↧↥(SphereOddDegree.subChainSubmodule R X S n)) (fun (n : ℕ) => SphereOddDegree.subBoundary R X S n) ⋯

@[simp]

theorem SphereOddDegree.subChainComplex_X {R : Type} [CommRing R] {X : TopCat} {S : Set ↑X} (n : ℕ) : (subChainComplex R X S).X n = ↧↥(subChainSubmodule R X S n)

@[simp]

theorem SphereOddDegree.subChainComplex_d {R : Type} [CommRing R] {X : TopCat} {S : Set ↑X} (n : ℕ) : (subChainComplex R X S).d (n + 1) n = subBoundary R X S n

5. Inclusion chain maps

noncomputable def SphereOddDegree.subChainInclusion {R : Type} [CommRing R] {X : TopCat} (S T : Set ↑X) (h : S ⊆ T) : subChainComplex R X S ⟶ subChainComplex R X T

The inclusion chain map C_*^S(X; R) ⟶ C_*^T(X; R) for S ⊆ T.

Equations

• SphereOddDegree.subChainInclusion S T h = { f := fun (n : ℕ) => ModuleCat.ofHom (Submodule.inclusion ⋯), comm' := ⋯ }

theorem SphereOddDegree.subChainInclusion_f_apply {R : Type} [CommRing R] {X : TopCat} {S T : Set ↑X} (h : S ⊆ T) (n : ℕ) (c : ↥(subChainSubmodule R X S n)) : ↑((ModuleCat.Hom.hom ((subChainInclusion S T h).f n)) c) = ↑c

noncomputable def SphereOddDegree.subChainToSmall {R : Type} [CommRing R] {X : TopCat} (𝒰 : OpenCoverData X) (S : Set ↑X) (hS : S ∈ 𝒰.sets) : subChainComplex R X S ⟶ smallChainComplex R X 𝒰

The inclusion chain map C_*^S(X; R) ⟶ C_*^𝒰(X; R) of the subordinate chains for a cover member S into the small-chain complex.

Equations

• SphereOddDegree.subChainToSmall 𝒰 S hS = { f := fun (n : ℕ) => ModuleCat.ofHom (Submodule.inclusion ⋯), comm' := ⋯ }

theorem SphereOddDegree.subChainToSmall_f_apply {R : Type} [CommRing R] {X : TopCat} {𝒰 : OpenCoverData X} {S : Set ↑X} (hS : S ∈ 𝒰.sets) (n : ℕ) (c : ↥(subChainSubmodule R X S n)) : ↑((ModuleCat.Hom.hom ((subChainToSmall 𝒰 S hS).f n)) c) = ↑c