Relative chains and complementary simplices

This file uses the coproduct presentation of relative chains to give a criterion for a map of pairs to induce an isomorphism: the map must biject the simplices of the ambient simplicial sets that do not come from their respective subspaces, in every degree.

The criterion isolates the algebraic step in singular-homology excision. For the cover by the complement of the excised set and the interior of the subspace, the complementary small simplices are exactly the complementary simplices of the excised pair.

References

• A. Hatcher, Algebraic Topology, Section 2.1, proof of excision.
• S. Eilenberg and N. Steenrod, Foundations of Algebraic Topology, Chapter I, Section 9.

@[reducible, inline]

abbrev SSetPair.RelativeSimplex (P : SSetPair) (n : ℕ) : Set (P.right.obj (Opposite.op { len := n }))

The simplices of the ambient simplicial set of a pair that do not come from its subspace.

Equations

• P.RelativeSimplex n = (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (P.hom.app (Opposite.op { len := n }))))ᶜ

theorem SSetPair.isIso_chainComplexMap_of_relativeSimplex_equiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {P P' : SSetPair} (f : P ⟶ P') (R : C) (e : (n : ℕ) → ↑(P.RelativeSimplex n) ≃ ↑(P'.RelativeSimplex n)) (he : ∀ (n : ℕ) (x : ↑(P.RelativeSimplex n)), ↑((e n) x) = (CategoryTheory.ConcreteCategory.hom (f.right.app (Opposite.op { len := n }))) ↑x) : CategoryTheory.IsIso (chainComplexMap f R)

A map of simplicial-set pairs that bijects the ambient simplices outside the subspaces in every degree induces an isomorphism of relative chain complexes.

theorem SSetPair.isIso_homologyMap_of_relativeSimplex_equiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {P P' : SSetPair} (f : P ⟶ P') (R : C) (e : (n : ℕ) → ↑(P.RelativeSimplex n) ≃ ↑(P'.RelativeSimplex n)) (he : ∀ (n : ℕ) (x : ↑(P.RelativeSimplex n)), ↑((e n) x) = (CategoryTheory.ConcreteCategory.hom (f.right.app (Opposite.op { len := n }))) ↑x) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : CategoryTheory.IsIso (SSetPair.homologyMap f R n)

A map of simplicial-set pairs that bijects the ambient simplices outside the subspaces induces an isomorphism on relative homology.

@[reducible, inline]

abbrev SSet.Subcomplex.interPair {X : SSet} (A B : X.Subcomplex) : SSetPair

The pair consisting of A ∩ B as a subcomplex of A.

Equations

• A.interPair B = SSetPair.of (SSet.Subcomplex.homOfLE ⋯)

def SSet.Subcomplex.excisionMap {X : SSet} (A B : X.Subcomplex) : A.interPair B ⟶ B.pair

The canonical map (A, A ∩ B) ⟶ (X, B) of simplicial-set pairs.

Equations

• A.excisionMap B = SSetPair.homMk (SSet.Subcomplex.homOfLE ⋯) A.ι ⋯

@[simp]

theorem SSet.Subcomplex.excisionMap_left {X : SSet} (A B : X.Subcomplex) : (A.excisionMap B).left = homOfLE ⋯

@[simp]

theorem SSet.Subcomplex.excisionMap_right {X : SSet} (A B : X.Subcomplex) : (A.excisionMap B).right = A.ι

def SSet.Subcomplex.excisionRelativeSimplexEquiv {X : SSet} {A B : X.Subcomplex} (h : A ⊔ B = ⊤) (n : ℕ) : ↑((A.interPair B).RelativeSimplex n) ≃ ↑(B.pair.RelativeSimplex n)

If A and B cover a simplicial set, the simplices of A outside A ∩ B correspond exactly to the simplices of the ambient simplicial set outside B.

Equations

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

@[simp]

theorem SSet.Subcomplex.excisionRelativeSimplexEquiv_apply_val {X : SSet} {A B : X.Subcomplex} (h : A ⊔ B = ⊤) (n : ℕ) (x : ↑((A.interPair B).RelativeSimplex n)) : ↑((excisionRelativeSimplexEquiv h n) x) = ↑↑x

@[simp]

theorem SSet.Subcomplex.excisionRelativeSimplexEquiv_symm_apply_val {X : SSet} {A B : X.Subcomplex} (h : A ⊔ B = ⊤) (n : ℕ) (x : ↑(B.pair.RelativeSimplex n)) : ↑↑((excisionRelativeSimplexEquiv h n).symm x) = ↑x

theorem SSet.Subcomplex.isIso_chainComplexMap_excisionMap {X : SSet} {A B : X.Subcomplex} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (h : A ⊔ B = ⊤) : CategoryTheory.IsIso (SSetPair.chainComplexMap (A.excisionMap B) R)

Simplicial chain excision. If two subcomplexes cover a simplicial set, inclusion induces an isomorphism from the chains of (A, A ∩ B) to the chains of (X, B).

theorem SSet.Subcomplex.isIso_homologyMap_excisionMap {X : SSet} {A B : X.Subcomplex} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.CategoryWithHomology C] (h : A ⊔ B = ⊤) (n : ℕ) : CategoryTheory.IsIso (SSetPair.homologyMap (A.excisionMap B) R n)

Simplicial homology excision. If two subcomplexes cover a simplicial set, inclusion induces an isomorphism from Hₙ(A, A ∩ B) to Hₙ(X, B).