Relative Mayer–Vietoris sequences

Let U and V be open subsets of a topological space X, and let R be an object of an abelian category with coproducts. This file constructs the relative Mayer–Vietoris long exact sequence of relative singular homology with coefficients in R, ⋯ ⟶ Hₙ(X, U ∩ V) ⟶ Hₙ(X, U) ⊞ Hₙ(X, V) ⟶ Hₙ(X, U ∪ V) ⟶ Hₙ₋₁(X, U ∩ V) ⟶ ⋯, whose first map is (i_U, -i_V) and whose second map is j_U + j_V, the i and j being the maps induced by the inclusions of pairs with the identity of X. Unlike the absolute sequence, U and V need not cover X.

For the complements U = X ∖ A and V = X ∖ B of closed sets this is the sequence ⋯ ⟶ Hₙ(X, X ∖ (A ∪ B)) ⟶ Hₙ(X, X ∖ A) ⊞ Hₙ(X, X ∖ B) ⟶ Hₙ(X, X ∖ (A ∩ B)) ⟶ ⋯ through which the homology of a manifold relative to the complement of a compact set is computed by induction on the number of convex pieces in charts, which is the route to fundamental classes and to Poincaré duality.

The construction applies the relative Mayer–Vietoris sequence of a square of pairs of simplicial sets (SSetPair.shortExact_mayerVietoris) to the pairs formed by the singular simplicial set of X and the singular simplicial sets of U ∩ V, U and V, together with the subcomplex of singular simplices of X lying in U or in V. The ambient square consists of identities and the square of subobjects is the pushout square of the absolute Mayer–Vietoris sequence (TopCat.isPushout_toSSet_inter_smallSingularSubcomplex). Since U and V are open, the small-chain theorem for the cover of U ∪ V by U and V identifies the relative homology of X modulo that subcomplex with Hₙ(X, U ∪ V).

The second sequence is the Mayer–Vietoris sequence of two pairs. For subsets C ⊆ A and D ⊆ B of X, with A and B open in A ∪ B and C and D open in C ∪ D, it is ⋯ ⟶ Hₙ(A ∩ B, C ∩ D) ⟶ Hₙ(A, C) ⊞ Hₙ(B, D) ⟶ Hₙ(A ∪ B, C ∪ D) ⟶ Hₙ₋₁(A ∩ B, C ∩ D) ⟶ ⋯, again with first map (i_A, -i_B) and second map j_A + j_B, now induced by the inclusions of the subspaces. For the restrictions (E|U, E₀|U) and (E|V, E₀|V) of a pair over two open sets of a base, such as the Thom pair of a vector bundle over a union of two trivializing open sets, this is the sequence that assembles the relative homology of the pair over U ∪ V from its pieces. Here the ambient square of singular simplicial sets is the pushout square of A ∩ B, A, B and the singular simplices of X lying in A or in B, the square of subobjects is the corresponding square for C and D, and the small-chain theorem for both covers identifies the corner pair with (A ∪ B, C ∪ D).

Main definitions and results

• TopCat.relativeMayerVietorisToBiprod, TopCat.relativeMayerVietorisFromBiprod: the maps Hₙ(X, U ∩ V) ⟶ Hₙ(X, U) ⊞ Hₙ(X, V) and Hₙ(X, U) ⊞ Hₙ(X, V) ⟶ Hₙ(X, U ∪ V).
• TopCat.relativeMayerVietorisδ: the connecting morphism Hₙ(X, U ∪ V) ⟶ Hₘ(X, U ∩ V), m + 1 = n.
• TopCat.relativeMayerVietoris_exact₁, TopCat.relativeMayerVietoris_exact₂, TopCat.relativeMayerVietoris_exact₃: exactness at Hₘ(X, U ∩ V), at Hₙ(X, U) ⊞ Hₙ(X, V) and at Hₙ(X, U ∪ V).
• TopCat.epi_relativeMayerVietorisFromBiprod_zero: surjectivity at the degree-zero endpoint.
• TopCat.mono_relativeMayerVietorisToBiprod: injectivity of the first map when Hₖ₊₁(X, U ∪ V) vanishes.
• TopCat.relativeMayerVietorisToBiprod_naturality, TopCat.relativeMayerVietorisFromBiprod_naturality, TopCat.relativeMayerVietorisδ_naturality: the maps of the sequence are natural in maps f : X ⟶ Y carrying U into U' and V into V'.
• TopCat.pairMayerVietorisToBiprod, TopCat.pairMayerVietorisFromBiprod: the maps Hₙ(A ∩ B, C ∩ D) ⟶ Hₙ(A, C) ⊞ Hₙ(B, D) and Hₙ(A, C) ⊞ Hₙ(B, D) ⟶ Hₙ(A ∪ B, C ∪ D).
• TopCat.pairMayerVietorisδ: the connecting morphism Hₙ(A ∪ B, C ∪ D) ⟶ Hₘ(A ∩ B, C ∩ D), m + 1 = n.
• TopCat.pairMayerVietoris_exact₁, TopCat.pairMayerVietoris_exact₂, TopCat.pairMayerVietoris_exact₃: exactness at Hₘ(A ∩ B, C ∩ D), at Hₙ(A, C) ⊞ Hₙ(B, D) and at Hₙ(A ∪ B, C ∪ D).
• TopCat.smallSingularSubcomplexPairToUnion: the comparison of X relative to its singular simplices lying in U or in V with (X, U ∪ V), compatible with the quotient maps (TopCat.chainComplexπ_smallSingularSubcomplexPairToUnion) and natural along the maps TopCat.smallSingularSubcomplexPairMap (TopCat.smallSingularSubcomplexPairToUnion_comp_ofSubsetMap).
• TopCat.smallSingularPair, TopCat.toSmallSingularPair and TopCat.smallSingularPairToUnion: the square of singular pairs underlying the sequence of two pairs and its comparison with (A ∪ B, C ∪ D), through TopCat.smallSingularSubcomplexToUnion; they are shared with the sequence in cohomology.
• TopCat.smallSingularPairMap: the map of these squares induced by a map f : X ⟶ Y carrying A, B, C and D into A', B', C' and D', functorial in f (TopCat.smallSingularPairMap_id, TopCat.smallSingularPairMap_comp), and compatible with TopCat.toSmallSingularPair (TopCat.toSmallSingularPair_comp_smallSingularPairMap) and with the comparison maps (TopCat.smallSingularPairToUnion_comp_ofInclusionMap).
• TopCat.epi_pairMayerVietorisFromBiprod_zero and TopCat.mono_pairMayerVietorisToBiprod: surjectivity at the degree-zero endpoint, and injectivity of the first map when Hₖ₊₁(A ∪ B, C ∪ D) vanishes.
• TopCat.isZero_singularHomology_ofInclusion_union: Hₙ(A ∪ B, C ∪ D) vanishes when Hₙ(A, C), Hₙ(B, D) and Hₙ₋₁(A ∩ B, C ∩ D) do.

References

• A. Hatcher, Algebraic Topology, Section 2.2, the relative Mayer–Vietoris sequence, both for (X, U ∩ V), (X, U), (X, V) and for pairs (A ∪ B, C ∪ D) with C ⊆ A and D ⊆ B, and Lemma 3.27 for its use on complements of compact sets in a manifold.
• J. W. Milnor, J. D. Stasheff, Characteristic Classes, Annals of Mathematics Studies 76, Princeton (1974), §10, where the cohomological sequence of two pairs over open sets of a base is used to construct the Thom class.

The maps of the sequence

noncomputable def TopCat.relativeMayerVietorisToBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} (U V : Set ↑X) (n : ℕ) : (TopPair.ofSubset (U ∩ V)).singularHomology R n ⟶ (TopPair.ofSubset U).singularHomology R n ⊞ (TopPair.ofSubset V).singularHomology R n

The first map Hₙ(X, U ∩ V) ⟶ Hₙ(X, U) ⊞ Hₙ(X, V) of the relative Mayer–Vietoris sequence, with components i_U and -i_V induced by the identity of X.

@[simp]

theorem TopCat.relativeMayerVietorisToBiprod_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} (U V : Set ↑X) (n : ℕ) : CategoryTheory.CategoryStruct.comp (relativeMayerVietorisToBiprod R U V n) CategoryTheory.Limits.biprod.fst = TopPair.singularHomologyMap (TopPair.ofSubsetMap (CategoryTheory.CategoryStruct.id X) ⋯) R n

@[simp]

theorem TopCat.relativeMayerVietorisToBiprod_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} (U V : Set ↑X) (n : ℕ) {Z : C} (h : (TopPair.ofSubset U).singularHomology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (relativeMayerVietorisToBiprod R U V n) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) = CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (TopPair.ofSubsetMap (CategoryTheory.CategoryStruct.id X) ⋯) R n) h

@[simp]

theorem TopCat.relativeMayerVietorisToBiprod_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} (U V : Set ↑X) (n : ℕ) : CategoryTheory.CategoryStruct.comp (relativeMayerVietorisToBiprod R U V n) CategoryTheory.Limits.biprod.snd = -TopPair.singularHomologyMap (TopPair.ofSubsetMap (CategoryTheory.CategoryStruct.id X) ⋯) R n

@[simp]

theorem TopCat.relativeMayerVietorisToBiprod_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} (U V : Set ↑X) (n : ℕ) {Z : C} (h : (TopPair.ofSubset V).singularHomology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (relativeMayerVietorisToBiprod R U V n) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = CategoryTheory.CategoryStruct.comp (-TopPair.singularHomologyMap (TopPair.ofSubsetMap (CategoryTheory.CategoryStruct.id X) ⋯) R n) h

noncomputable def TopCat.relativeMayerVietorisFromBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} (U V : Set ↑X) (n : ℕ) : (TopPair.ofSubset U).singularHomology R n ⊞ (TopPair.ofSubset V).singularHomology R n ⟶ (TopPair.ofSubset (U ∪ V)).singularHomology R n

The second map Hₙ(X, U) ⊞ Hₙ(X, V) ⟶ Hₙ(X, U ∪ V) of the relative Mayer–Vietoris sequence, the sum of the maps j_U and j_V induced by the identity of X.

@[simp]

theorem TopCat.inl_relativeMayerVietorisFromBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} (U V : Set ↑X) (n : ℕ) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (relativeMayerVietorisFromBiprod R U V n) = TopPair.singularHomologyMap (TopPair.ofSubsetMap (CategoryTheory.CategoryStruct.id X) ⋯) R n

@[simp]

theorem TopCat.inl_relativeMayerVietorisFromBiprod_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} (U V : Set ↑X) (n : ℕ) {Z : C} (h : (TopPair.ofSubset (U ∪ V)).singularHomology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp (relativeMayerVietorisFromBiprod R U V n) h) = CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (TopPair.ofSubsetMap (CategoryTheory.CategoryStruct.id X) ⋯) R n) h

@[simp]

theorem TopCat.inr_relativeMayerVietorisFromBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} (U V : Set ↑X) (n : ℕ) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (relativeMayerVietorisFromBiprod R U V n) = TopPair.singularHomologyMap (TopPair.ofSubsetMap (CategoryTheory.CategoryStruct.id X) ⋯) R n

@[simp]

theorem TopCat.inr_relativeMayerVietorisFromBiprod_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} (U V : Set ↑X) (n : ℕ) {Z : C} (h : (TopPair.ofSubset (U ∪ V)).singularHomology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (relativeMayerVietorisFromBiprod R U V n) h) = CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (TopPair.ofSubsetMap (CategoryTheory.CategoryStruct.id X) ⋯) R n) h

The square of singular pairs

Comparison with the pair (X, U ∪ V)

noncomputable def TopCat.smallSingularSubcomplexToUnion {X : TopCat} (U V : Set ↑X) : (X.smallSingularSubcomplex ![U, V]).toSSet ⟶ toSSet.obj ↧↑(U ∪ V)

The singular simplices of X lying in U or in V are singular simplices of U ∪ V.

theorem TopCat.smallSingularSubcomplexToUnion_comp {X : TopCat} (U V : Set ↑X) : CategoryTheory.CategoryStruct.comp (smallSingularSubcomplexToUnion U V) (toSSet.map (ofHom (ContinuousMap.subtypeVal (U ∪ V)))) = (X.smallSingularSubcomplex ![U, V]).ι

Followed by the inclusion of U ∪ V into X, the map TopCat.smallSingularSubcomplexToUnion is the inclusion of the singular simplices of X lying in U or in V.

theorem TopCat.smallSingularSubcomplexToUnion_comp_assoc {X : TopCat} (U V : Set ↑X) {Z : SSet} (h : toSSet.obj ↧↑X ⟶ Z) : CategoryTheory.CategoryStruct.comp (smallSingularSubcomplexToUnion U V) (CategoryTheory.CategoryStruct.comp (toSSet.map (ofHom (ContinuousMap.subtypeVal (U ∪ V)))) h) = CategoryTheory.CategoryStruct.comp (X.smallSingularSubcomplex ![U, V]).ι h

Followed by the inclusion of U ∪ V into X, the map TopCat.smallSingularSubcomplexToUnion is the inclusion of the singular simplices of X lying in U or in V.

theorem TopCat.smallSingularSubcomplexToUnion_comp_restrict {X : TopCat} (U V : Set ↑X) {Y : TopCat} (f : X ⟶ Y) {U' V' : Set ↑Y} (hfU : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) U U') (hfV : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) V V') : CategoryTheory.CategoryStruct.comp (smallSingularSubcomplexToUnion U V) (toSSet.map (ofHom { toFun := Set.MapsTo.restrict (⇑(CategoryTheory.ConcreteCategory.hom f)) (U ∪ V) (U' ∪ V') ⋯, continuous_toFun := ⋯ })) = CategoryTheory.CategoryStruct.comp (smallSingularSubcomplexMap ![U, V] ![U', V'] f id ⋯) (smallSingularSubcomplexToUnion U' V')

The comparison maps TopCat.smallSingularSubcomplexToUnion are natural in maps carrying U into U' and V into V'.

theorem TopCat.smallSingularSubcomplexToUnion_comp_restrict_assoc {X : TopCat} (U V : Set ↑X) {Y : TopCat} (f : X ⟶ Y) {U' V' : Set ↑Y} (hfU : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) U U') (hfV : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) V V') {Z : SSet} (h : toSSet.obj ↧↑(U' ∪ V') ⟶ Z) : CategoryTheory.CategoryStruct.comp (smallSingularSubcomplexToUnion U V) (CategoryTheory.CategoryStruct.comp (toSSet.map (ofHom { toFun := Set.MapsTo.restrict (⇑(CategoryTheory.ConcreteCategory.hom f)) (U ∪ V) (U' ∪ V') ⋯, continuous_toFun := ⋯ })) h) = CategoryTheory.CategoryStruct.comp (smallSingularSubcomplexMap ![U, V] ![U', V'] f id ⋯) (CategoryTheory.CategoryStruct.comp (smallSingularSubcomplexToUnion U' V') h)

The comparison maps TopCat.smallSingularSubcomplexToUnion are natural in maps carrying U into U' and V into V'.

theorem TopCat.exists_iso_comp_smallSingularSubcomplexToUnion {X : TopCat} (U V : Set ↑X) : ∃ (e : ((↧↑(U ∪ V)).smallSingularSubcomplex fun (i : Fin (Nat.succ 0).succ) => ⇑(CategoryTheory.ConcreteCategory.hom (ofHom (ContinuousMap.subtypeVal (U ∪ V)))) ⁻¹' ![U, V] i).toSSet ≅ (X.smallSingularSubcomplex ![U, V]).toSSet), CategoryTheory.CategoryStruct.comp e.hom (smallSingularSubcomplexToUnion U V) = ((↧↑(U ∪ V)).smallSingularSubcomplex fun (i : Fin (Nat.succ 0).succ) => ⇑(CategoryTheory.ConcreteCategory.hom (ofHom (ContinuousMap.subtypeVal (U ∪ V)))) ⁻¹' ![U, V] i).ι

Up to an isomorphism of simplicial sets, TopCat.smallSingularSubcomplexToUnion U V is the inclusion of the singular simplices of U ∪ V lying in the trace of U or in the trace of V: the singular simplices of X lying in U or in V are exactly the images of those.

noncomputable def TopCat.smallSingularSubcomplexPairToUnion {X : TopCat} (U V : Set ↑X) : (X.smallSingularSubcomplex ![U, V]).pair ⟶ TopPair.toSSetPair.obj (TopPair.ofSubset (U ∪ V))

The map of singular pairs from X relative to its singular simplices lying in U or in V to (X, U ∪ V), given by TopCat.smallSingularSubcomplexToUnion on subobjects and the identity on the singular simplicial set of X.

@[simp]

theorem TopCat.smallSingularSubcomplexPairToUnion_left {X : TopCat} (U V : Set ↑X) : (smallSingularSubcomplexPairToUnion U V).left = smallSingularSubcomplexToUnion U V

@[simp]

theorem TopCat.smallSingularSubcomplexPairToUnion_right {X : TopCat} (U V : Set ↑X) : (smallSingularSubcomplexPairToUnion U V).right = CategoryTheory.CategoryStruct.id (toSSet.obj X)

theorem TopCat.chainComplexMap_smallSingularSubcomplexPairToUnion_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} (U V : Set ↑X) : SSet.chainComplexMap (smallSingularSubcomplexPairToUnion U V).right R = CategoryTheory.CategoryStruct.id ((X.smallSingularSubcomplex ![U, V]).pair.right.chainComplex R)

The chain map induced by the ambient component of TopCat.smallSingularSubcomplexPairToUnion is the identity. Not @[simp]: TopCat.smallSingularSubcomplexPairToUnion_right already rewrites its left-hand side.

theorem TopCat.chainComplexπ_smallSingularSubcomplexPairToUnion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} (U V : Set ↑X) : CategoryTheory.CategoryStruct.comp ((X.smallSingularSubcomplex ![U, V]).pair.chainComplexπ R) (SSetPair.chainComplexMap (smallSingularSubcomplexPairToUnion U V) R) = (TopPair.ofSubset (U ∪ V)).singularChainComplexπ R

The quotient map from the singular chains of X to its chains relative to the singular simplices lying in U or in V, followed by TopCat.smallSingularSubcomplexPairToUnion, is the quotient map to the relative chains of (X, U ∪ V).

theorem TopCat.chainComplexπ_smallSingularSubcomplexPairToUnion_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} (U V : Set ↑X) {Z : ChainComplex C ℕ} (h : (TopPair.toSSetPair.obj (TopPair.ofSubset (U ∪ V))).chainComplex R ⟶ Z) : CategoryTheory.CategoryStruct.comp ((X.smallSingularSubcomplex ![U, V]).pair.chainComplexπ R) (CategoryTheory.CategoryStruct.comp (SSetPair.chainComplexMap (smallSingularSubcomplexPairToUnion U V) R) h) = CategoryTheory.CategoryStruct.comp ((TopPair.ofSubset (U ∪ V)).singularChainComplexπ R) h

The quotient map from the singular chains of X to its chains relative to the singular simplices lying in U or in V, followed by TopCat.smallSingularSubcomplexPairToUnion, is the quotient map to the relative chains of (X, U ∪ V).

theorem TopCat.quasiIso_chainComplexMap_smallSingularSubcomplexToUnion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} (U V : Set ↑X) (hU : IsOpen (Subtype.val ⁻¹' U)) (hV : IsOpen (Subtype.val ⁻¹' V)) : QuasiIso (SSet.chainComplexMap (smallSingularSubcomplexToUnion U V) R)

The singular simplices of X lying in U or in V compute the homology of U ∪ V, by the small-chain theorem for the cover of U ∪ V by U and V, which only needs to be open in U ∪ V.

The long exact sequence

@[simp]

theorem TopCat.relativeMayerVietorisToBiprod_fromBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} (U V : Set ↑X) (n : ℕ) : CategoryTheory.CategoryStruct.comp (relativeMayerVietorisToBiprod R U V n) (relativeMayerVietorisFromBiprod R U V n) = 0

The first two maps of the relative Mayer–Vietoris sequence compose to zero.

@[simp]

theorem TopCat.relativeMayerVietorisToBiprod_fromBiprod_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} (U V : Set ↑X) (n : ℕ) {Z : C} (h : (TopPair.ofSubset (U ∪ V)).singularHomology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (relativeMayerVietorisToBiprod R U V n) (CategoryTheory.CategoryStruct.comp (relativeMayerVietorisFromBiprod R U V n) h) = CategoryTheory.CategoryStruct.comp 0 h

The first two maps of the relative Mayer–Vietoris sequence compose to zero.

noncomputable def TopCat.relativeMayerVietorisδ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (n m : ℕ) (h : m + 1 = n := by lia) : (TopPair.ofSubset (U ∪ V)).singularHomology R n ⟶ (TopPair.ofSubset (U ∩ V)).singularHomology R m

The relative Mayer–Vietoris connecting morphism Hₙ(X, U ∪ V) ⟶ Hₘ(X, U ∩ V), where m + 1 = n, for open sets U and V. It is the connecting morphism of the relative Mayer–Vietoris sequence of the singular pairs of X modulo U ∩ V, U, V and the singular simplices lying in U or in V, precomposed with the inverse of the small-chain isomorphism identifying the last of these with Hₙ(X, U ∪ V).

@[simp]

theorem TopCat.relativeMayerVietorisδ_toBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (relativeMayerVietorisδ R hU hV n m h) (relativeMayerVietorisToBiprod R U V m) = 0

@[simp]

theorem TopCat.relativeMayerVietorisδ_toBiprod_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (n m : ℕ) (h : m + 1 = n := by lia) {Z : C} (h✝ : (TopPair.ofSubset U).singularHomology R m ⊞ (TopPair.ofSubset V).singularHomology R m ⟶ Z) : CategoryTheory.CategoryStruct.comp (relativeMayerVietorisδ R hU hV n m h) (CategoryTheory.CategoryStruct.comp (relativeMayerVietorisToBiprod R U V m) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

@[simp]

theorem TopCat.relativeMayerVietorisFromBiprod_δ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (relativeMayerVietorisFromBiprod R U V n) (relativeMayerVietorisδ R hU hV n m h) = 0

@[simp]

theorem TopCat.relativeMayerVietorisFromBiprod_δ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (n m : ℕ) (h : m + 1 = n := by lia) {Z : C} (h✝ : (TopPair.ofSubset (U ∩ V)).singularHomology R m ⟶ Z) : CategoryTheory.CategoryStruct.comp (relativeMayerVietorisFromBiprod R U V n) (CategoryTheory.CategoryStruct.comp (relativeMayerVietorisδ R hU hV n m h) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

theorem TopCat.relativeMayerVietoris_exact₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (n m : ℕ) (h : m + 1 = n := by lia) : { X₁ := (TopPair.ofSubset (U ∪ V)).singularHomology R n, X₂ := (TopPair.ofSubset (U ∩ V)).singularHomology R m, X₃ := (TopPair.ofSubset U).singularHomology R m ⊞ (TopPair.ofSubset V).singularHomology R m, f := relativeMayerVietorisδ R hU hV n m h, g := relativeMayerVietorisToBiprod R U V m, zero := ⋯ }.Exact

Exactness of the relative Mayer–Vietoris sequence at Hₘ(X, U ∩ V).

theorem TopCat.mono_relativeMayerVietorisToBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) {k : ℕ} (h : CategoryTheory.Limits.IsZero ((TopPair.ofSubset (U ∪ V)).singularHomology R (k + 1))) : CategoryTheory.Mono (relativeMayerVietorisToBiprod R U V k)

If Hₖ₊₁(X, U ∪ V) vanishes, the first map Hₖ(X, U ∩ V) ⟶ Hₖ(X, U) ⊞ Hₖ(X, V) of the relative Mayer–Vietoris sequence is a monomorphism.

theorem TopCat.relativeMayerVietoris_exact₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (n : ℕ) : { X₁ := (TopPair.ofSubset (U ∩ V)).singularHomology R n, X₂ := (TopPair.ofSubset U).singularHomology R n ⊞ (TopPair.ofSubset V).singularHomology R n, X₃ := (TopPair.ofSubset (U ∪ V)).singularHomology R n, f := relativeMayerVietorisToBiprod R U V n, g := relativeMayerVietorisFromBiprod R U V n, zero := ⋯ }.Exact

Exactness of the relative Mayer–Vietoris sequence at Hₙ(X, U) ⊞ Hₙ(X, V).

theorem TopCat.relativeMayerVietoris_exact₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (n m : ℕ) (h : m + 1 = n := by lia) : { X₁ := (TopPair.ofSubset U).singularHomology R n ⊞ (TopPair.ofSubset V).singularHomology R n, X₂ := (TopPair.ofSubset (U ∪ V)).singularHomology R n, X₃ := (TopPair.ofSubset (U ∩ V)).singularHomology R m, f := relativeMayerVietorisFromBiprod R U V n, g := relativeMayerVietorisδ R hU hV n m h, zero := ⋯ }.Exact

Exactness of the relative Mayer–Vietoris sequence at Hₙ(X, U ∪ V).

theorem TopCat.epi_relativeMayerVietorisFromBiprod_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) : CategoryTheory.Epi (relativeMayerVietorisFromBiprod R U V 0)

The map H₀(X, U) ⊞ H₀(X, V) ⟶ H₀(X, U ∪ V) at the end of the relative Mayer–Vietoris sequence is an epimorphism.

Naturality

theorem TopCat.relativeMayerVietorisToBiprod_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {U V : Set ↑X} {Y : TopCat} {U' V' : Set ↑Y} (f : X ⟶ Y) (hfU : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) U U') (hfV : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) V V') (n : ℕ) : CategoryTheory.CategoryStruct.comp (relativeMayerVietorisToBiprod R U V n) (CategoryTheory.Limits.biprod.map (TopPair.singularHomologyMap (TopPair.ofSubsetMap f hfU) R n) (TopPair.singularHomologyMap (TopPair.ofSubsetMap f hfV) R n)) = CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (TopPair.ofSubsetMap f ⋯) R n) (relativeMayerVietorisToBiprod R U' V' n)

The first map of the relative Mayer–Vietoris sequence is natural in maps f : X ⟶ Y carrying U into U' and V into V'.

theorem TopCat.relativeMayerVietorisToBiprod_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {U V : Set ↑X} {Y : TopCat} {U' V' : Set ↑Y} (f : X ⟶ Y) (hfU : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) U U') (hfV : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) V V') (n : ℕ) {Z : C} (h : (TopPair.ofSubset U').singularHomology R n ⊞ (TopPair.ofSubset V').singularHomology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (relativeMayerVietorisToBiprod R U V n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (TopPair.singularHomologyMap (TopPair.ofSubsetMap f hfU) R n) (TopPair.singularHomologyMap (TopPair.ofSubsetMap f hfV) R n)) h) = CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (TopPair.ofSubsetMap f ⋯) R n) (CategoryTheory.CategoryStruct.comp (relativeMayerVietorisToBiprod R U' V' n) h)

The first map of the relative Mayer–Vietoris sequence is natural in maps f : X ⟶ Y carrying U into U' and V into V'.

theorem TopCat.relativeMayerVietorisFromBiprod_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {U V : Set ↑X} {Y : TopCat} {U' V' : Set ↑Y} (f : X ⟶ Y) (hfU : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) U U') (hfV : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) V V') (n : ℕ) : CategoryTheory.CategoryStruct.comp (relativeMayerVietorisFromBiprod R U V n) (TopPair.singularHomologyMap (TopPair.ofSubsetMap f ⋯) R n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (TopPair.singularHomologyMap (TopPair.ofSubsetMap f hfU) R n) (TopPair.singularHomologyMap (TopPair.ofSubsetMap f hfV) R n)) (relativeMayerVietorisFromBiprod R U' V' n)

The second map of the relative Mayer–Vietoris sequence is natural in maps f : X ⟶ Y carrying U into U' and V into V'.

theorem TopCat.relativeMayerVietorisFromBiprod_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {U V : Set ↑X} {Y : TopCat} {U' V' : Set ↑Y} (f : X ⟶ Y) (hfU : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) U U') (hfV : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) V V') (n : ℕ) {Z : C} (h : (TopPair.ofSubset (U' ∪ V')).singularHomology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (relativeMayerVietorisFromBiprod R U V n) (CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (TopPair.ofSubsetMap f ⋯) R n) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (TopPair.singularHomologyMap (TopPair.ofSubsetMap f hfU) R n) (TopPair.singularHomologyMap (TopPair.ofSubsetMap f hfV) R n)) (CategoryTheory.CategoryStruct.comp (relativeMayerVietorisFromBiprod R U' V' n) h)

The second map of the relative Mayer–Vietoris sequence is natural in maps f : X ⟶ Y carrying U into U' and V into V'.

noncomputable def TopCat.smallSingularSubcomplexPairMap {X : TopCat} {U V : Set ↑X} {Y : TopCat} {U' V' : Set ↑Y} (f : X ⟶ Y) (hfU : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) U U') (hfV : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) V V') : (X.smallSingularSubcomplex ![U, V]).pair ⟶ (Y.smallSingularSubcomplex ![U', V']).pair

The map of singular pairs from X relative to its singular simplices lying in U or in V to Y relative to its singular simplices lying in U' or in V', induced by a map f carrying U into U' and V into V'.

@[simp]

theorem TopCat.smallSingularSubcomplexPairMap_left {X : TopCat} {U V : Set ↑X} {Y : TopCat} {U' V' : Set ↑Y} (f : X ⟶ Y) (hfU : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) U U') (hfV : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) V V') : (smallSingularSubcomplexPairMap f hfU hfV).left = smallSingularSubcomplexMap ![U, V] ![U', V'] f id ⋯

@[simp]

theorem TopCat.smallSingularSubcomplexPairMap_right {X : TopCat} {U V : Set ↑X} {Y : TopCat} {U' V' : Set ↑Y} (f : X ⟶ Y) (hfU : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) U U') (hfV : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) V V') : (smallSingularSubcomplexPairMap f hfU hfV).right = toSSet.map f

theorem TopCat.smallSingularSubcomplexPairToUnion_comp_ofSubsetMap {X : TopCat} {U V : Set ↑X} {Y : TopCat} {U' V' : Set ↑Y} (f : X ⟶ Y) (hfU : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) U U') (hfV : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) V V') : CategoryTheory.CategoryStruct.comp (smallSingularSubcomplexPairToUnion U V) (TopPair.toSSetPair.map (TopPair.ofSubsetMap f ⋯)) = CategoryTheory.CategoryStruct.comp (smallSingularSubcomplexPairMap f hfU hfV) (smallSingularSubcomplexPairToUnion U' V')

The comparison maps TopCat.smallSingularSubcomplexPairToUnion are natural in maps carrying U into U' and V into V'.

theorem TopCat.smallSingularSubcomplexPairToUnion_comp_ofSubsetMap_assoc {X : TopCat} {U V : Set ↑X} {Y : TopCat} {U' V' : Set ↑Y} (f : X ⟶ Y) (hfU : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) U U') (hfV : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) V V') {Z : SSetPair} (h : TopPair.toSSetPair.obj (TopPair.ofSubset (U' ∪ V')) ⟶ Z) : CategoryTheory.CategoryStruct.comp (smallSingularSubcomplexPairToUnion U V) (CategoryTheory.CategoryStruct.comp (TopPair.toSSetPair.map (TopPair.ofSubsetMap f ⋯)) h) = CategoryTheory.CategoryStruct.comp (smallSingularSubcomplexPairMap f hfU hfV) (CategoryTheory.CategoryStruct.comp (smallSingularSubcomplexPairToUnion U' V') h)

The comparison maps TopCat.smallSingularSubcomplexPairToUnion are natural in maps carrying U into U' and V into V'.

theorem TopCat.relativeMayerVietorisδ_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) {Y : TopCat} {U' V' : Set ↑Y} (hU' : IsOpen U') (hV' : IsOpen V') (f : X ⟶ Y) (hfU : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) U U') (hfV : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) V V') (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (relativeMayerVietorisδ R hU hV n m h) (TopPair.singularHomologyMap (TopPair.ofSubsetMap f ⋯) R m) = CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (TopPair.ofSubsetMap f ⋯) R n) (relativeMayerVietorisδ R hU' hV' n m h)

Naturality of the relative Mayer–Vietoris connecting morphism. A map f : X ⟶ Y carrying U into U' and V into V' commutes with the connecting morphisms.

theorem TopCat.relativeMayerVietorisδ_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) {Y : TopCat} {U' V' : Set ↑Y} (hU' : IsOpen U') (hV' : IsOpen V') (f : X ⟶ Y) (hfU : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) U U') (hfV : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) V V') (n m : ℕ) (h : m + 1 = n := by lia) {Z : C} (h✝ : (TopPair.ofSubset (U' ∩ V')).singularHomology R m ⟶ Z) : CategoryTheory.CategoryStruct.comp (relativeMayerVietorisδ R hU hV n m h) (CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (TopPair.ofSubsetMap f ⋯) R m) h✝) = CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (TopPair.ofSubsetMap f ⋯) R n) (CategoryTheory.CategoryStruct.comp (relativeMayerVietorisδ R hU' hV' n m h) h✝)

Naturality of the relative Mayer–Vietoris connecting morphism. A map f : X ⟶ Y carrying U into U' and V into V' commutes with the connecting morphisms.

The Mayer–Vietoris sequence of two pairs

noncomputable def TopCat.pairMayerVietorisToBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) : (TopPair.ofInclusion ⋯).singularHomology R n ⟶ (TopPair.ofInclusion hCA).singularHomology R n ⊞ (TopPair.ofInclusion hDB).singularHomology R n

The first map Hₙ(A ∩ B, C ∩ D) ⟶ Hₙ(A, C) ⊞ Hₙ(B, D) of the Mayer–Vietoris sequence of the pairs (A, C) and (B, D), with components i_A and -i_B induced by the inclusions.

@[simp]

theorem TopCat.pairMayerVietorisToBiprod_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) : CategoryTheory.CategoryStruct.comp (pairMayerVietorisToBiprod R hCA hDB n) CategoryTheory.Limits.biprod.fst = TopPair.singularHomologyMap (TopPair.ofInclusionMap ⋯ hCA (ContinuousMap.inclusion ⋯) ⋯) R n

@[simp]

theorem TopCat.pairMayerVietorisToBiprod_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) {Z : C} (h : (TopPair.ofInclusion hCA).singularHomology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (pairMayerVietorisToBiprod R hCA hDB n) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) = CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (TopPair.ofInclusionMap ⋯ hCA (ContinuousMap.inclusion ⋯) ⋯) R n) h

@[simp]

theorem TopCat.pairMayerVietorisToBiprod_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) : CategoryTheory.CategoryStruct.comp (pairMayerVietorisToBiprod R hCA hDB n) CategoryTheory.Limits.biprod.snd = -TopPair.singularHomologyMap (TopPair.ofInclusionMap ⋯ hDB (ContinuousMap.inclusion ⋯) ⋯) R n

@[simp]

theorem TopCat.pairMayerVietorisToBiprod_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) {Z : C} (h : (TopPair.ofInclusion hDB).singularHomology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (pairMayerVietorisToBiprod R hCA hDB n) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = CategoryTheory.CategoryStruct.comp (-TopPair.singularHomologyMap (TopPair.ofInclusionMap ⋯ hDB (ContinuousMap.inclusion ⋯) ⋯) R n) h

noncomputable def TopCat.pairMayerVietorisFromBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) : (TopPair.ofInclusion hCA).singularHomology R n ⊞ (TopPair.ofInclusion hDB).singularHomology R n ⟶ (TopPair.ofInclusion ⋯).singularHomology R n

The second map Hₙ(A, C) ⊞ Hₙ(B, D) ⟶ Hₙ(A ∪ B, C ∪ D) of the Mayer–Vietoris sequence of the pairs (A, C) and (B, D), the sum of the maps j_A and j_B induced by the inclusions.

@[simp]

theorem TopCat.inl_pairMayerVietorisFromBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (pairMayerVietorisFromBiprod R hCA hDB n) = TopPair.singularHomologyMap (TopPair.ofInclusionMap hCA ⋯ (ContinuousMap.inclusion ⋯) ⋯) R n

@[simp]

theorem TopCat.inl_pairMayerVietorisFromBiprod_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) {Z : C} (h : (TopPair.ofInclusion ⋯).singularHomology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp (pairMayerVietorisFromBiprod R hCA hDB n) h) = CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (TopPair.ofInclusionMap hCA ⋯ (ContinuousMap.inclusion ⋯) ⋯) R n) h

@[simp]

theorem TopCat.inr_pairMayerVietorisFromBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (pairMayerVietorisFromBiprod R hCA hDB n) = TopPair.singularHomologyMap (TopPair.ofInclusionMap hDB ⋯ (ContinuousMap.inclusion ⋯) ⋯) R n

@[simp]

theorem TopCat.inr_pairMayerVietorisFromBiprod_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) {Z : C} (h : (TopPair.ofInclusion ⋯).singularHomology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (pairMayerVietorisFromBiprod R hCA hDB n) h) = CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (TopPair.ofInclusionMap hDB ⋯ (ContinuousMap.inclusion ⋯) ⋯) R n) h

The square of singular pairs

@[reducible, inline]

noncomputable abbrev TopCat.smallSingularPair {X : TopCat} {A B C D : Set ↑X} (hCA : C ⊆ A) (hDB : D ⊆ B) : SSetPair

The pair formed by the singular simplices of X lying in A or in B and those lying in C or in D. For A and B open in A ∪ B and C and D open in C ∪ D, the small-chain theorem shows that its comparison map TopCat.smallSingularPairToUnion to the singular pair of (A ∪ B, C ∪ D) induces an isomorphism on relative homology.

@[reducible, inline]

noncomputable abbrev TopCat.toSmallSingularPair {X : TopCat} {A B C D : Set ↑X} (hCA : C ⊆ A) (hDB : D ⊆ B) {A₁ C₁ : Set ↑X} (h₁ : C₁ ⊆ A₁) {i : Fin 2} (hA : A₁ ⊆ ![A, B] i) (hC : C₁ ⊆ ![C, D] i) : TopPair.toSSetPair.obj (TopPair.ofInclusion h₁) ⟶ smallSingularPair hCA hDB

The map of singular pairs (A₁, C₁) ⟶ TopCat.smallSingularPair hCA hDB for A₁ and C₁ lying in matching members of the covers ![A, B] and ![C, D].

theorem TopCat.isPushout_toSmallSingularPair_left {X : TopCat} {A B C D : Set ↑X} (hCA : C ⊆ A) (hDB : D ⊆ B) : CategoryTheory.IsPushout (TopPair.toSSetPair.map (TopPair.ofInclusionMap ⋯ hCA (ContinuousMap.inclusion ⋯) ⋯)).left (TopPair.toSSetPair.map (TopPair.ofInclusionMap ⋯ hDB (ContinuousMap.inclusion ⋯) ⋯)).left (toSmallSingularPair hCA hDB hCA ⋯ ⋯).left (toSmallSingularPair hCA hDB hDB ⋯ ⋯).left

On subobjects, the square of singular pairs (A ∩ B, C ∩ D), (A, C), (B, D) and TopCat.smallSingularPair hCA hDB is the pushout square of the singular simplicial sets of C ∩ D, C and D and of the singular simplices lying in C or in D.

theorem TopCat.isPushout_toSmallSingularPair_right {X : TopCat} {A B C D : Set ↑X} (hCA : C ⊆ A) (hDB : D ⊆ B) : CategoryTheory.IsPushout (TopPair.toSSetPair.map (TopPair.ofInclusionMap ⋯ hCA (ContinuousMap.inclusion ⋯) ⋯)).right (TopPair.toSSetPair.map (TopPair.ofInclusionMap ⋯ hDB (ContinuousMap.inclusion ⋯) ⋯)).right (toSmallSingularPair hCA hDB hCA ⋯ ⋯).right (toSmallSingularPair hCA hDB hDB ⋯ ⋯).right

On ambient simplicial sets, the square of singular pairs (A ∩ B, C ∩ D), (A, C), (B, D) and TopCat.smallSingularPair hCA hDB is the pushout square of the singular simplicial sets of A ∩ B, A and B and of the singular simplices lying in A or in B.

Comparison with the pair (A ∪ B, C ∪ D)

@[reducible, inline]

noncomputable abbrev TopCat.smallSingularPairToUnion {X : TopCat} {A B C D : Set ↑X} (hCA : C ⊆ A) (hDB : D ⊆ B) : smallSingularPair hCA hDB ⟶ TopPair.toSSetPair.obj (TopPair.ofInclusion ⋯)

The map of singular pairs TopCat.smallSingularPair hCA hDB ⟶ (A ∪ B, C ∪ D), given by TopCat.smallSingularSubcomplexToUnion on both components.

theorem TopCat.toSmallSingularPair_comp_smallSingularPairToUnion {X : TopCat} {A B C D : Set ↑X} (hCA : C ⊆ A) (hDB : D ⊆ B) {A₁ C₁ : Set ↑X} (h₁ : C₁ ⊆ A₁) {i : Fin 2} (hA : A₁ ⊆ ![A, B] i) (hC : C₁ ⊆ ![C, D] i) (hA' : A₁ ⊆ A ∪ B) (hC' : C₁ ⊆ C ∪ D) : CategoryTheory.CategoryStruct.comp (toSmallSingularPair hCA hDB h₁ hA hC) (smallSingularPairToUnion hCA hDB) = TopPair.toSSetPair.map (TopPair.ofInclusionMap h₁ ⋯ (ContinuousMap.inclusion hA') ⋯)

Followed by TopCat.smallSingularPairToUnion, the map TopCat.toSmallSingularPair is the map of singular pairs induced by the inclusion (A₁, C₁) ⟶ (A ∪ B, C ∪ D).

theorem TopCat.isIso_homologyMap_smallSingularPairToUnion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) (n : ℕ) : CategoryTheory.IsIso (SSetPair.homologyMap (smallSingularPairToUnion hCA hDB) R n)

The relative homology of TopCat.smallSingularPair hCA hDB is identified with that of (A ∪ B, C ∪ D) by TopCat.smallSingularPairToUnion.

The long exact sequence

@[simp]

theorem TopCat.pairMayerVietorisToBiprod_fromBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) : CategoryTheory.CategoryStruct.comp (pairMayerVietorisToBiprod R hCA hDB n) (pairMayerVietorisFromBiprod R hCA hDB n) = 0

The first two maps of the Mayer–Vietoris sequence of two pairs compose to zero.

@[simp]

theorem TopCat.pairMayerVietorisToBiprod_fromBiprod_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (n : ℕ) {Z : C} (h : (TopPair.ofInclusion ⋯).singularHomology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (pairMayerVietorisToBiprod R hCA hDB n) (CategoryTheory.CategoryStruct.comp (pairMayerVietorisFromBiprod R hCA hDB n) h) = CategoryTheory.CategoryStruct.comp 0 h

The first two maps of the Mayer–Vietoris sequence of two pairs compose to zero.

noncomputable def TopCat.pairMayerVietorisδ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) (n m : ℕ) (h : m + 1 = n := by lia) : (TopPair.ofInclusion ⋯).singularHomology R n ⟶ (TopPair.ofInclusion ⋯).singularHomology R m

The connecting morphism Hₙ(A ∪ B, C ∪ D) ⟶ Hₘ(A ∩ B, C ∩ D), m + 1 = n, of the Mayer–Vietoris sequence of the pairs (A, C) and (B, D), for A and B open in A ∪ B and C and D open in C ∪ D. It is the connecting morphism of the Mayer–Vietoris sequence of the singular pairs of A ∩ B, A, B and of the singular simplices of X lying in A or in B (relative to those lying in C or in D), precomposed with the inverse of the small-chain isomorphism identifying the last of these with Hₙ(A ∪ B, C ∪ D).

@[simp]

theorem TopCat.pairMayerVietorisδ_toBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (pairMayerVietorisδ R hCA hDB hA hB hC hD n m h) (pairMayerVietorisToBiprod R hCA hDB m) = 0

@[simp]

theorem TopCat.pairMayerVietorisδ_toBiprod_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) (n m : ℕ) (h : m + 1 = n := by lia) {Z : C} (h✝ : (TopPair.ofInclusion hCA).singularHomology R m ⊞ (TopPair.ofInclusion hDB).singularHomology R m ⟶ Z) : CategoryTheory.CategoryStruct.comp (pairMayerVietorisδ R hCA hDB hA hB hC hD n m h) (CategoryTheory.CategoryStruct.comp (pairMayerVietorisToBiprod R hCA hDB m) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

@[simp]

theorem TopCat.pairMayerVietorisFromBiprod_δ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (pairMayerVietorisFromBiprod R hCA hDB n) (pairMayerVietorisδ R hCA hDB hA hB hC hD n m h) = 0

@[simp]

theorem TopCat.pairMayerVietorisFromBiprod_δ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) (n m : ℕ) (h : m + 1 = n := by lia) {Z : C} (h✝ : (TopPair.ofInclusion ⋯).singularHomology R m ⟶ Z) : CategoryTheory.CategoryStruct.comp (pairMayerVietorisFromBiprod R hCA hDB n) (CategoryTheory.CategoryStruct.comp (pairMayerVietorisδ R hCA hDB hA hB hC hD n m h) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

theorem TopCat.pairMayerVietoris_exact₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) (n m : ℕ) (h : m + 1 = n := by lia) : { X₁ := (TopPair.ofInclusion ⋯).singularHomology R n, X₂ := (TopPair.ofInclusion ⋯).singularHomology R m, X₃ := (TopPair.ofInclusion hCA).singularHomology R m ⊞ (TopPair.ofInclusion hDB).singularHomology R m, f := pairMayerVietorisδ R hCA hDB hA hB hC hD n m h, g := pairMayerVietorisToBiprod R hCA hDB m, zero := ⋯ }.Exact

Exactness of the Mayer–Vietoris sequence of two pairs at Hₘ(A ∩ B, C ∩ D).

theorem TopCat.pairMayerVietoris_exact₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) (n : ℕ) : { X₁ := (TopPair.ofInclusion ⋯).singularHomology R n, X₂ := (TopPair.ofInclusion hCA).singularHomology R n ⊞ (TopPair.ofInclusion hDB).singularHomology R n, X₃ := (TopPair.ofInclusion ⋯).singularHomology R n, f := pairMayerVietorisToBiprod R hCA hDB n, g := pairMayerVietorisFromBiprod R hCA hDB n, zero := ⋯ }.Exact

Exactness of the Mayer–Vietoris sequence of two pairs at Hₙ(A, C) ⊞ Hₙ(B, D).

theorem TopCat.pairMayerVietoris_exact₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) (n m : ℕ) (h : m + 1 = n := by lia) : { X₁ := (TopPair.ofInclusion hCA).singularHomology R n ⊞ (TopPair.ofInclusion hDB).singularHomology R n, X₂ := (TopPair.ofInclusion ⋯).singularHomology R n, X₃ := (TopPair.ofInclusion ⋯).singularHomology R m, f := pairMayerVietorisFromBiprod R hCA hDB n, g := pairMayerVietorisδ R hCA hDB hA hB hC hD n m h, zero := ⋯ }.Exact

Exactness of the Mayer–Vietoris sequence of two pairs at Hₙ(A ∪ B, C ∪ D).

theorem TopCat.mono_pairMayerVietorisToBiprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) {k : ℕ} (h : CategoryTheory.Limits.IsZero ((TopPair.ofInclusion ⋯).singularHomology R (k + 1))) : CategoryTheory.Mono (pairMayerVietorisToBiprod R hCA hDB k)

If Hₖ₊₁(A ∪ B, C ∪ D) vanishes, the first map Hₖ(A ∩ B, C ∩ D) ⟶ Hₖ(A, C) ⊞ Hₖ(B, D) of the Mayer–Vietoris sequence of two pairs is a monomorphism.

theorem TopCat.epi_pairMayerVietorisFromBiprod_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) : CategoryTheory.Epi (pairMayerVietorisFromBiprod R hCA hDB 0)

The map H₀(A, C) ⊞ H₀(B, D) ⟶ H₀(A ∪ B, C ∪ D) at the end of the Mayer–Vietoris sequence of two pairs is an epimorphism.

theorem TopCat.isZero_singularHomology_ofInclusion_union {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {X : TopCat} {A B C✝ D : Set ↑X} (hCA : C✝ ⊆ A) (hDB : D ⊆ B) (hA : IsOpen (Subtype.val ⁻¹' A)) (hB : IsOpen (Subtype.val ⁻¹' B)) (hC : IsOpen (Subtype.val ⁻¹' C✝)) (hD : IsOpen (Subtype.val ⁻¹' D)) {n : ℕ} (hAC : CategoryTheory.Limits.IsZero ((TopPair.ofInclusion hCA).singularHomology R n)) (hBD : CategoryTheory.Limits.IsZero ((TopPair.ofInclusion hDB).singularHomology R n)) (hABCD : ∀ (m : ℕ), m + 1 = n → CategoryTheory.Limits.IsZero ((TopPair.ofInclusion ⋯).singularHomology R m)) : CategoryTheory.Limits.IsZero ((TopPair.ofInclusion ⋯).singularHomology R n)

Vanishing propagates along the Mayer–Vietoris sequence of two pairs: if Hₙ(A, C) and Hₙ(B, D) vanish, and so does Hₙ₋₁(A ∩ B, C ∩ D) when n is positive, then Hₙ(A ∪ B, C ∪ D) vanishes.

Naturality of the square of singular pairs

noncomputable def TopCat.smallSingularPairMap {X : TopCat} {A B C D : Set ↑X} (hCA : C ⊆ A) (hDB : D ⊆ B) {Y : TopCat} {A' B' C' D' : Set ↑Y} (hCA' : C' ⊆ A') (hDB' : D' ⊆ B') (f : X ⟶ Y) (hfA : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) A A') (hfB : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) B B') (hfC : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) C C') (hfD : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) D D') : smallSingularPair hCA hDB ⟶ smallSingularPair hCA' hDB'

The map of pairs TopCat.smallSingularPair hCA hDB ⟶ TopCat.smallSingularPair hCA' hDB' induced by a map f carrying A, B, C and D into A', B', C' and D': the restrictions of f to the singular simplices lying in C or in D and to those lying in A or in B.

@[simp]

theorem TopCat.smallSingularPairMap_left {X : TopCat} {A B C D : Set ↑X} (hCA : C ⊆ A) (hDB : D ⊆ B) {Y : TopCat} {A' B' C' D' : Set ↑Y} (hCA' : C' ⊆ A') (hDB' : D' ⊆ B') (f : X ⟶ Y) (hfA : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) A A') (hfB : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) B B') (hfC : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) C C') (hfD : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) D D') : (smallSingularPairMap hCA hDB hCA' hDB' f hfA hfB hfC hfD).left = smallSingularSubcomplexMap ![C, D] ![C', D'] f id ⋯

@[simp]

theorem TopCat.smallSingularPairMap_right {X : TopCat} {A B C D : Set ↑X} (hCA : C ⊆ A) (hDB : D ⊆ B) {Y : TopCat} {A' B' C' D' : Set ↑Y} (hCA' : C' ⊆ A') (hDB' : D' ⊆ B') (f : X ⟶ Y) (hfA : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) A A') (hfB : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) B B') (hfC : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) C C') (hfD : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) D D') : (smallSingularPairMap hCA hDB hCA' hDB' f hfA hfB hfC hfD).right = smallSingularSubcomplexMap ![A, B] ![A', B'] f id ⋯

@[simp]

theorem TopCat.smallSingularPairMap_id {X : TopCat} {A B C D : Set ↑X} (hCA : C ⊆ A) (hDB : D ⊆ B) : smallSingularPairMap hCA hDB hCA hDB (CategoryTheory.CategoryStruct.id X) ⋯ ⋯ ⋯ ⋯ = CategoryTheory.CategoryStruct.id (smallSingularPair hCA hDB)

theorem TopCat.smallSingularPairMap_comp {X : TopCat} {A B C D : Set ↑X} (hCA : C ⊆ A) (hDB : D ⊆ B) {Y : TopCat} {A' B' C' D' : Set ↑Y} (hCA' : C' ⊆ A') (hDB' : D' ⊆ B') (f : X ⟶ Y) (hfA : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) A A') (hfB : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) B B') (hfC : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) C C') (hfD : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) D D') {Z : TopCat} {A'' B'' C'' D'' : Set ↑Z} (hCA'' : C'' ⊆ A'') (hDB'' : D'' ⊆ B'') (g : Y ⟶ Z) (hgA : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom g)) A' A'') (hgB : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom g)) B' B'') (hgC : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom g)) C' C'') (hgD : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom g)) D' D'') : smallSingularPairMap hCA hDB hCA'' hDB'' (CategoryTheory.CategoryStruct.comp f g) ⋯ ⋯ ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (smallSingularPairMap hCA hDB hCA' hDB' f hfA hfB hfC hfD) (smallSingularPairMap hCA' hDB' hCA'' hDB'' g hgA hgB hgC hgD)

The maps TopCat.smallSingularPairMap respect composition.

theorem TopCat.smallSingularPairMap_comp_assoc {X : TopCat} {A B C D : Set ↑X} (hCA : C ⊆ A) (hDB : D ⊆ B) {Y : TopCat} {A' B' C' D' : Set ↑Y} (hCA' : C' ⊆ A') (hDB' : D' ⊆ B') (f : X ⟶ Y) (hfA : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) A A') (hfB : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) B B') (hfC : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) C C') (hfD : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) D D') {Z : TopCat} {A'' B'' C'' D'' : Set ↑Z} (hCA'' : C'' ⊆ A'') (hDB'' : D'' ⊆ B'') (g : Y ⟶ Z) (hgA : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom g)) A' A'') (hgB : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom g)) B' B'') (hgC : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom g)) C' C'') (hgD : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom g)) D' D'') {Z✝ : SSetPair} (h : smallSingularPair hCA'' hDB'' ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (smallSingularPairMap hCA hDB hCA'' hDB'' (CategoryTheory.CategoryStruct.comp f g) ⋯ ⋯ ⋯ ⋯) h = CategoryTheory.CategoryStruct.comp (smallSingularPairMap hCA hDB hCA' hDB' f hfA hfB hfC hfD) (CategoryTheory.CategoryStruct.comp (smallSingularPairMap hCA' hDB' hCA'' hDB'' g hgA hgB hgC hgD) h)

The maps TopCat.smallSingularPairMap respect composition.

theorem TopCat.toSmallSingularPair_comp_smallSingularPairMap {X : TopCat} {A B C D : Set ↑X} (hCA : C ⊆ A) (hDB : D ⊆ B) {Y : TopCat} {A' B' C' D' : Set ↑Y} (hCA' : C' ⊆ A') (hDB' : D' ⊆ B') (f : X ⟶ Y) (hfA : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) A A') (hfB : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) B B') (hfC : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) C C') (hfD : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) D D') {A₁ C₁ : Set ↑X} (h₁ : C₁ ⊆ A₁) {A₂ C₂ : Set ↑Y} (h₂ : C₂ ⊆ A₂) {i : Fin 2} (hA₁ : A₁ ⊆ ![A, B] i) (hC₁ : C₁ ⊆ ![C, D] i) (hA₂ : A₂ ⊆ ![A', B'] i) (hC₂ : C₂ ⊆ ![C', D'] i) (hfA₁ : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) A₁ A₂) (hfC₁ : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) C₁ C₂) : CategoryTheory.CategoryStruct.comp (toSmallSingularPair hCA hDB h₁ hA₁ hC₁) (smallSingularPairMap hCA hDB hCA' hDB' f hfA hfB hfC hfD) = CategoryTheory.CategoryStruct.comp (TopPair.toSSetPair.map (TopPair.ofInclusionMap h₁ h₂ { toFun := Set.MapsTo.restrict (⇑(CategoryTheory.ConcreteCategory.hom f)) A₁ A₂ hfA₁, continuous_toFun := ⋯ } ⋯)) (toSmallSingularPair hCA' hDB' h₂ hA₂ hC₂)

The maps TopCat.toSmallSingularPair are natural along the maps TopCat.smallSingularPairMap.

theorem TopCat.toSmallSingularPair_comp_smallSingularPairMap_assoc {X : TopCat} {A B C D : Set ↑X} (hCA : C ⊆ A) (hDB : D ⊆ B) {Y : TopCat} {A' B' C' D' : Set ↑Y} (hCA' : C' ⊆ A') (hDB' : D' ⊆ B') (f : X ⟶ Y) (hfA : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) A A') (hfB : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) B B') (hfC : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) C C') (hfD : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) D D') {A₁ C₁ : Set ↑X} (h₁ : C₁ ⊆ A₁) {A₂ C₂ : Set ↑Y} (h₂ : C₂ ⊆ A₂) {i : Fin 2} (hA₁ : A₁ ⊆ ![A, B] i) (hC₁ : C₁ ⊆ ![C, D] i) (hA₂ : A₂ ⊆ ![A', B'] i) (hC₂ : C₂ ⊆ ![C', D'] i) (hfA₁ : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) A₁ A₂) (hfC₁ : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) C₁ C₂) {Z : SSetPair} (h : smallSingularPair hCA' hDB' ⟶ Z) : CategoryTheory.CategoryStruct.comp (toSmallSingularPair hCA hDB h₁ hA₁ hC₁) (CategoryTheory.CategoryStruct.comp (smallSingularPairMap hCA hDB hCA' hDB' f hfA hfB hfC hfD) h) = CategoryTheory.CategoryStruct.comp (TopPair.toSSetPair.map (TopPair.ofInclusionMap h₁ h₂ { toFun := Set.MapsTo.restrict (⇑(CategoryTheory.ConcreteCategory.hom f)) A₁ A₂ hfA₁, continuous_toFun := ⋯ } ⋯)) (CategoryTheory.CategoryStruct.comp (toSmallSingularPair hCA' hDB' h₂ hA₂ hC₂) h)

The maps TopCat.toSmallSingularPair are natural along the maps TopCat.smallSingularPairMap.

theorem TopCat.smallSingularPairToUnion_comp_ofInclusionMap {X : TopCat} {A B C D : Set ↑X} (hCA : C ⊆ A) (hDB : D ⊆ B) {Y : TopCat} {A' B' C' D' : Set ↑Y} (hCA' : C' ⊆ A') (hDB' : D' ⊆ B') (f : X ⟶ Y) (hfA : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) A A') (hfB : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) B B') (hfC : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) C C') (hfD : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) D D') : CategoryTheory.CategoryStruct.comp (smallSingularPairToUnion hCA hDB) (TopPair.toSSetPair.map (TopPair.ofInclusionMap ⋯ ⋯ { toFun := Set.MapsTo.restrict (⇑(CategoryTheory.ConcreteCategory.hom f)) (A ∪ B) (A' ∪ B') ⋯, continuous_toFun := ⋯ } ⋯)) = CategoryTheory.CategoryStruct.comp (smallSingularPairMap hCA hDB hCA' hDB' f hfA hfB hfC hfD) (smallSingularPairToUnion hCA' hDB')

The comparison maps TopCat.smallSingularPairToUnion are natural along the maps TopCat.smallSingularPairMap.

theorem TopCat.smallSingularPairToUnion_comp_ofInclusionMap_assoc {X : TopCat} {A B C D : Set ↑X} (hCA : C ⊆ A) (hDB : D ⊆ B) {Y : TopCat} {A' B' C' D' : Set ↑Y} (hCA' : C' ⊆ A') (hDB' : D' ⊆ B') (f : X ⟶ Y) (hfA : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) A A') (hfB : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) B B') (hfC : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) C C') (hfD : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) D D') {Z : SSetPair} (h : TopPair.toSSetPair.obj (TopPair.ofInclusion ⋯) ⟶ Z) : CategoryTheory.CategoryStruct.comp (smallSingularPairToUnion hCA hDB) (CategoryTheory.CategoryStruct.comp (TopPair.toSSetPair.map (TopPair.ofInclusionMap ⋯ ⋯ { toFun := Set.MapsTo.restrict (⇑(CategoryTheory.ConcreteCategory.hom f)) (A ∪ B) (A' ∪ B') ⋯, continuous_toFun := ⋯ } ⋯)) h) = CategoryTheory.CategoryStruct.comp (smallSingularPairMap hCA hDB hCA' hDB' f hfA hfB hfC hfD) (CategoryTheory.CategoryStruct.comp (smallSingularPairToUnion hCA' hDB') h)

The comparison maps TopCat.smallSingularPairToUnion are natural along the maps TopCat.smallSingularPairMap.