@[reducible, inline]

noncomputable abbrev FullyRelativeCapProduct.singChainCx (R : Type) [CommRing R] (Y : TopCat) : ChainComplex (ModuleCat R) ℕ

The singular chain complex S_*(Y; R) of a topological space Y with coefficients in the commutative ring R, viewed as a chain complex of R-modules indexed by ℕ.

def FullyRelativeCapProduct.subtypeIncl (X : TopCat) (A : Set ↑X) : TopCat.of ↑A ⟶ X

The continuous inclusion A ↪ X of a subset A ⊆ X as a morphism in TopCat, given by the subtype valuation map.

noncomputable def FullyRelativeCapProduct.inclChainMap (R : Type) [CommRing R] (X : TopCat) (A : Set ↑X) : singChainCx R (TopCat.of ↑A) ⟶ singChainCx R X

The chain map S_*(A; R) → S_*(X; R) induced by the inclusion of a subspace A ⊆ X into X.

noncomputable def FullyRelativeCapProduct.relSingChainCx (R : Type) [CommRing R] (X : TopCat) (A : Set ↑X) : ChainComplex (ModuleCat R) ℕ

The relative singular chain complex S_*(X, A; R), defined as the cokernel of the inclusion-induced chain map S_*(A; R) → S_*(X; R).

noncomputable def FullyRelativeCapProduct.relSingularHomology (R : Type) [CommRing R] (X : TopCat) (A : Set ↑X) (n : ℕ) : ModuleCat R

The relative singular homology H_n(X, A; R), defined as the n-th homology of the relative singular chain complex.

noncomputable def FullyRelativeCapProduct.absSingularHomology (R : Type) [CommRing R] (X : TopCat) (n : ℕ) : ModuleCat R

The absolute singular homology H_n(X; R), the n-th homology of the singular chain complex.

noncomputable def FullyRelativeCapProduct.cechCohomology (R : Type) [CommRing R] (X : TopCat) (K : Set ↑X) (p : ℕ) : ModuleCat R

The Čech cohomology Ȟ^p(K; R) of a subset K ⊆ X, obtained as the direct limit of the singular cohomologies of open neighbourhoods of K.

structure FullyRelativeCapProduct.OpenNbhdPair {X : Type} [TopologicalSpace X] (K L : Set X) : Type

A pair (U, V) of open neighbourhoods with K ⊆ U, L ⊆ V and V ⊆ U, indexing the directed system used to define relative Čech cohomology Ȟ^p(K, L; R).

• U : TopologicalSpace.Opens X
• V : TopologicalSpace.Opens X
• hK : K ⊆ ↑self.U
• hL : L ⊆ ↑self.V
• hVU : self.V ≤ self.U

@[implicit_reducible]

instance FullyRelativeCapProduct.openNbhdPair_preorder {X : Type} [TopologicalSpace X] {K L : Set X} : Preorder (OpenNbhdPair K L)

The reverse-inclusion preorder on OpenNbhdPair K L: a pair p is smaller than q when q.U ⊆ p.U and q.V ⊆ p.V. This makes the family of pairs into a directed system as the neighbourhoods shrink down to (K, L).

def FullyRelativeCapProduct.opensInclusion {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (h : V ≤ U) : TopCat.of ↑V.carrier ⟶ TopCat.of ↑U.carrier

The inclusion V ↪ U of opens V ≤ U as a morphism in TopCat.

noncomputable def FullyRelativeCapProduct.relCohomOfPair (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p : ℕ) : ModuleCat R

The relative singular cohomology H^p(U, V; R) of an OpenNbhdPair (U, V), constructed as the p-th cohomology of the kernel of the cochain restriction S^*(U; R) → S^*(V; R).

def FullyRelativeCapProduct.relCechFamily (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (p : ℕ) (pair : OpenNbhdPair K L) : Type

The underlying type of relCohomOfPair, exposed as a Type to serve as the type-theoretic family for the direct-limit construction of relative Čech cohomology.

@[implicit_reducible]

noncomputable instance FullyRelativeCapProduct.relCechFamily_addCommGroup (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (p : ℕ) (pair : OpenNbhdPair K L) : AddCommGroup (relCechFamily R p pair)

Transport the additive commutative group structure from relCohomOfPair to its underlying type relCechFamily.

@[implicit_reducible]

noncomputable instance FullyRelativeCapProduct.relCechFamily_module (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (p : ℕ) (pair : OpenNbhdPair K L) : Module R (relCechFamily R p pair)

Transport the R-module structure from relCohomOfPair to its underlying type relCechFamily.

noncomputable def FullyRelativeCapProduct.relCechTransition (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (p : ℕ) (pair₁ pair₂ : OpenNbhdPair K L) (h : pair₁ ≤ pair₂) : relCechFamily R p pair₁ →ₗ[R] relCechFamily R p pair₂

The transition map relCohomOfPair pair₁ p → relCohomOfPair pair₂ p in the directed system of open neighbourhood pairs, induced by restriction of cochains along the inclusions pair₂.U ⊆ pair₁.U and pair₂.V ⊆ pair₁.V.

noncomputable def FullyRelativeCapProduct.cechCohomologyRel (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (p : ℕ) : ModuleCat R

The relative Čech cohomology Ȟ^p(K, L; R), defined as the direct limit of the relative singular cohomologies H^p(U, V; R) over the cofinal system of OpenNbhdPairs shrinking down to (K, L).

def FullyRelativeCapProduct.complementInComplement (X : TopCat) (K L : Set ↑X) : Set ↑(TopCat.of ↑Lᶜ)

The subset (X - K) ∩ (X - L) ⊆ X - L, encoded as the preimage of Kᶜ inside the subspace Lᶜ.

def FullyRelativeCapProduct.pairToNbhdK {X : Type} [TopologicalSpace X] {K L : Set X} (pair : OpenNbhdPair K L) : CechCohomology.OpenNeighborhoods K

Extract the open neighbourhood of K from an OpenNbhdPair K L.

def FullyRelativeCapProduct.pairToNbhdL {X : Type} [TopologicalSpace X] {K L : Set X} (pair : OpenNbhdPair K L) : CechCohomology.OpenNeighborhoods L

Extract the open neighbourhood of L from an OpenNbhdPair K L.

noncomputable def FullyRelativeCapProduct.nbhdRestrictToLimit (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (p : ℕ) (pair : OpenNbhdPair K L) : relCechFamily R p pair →ₗ[R] ↑(CechCohomology.cechCohomology R K p)

For a single neighbourhood pair, the map from the relative cohomology H^p(U, V; R) to absolute Čech cohomology Ȟ^p(K; R), obtained by forgetting the relativity (via the kernel inclusion) and then injecting into the direct limit.

theorem FullyRelativeCapProduct.nbhdRestrictToLimit_compat (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (p : ℕ) (pair₁ pair₂ : OpenNbhdPair K L) (h : pair₁ ≤ pair₂) (x : relCechFamily R p pair₁) : (nbhdRestrictToLimit R p pair₂) ((relCechTransition R p pair₁ pair₂ h) x) = (nbhdRestrictToLimit R p pair₁) x

Compatibility of nbhdRestrictToLimit with the transition maps of the neighbourhood-pair directed system; required for assembling the maps into a well-defined map on the direct limit.

noncomputable def FullyRelativeCapProduct.cechCohomRestrict (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (p : ℕ) : cechCohomologyRel R X K L p ⟶ cechCohomology R X K p

The restriction map Ȟ^p(K, L; R) → Ȟ^p(K; R) from relative to absolute Čech cohomology, obtained from the direct-limit description by forgetting the relativity.

noncomputable def FullyRelativeCapProduct.nbhdToSubspaceViaLimit (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (L : Set ↑X) (p : ℕ) (U : CechCohomology.OpenNeighborhoods K) : CechCohomology.cechFamily R K p U →ₗ[R] ↑(CechCohomology.cechCohomology R L p)

For an open neighbourhood U of K, the map from the cohomology of U to the Čech cohomology of L, defined to be the natural injection into the direct limit when L ⊆ K (so U is also a neighbourhood of L), and zero otherwise.

theorem FullyRelativeCapProduct.nbhdToSubspaceViaLimit_compat (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (L : Set ↑X) (p : ℕ) (U₁ U₂ : CechCohomology.OpenNeighborhoods K) (h : U₁ ≤ U₂) (x : CechCohomology.cechFamily R K p U₁) : (nbhdToSubspaceViaLimit R L p U₂) ((CechCohomology.cechTransition R K p U₁ U₂ h) x) = (nbhdToSubspaceViaLimit R L p U₁) x

Compatibility of nbhdToSubspaceViaLimit with the Čech transition maps, required to define a map on the direct limit Ȟ^p(K; R) → Ȟ^p(L; R).

noncomputable def FullyRelativeCapProduct.cechCohomToSubspace (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (p : ℕ) : cechCohomology R X K p ⟶ cechCohomology R X L p

Restriction in Čech cohomology along a subspace inclusion L ⊆ K, giving the map Ȟ^p(K; R) → Ȟ^p(L; R) (taken to be zero if L ⊄ K).

noncomputable def FullyRelativeCapProduct.nbhdCoboundaryToLimit (R : Type) [CommRing R] {X : TopCat} (K : Set ↑X) {L : Set ↑X} (p : ℕ) (V : CechCohomology.OpenNeighborhoods L) : CechCohomology.cechFamily R L p V →ₗ[R] ↑(cechCohomologyRel R X K L (p + 1))

For an open neighbourhood V of L, the connecting map from the cohomology of V to the relative Čech cohomology Ȟ^{p+1}(K, L; R), used to assemble the boundary Ȟ^p(L; R) → Ȟ^{p+1}(K, L; R) of the long exact sequence of the pair (K, L).

theorem FullyRelativeCapProduct.nbhdCoboundaryToLimit_compat (R : Type) [CommRing R] {X : TopCat} (K : Set ↑X) {L : Set ↑X} (p : ℕ) (V₁ V₂ : CechCohomology.OpenNeighborhoods L) (h : V₁ ≤ V₂) (x : CechCohomology.cechFamily R L p V₁) : (nbhdCoboundaryToLimit R K p V₂) ((CechCohomology.cechTransition R L p V₁ V₂ h) x) = (nbhdCoboundaryToLimit R K p V₁) x

Compatibility of nbhdCoboundaryToLimit with the Čech transition maps, required to assemble the coboundary Ȟ^p(L; R) → Ȟ^{p+1}(K, L; R).

noncomputable def FullyRelativeCapProduct.cechCohomCoboundary (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (p : ℕ) : cechCohomology R X L p ⟶ cechCohomologyRel R X K L (p + 1)

The coboundary δ : Ȟ^p(L; R) → Ȟ^{p+1}(K, L; R) in the long exact sequence of the Čech pair (K, L).

def FullyRelativeCapProduct.subsetInclusion (X : TopCat) (A B : Set ↑X) (h : A ⊆ B) : TopCat.of ↑A ⟶ TopCat.of ↑B

The inclusion A ↪ B of one subset into another (with A ⊆ B), as a morphism in TopCat.

theorem FullyRelativeCapProduct.subtypeIncl_factor (X : TopCat) (A B : Set ↑X) (h : A ⊆ B) : subtypeIncl X A = CategoryTheory.CategoryStruct.comp (subsetInclusion X A B h) (subtypeIncl X B)

The inclusion A ↪ X factors through A ↪ B ↪ X whenever A ⊆ B.

def FullyRelativeCapProduct.complToComplement (X : TopCat) (K L : Set ↑X) : TopCat.of ↑(complementInComplement X K L) ⟶ TopCat.of ↑Kᶜ

The natural map (X - L) ∩ (X - K) ↪ X - K viewed as a morphism in TopCat.

theorem FullyRelativeCapProduct.tripleIncl_comm_topcat (X : TopCat) (K L : Set ↑X) : CategoryTheory.CategoryStruct.comp (subtypeIncl (TopCat.of ↑Lᶜ) (complementInComplement X K L)) (subtypeIncl X Lᶜ) = CategoryTheory.CategoryStruct.comp (complToComplement X K L) (subtypeIncl X Kᶜ)

Commutativity of the square of inclusions (Lᶜ ∩ Kᶜ) ↪ Lᶜ ↪ X and (Lᶜ ∩ Kᶜ) ↪ Kᶜ ↪ X in TopCat.

theorem FullyRelativeCapProduct.tripleIncl_comm_chain (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) : CategoryTheory.CategoryStruct.comp (inclChainMap R (TopCat.of ↑Lᶜ) (complementInComplement X K L)) (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj (ModuleCat.of R R)).map (subtypeIncl X Lᶜ)) = CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj (ModuleCat.of R R)).map (complToComplement X K L)) (inclChainMap R X Kᶜ)

The chain-level version of tripleIncl_comm_topcat: the corresponding square of chain maps between singular chain complexes commutes.

noncomputable def FullyRelativeCapProduct.tripleInclChainMap (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) : relSingChainCx R (TopCat.of ↑Lᶜ) (complementInComplement X K L) ⟶ relSingChainCx R X Kᶜ

The induced chain map on relative singular chain complexes, S_*(Lᶜ, Lᶜ ∩ Kᶜ; R) → S_*(X, Kᶜ; R), coming from the inclusions of the triple (Lᶜ ∩ Kᶜ) ⊆ Lᶜ ⊆ X and (Lᶜ ∩ Kᶜ) ⊆ Kᶜ ⊆ X.

noncomputable def FullyRelativeCapProduct.homolTripleInclusion (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (q : ℕ) : relSingularHomology R (TopCat.of ↑Lᶜ) (complementInComplement X K L) q ⟶ relSingularHomology R X Kᶜ q

The induced map on relative homology, H_q(Lᶜ, Lᶜ ∩ Kᶜ; R) → H_q(X, Kᶜ; R), coming from the inclusion of pairs (Lᶜ, Lᶜ ∩ Kᶜ) → (X, Kᶜ).

theorem FullyRelativeCapProduct.restriction_comm_chain (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (h : Kᶜ ⊆ Lᶜ) : CategoryTheory.CategoryStruct.comp (inclChainMap R X Kᶜ) (CategoryTheory.CategoryStruct.id (singChainCx R X)) = CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj (ModuleCat.of R R)).map (subsetInclusion X Kᶜ Lᶜ h)) (inclChainMap R X Lᶜ)

Compatibility square needed to define the restriction chain map S_*(X, Kᶜ; R) → S_*(X, Lᶜ; R) when Kᶜ ⊆ Lᶜ.

noncomputable def FullyRelativeCapProduct.restrictionChainMap (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (h : Kᶜ ⊆ Lᶜ) : relSingChainCx R X Kᶜ ⟶ relSingChainCx R X Lᶜ

The chain map between relative singular chain complexes S_*(X, Kᶜ; R) → S_*(X, Lᶜ; R), induced by enlarging the relative subspace from Kᶜ to Lᶜ (assuming Kᶜ ⊆ Lᶜ, i.e. L ⊆ K).

noncomputable def FullyRelativeCapProduct.homolRestriction (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (q : ℕ) : relSingularHomology R X Kᶜ q ⟶ relSingularHomology R X Lᶜ q

The restriction map H_q(X, Kᶜ; R) → H_q(X, Lᶜ; R) induced by enlarging the relative subspace from Kᶜ to Lᶜ (defined to be zero if Kᶜ ⊄ Lᶜ).

theorem FullyRelativeCapProduct.tripleInclChainMap_comp_restrictionChainMap_eq_zero (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (h : Kᶜ ⊆ Lᶜ) : CategoryTheory.CategoryStruct.comp (tripleInclChainMap R X K L) (restrictionChainMap R X K L h) = 0

The composition tripleInclChainMap ≫ restrictionChainMap vanishes, expressing the chain-level exactness needed to obtain the short exact sequence of relative chain complexes for the triple (X, Lᶜ, Kᶜ).

noncomputable def FullyRelativeCapProduct.tripleShortComplex (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (h : Kᶜ ⊆ Lᶜ) : CategoryTheory.ShortComplex (ChainComplex (ModuleCat R) ℕ)

The short complex of relative singular chain complexes for the triple (X, Lᶜ, Kᶜ), namely S_*(Lᶜ, Lᶜ ∩ Kᶜ; R) → S_*(X, Kᶜ; R) → S_*(X, Lᶜ; R).

theorem FullyRelativeCapProduct.tripleShortComplex_shortExact (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (h : Kᶜ ⊆ Lᶜ) : (tripleShortComplex R X K L h).ShortExact

The short complex tripleShortComplex is short exact; this is the chain-level input for the long exact sequence of the triple.

noncomputable def FullyRelativeCapProduct.homolTripleBoundary (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (q : ℕ) : relSingularHomology R X Lᶜ (q + 1) ⟶ relSingularHomology R (TopCat.of ↑Lᶜ) (complementInComplement X K L) q

The boundary map H_{q+1}(X, Lᶜ; R) → H_q(Lᶜ, Lᶜ ∩ Kᶜ; R) in the long exact sequence of the triple (X, Lᶜ, Kᶜ), obtained via the connecting homomorphism of tripleShortComplex_shortExact.

noncomputable def FullyRelativeCapProduct.awCapShortComplexMap_τ₁ (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p q : ℕ) (β : relCechFamily R p pair) : (HomologicalComplex.sc (relSingChainCx R (TopCat.of ↑pair.U.carrier) (Subtype.val ⁻¹' Kᶜ)) (p + q)).X₁ ⟶ (HomologicalComplex.sc (relSingChainCx R (TopCat.of ↑(pair.U.carrier \ L)) (Subtype.val ⁻¹' Kᶜ)) q).X₁

The first component τ₁ of the Alexander–Whitney cap product short-complex map at a neighbourhood pair, acting on the (p+q-1)-degree slot of the relative chain complex.

noncomputable def FullyRelativeCapProduct.awCapShortComplexMap_τ₂ (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p q : ℕ) (β : relCechFamily R p pair) : (HomologicalComplex.sc (relSingChainCx R (TopCat.of ↑pair.U.carrier) (Subtype.val ⁻¹' Kᶜ)) (p + q)).X₂ ⟶ (HomologicalComplex.sc (relSingChainCx R (TopCat.of ↑(pair.U.carrier \ L)) (Subtype.val ⁻¹' Kᶜ)) q).X₂

The middle component τ₂ of the Alexander–Whitney cap product short-complex map, acting on the (p+q)-degree slot of the relative chain complex.

noncomputable def FullyRelativeCapProduct.awCapShortComplexMap_τ₃ (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p q : ℕ) (β : relCechFamily R p pair) : (HomologicalComplex.sc (relSingChainCx R (TopCat.of ↑pair.U.carrier) (Subtype.val ⁻¹' Kᶜ)) (p + q)).X₃ ⟶ (HomologicalComplex.sc (relSingChainCx R (TopCat.of ↑(pair.U.carrier \ L)) (Subtype.val ⁻¹' Kᶜ)) q).X₃

The third component τ₃ of the Alexander–Whitney cap product short-complex map, acting on the (p+q+1)-degree slot of the relative chain complex.

theorem FullyRelativeCapProduct.awCapShortComplexMap_comm12 (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p q : ℕ) (β : relCechFamily R p pair) : CategoryTheory.CategoryStruct.comp (awCapShortComplexMap_τ₁ R pair p q β) (HomologicalComplex.sc (relSingChainCx R (TopCat.of ↑(pair.U.carrier \ L)) (Subtype.val ⁻¹' Kᶜ)) q).f = CategoryTheory.CategoryStruct.comp (HomologicalComplex.sc (relSingChainCx R (TopCat.of ↑pair.U.carrier) (Subtype.val ⁻¹' Kᶜ)) (p + q)).f (awCapShortComplexMap_τ₂ R pair p q β)

First commutativity condition (between τ₁ and τ₂) ensuring that the Alexander–Whitney cap product respects the differentials of the short complex of relative chains.

theorem FullyRelativeCapProduct.awCapShortComplexMap_comm23 (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p q : ℕ) (β : relCechFamily R p pair) : CategoryTheory.CategoryStruct.comp (awCapShortComplexMap_τ₂ R pair p q β) (HomologicalComplex.sc (relSingChainCx R (TopCat.of ↑(pair.U.carrier \ L)) (Subtype.val ⁻¹' Kᶜ)) q).g = CategoryTheory.CategoryStruct.comp (HomologicalComplex.sc (relSingChainCx R (TopCat.of ↑pair.U.carrier) (Subtype.val ⁻¹' Kᶜ)) (p + q)).g (awCapShortComplexMap_τ₃ R pair p q β)

Second commutativity condition (between τ₂ and τ₃) ensuring that the Alexander–Whitney cap product respects the differentials of the short complex of relative chains.

@[irreducible]

noncomputable def FullyRelativeCapProduct.awCapShortComplexMap (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p q : ℕ) (β : relCechFamily R p pair) : HomologicalComplex.sc (relSingChainCx R (TopCat.of ↑pair.U.carrier) (Subtype.val ⁻¹' Kᶜ)) (p + q) ⟶ HomologicalComplex.sc (relSingChainCx R (TopCat.of ↑(pair.U.carrier \ L)) (Subtype.val ⁻¹' Kᶜ)) q

The Alexander–Whitney cap product, assembled into a morphism of short complexes of relative chain complexes, at a neighbourhood pair. The short complex at degree n is the slice of S_*(U, U ∩ Kᶜ) around n, and the target is the analogous slice for (U \ L, U \ L ∩ Kᶜ) around q.

theorem FullyRelativeCapProduct.awCapShortComplexMap_τ₁_eq (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p q : ℕ) (β : relCechFamily R p pair) : (awCapShortComplexMap R pair p q β).τ₁ = awCapShortComplexMap_τ₁ R pair p q β

Projection lemma: the τ₁ component of awCapShortComplexMap is, by construction, awCapShortComplexMap_τ₁.

theorem FullyRelativeCapProduct.awCapShortComplexMap_τ₂_eq (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p q : ℕ) (β : relCechFamily R p pair) : (awCapShortComplexMap R pair p q β).τ₂ = awCapShortComplexMap_τ₂ R pair p q β

Projection lemma: the τ₂ component of awCapShortComplexMap is, by construction, awCapShortComplexMap_τ₂.

theorem FullyRelativeCapProduct.awCapShortComplexMap_τ₃_eq (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p q : ℕ) (β : relCechFamily R p pair) : (awCapShortComplexMap R pair p q β).τ₃ = awCapShortComplexMap_τ₃ R pair p q β

Projection lemma: the τ₃ component of awCapShortComplexMap is, by construction, awCapShortComplexMap_τ₃.

theorem FullyRelativeCapProduct.awCapShortComplexMap_τ₁_add (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p q : ℕ) (β₁ β₂ : relCechFamily R p pair) : awCapShortComplexMap_τ₁ R pair p q (β₁ + β₂) = awCapShortComplexMap_τ₁ R pair p q β₁ + awCapShortComplexMap_τ₁ R pair p q β₂

Additivity of the τ₁ component of the Alexander–Whitney cap product short-complex map in the cohomology class β.

theorem FullyRelativeCapProduct.awCapShortComplexMap_τ₂_add (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p q : ℕ) (β₁ β₂ : relCechFamily R p pair) : awCapShortComplexMap_τ₂ R pair p q (β₁ + β₂) = awCapShortComplexMap_τ₂ R pair p q β₁ + awCapShortComplexMap_τ₂ R pair p q β₂

Additivity of the τ₂ component of the Alexander–Whitney cap product short-complex map in the cohomology class β.

theorem FullyRelativeCapProduct.awCapShortComplexMap_τ₃_add (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p q : ℕ) (β₁ β₂ : relCechFamily R p pair) : awCapShortComplexMap_τ₃ R pair p q (β₁ + β₂) = awCapShortComplexMap_τ₃ R pair p q β₁ + awCapShortComplexMap_τ₃ R pair p q β₂

Additivity of the τ₃ component of the Alexander–Whitney cap product short-complex map in the cohomology class β.

theorem FullyRelativeCapProduct.awCapShortComplexMap_τ₁_smul (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p q : ℕ) (r : R) (β : relCechFamily R p pair) : awCapShortComplexMap_τ₁ R pair p q (r • β) = r • awCapShortComplexMap_τ₁ R pair p q β

R-linearity in the cohomology class β of the τ₁ component of the Alexander–Whitney cap product short-complex map.

theorem FullyRelativeCapProduct.awCapShortComplexMap_τ₂_smul (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p q : ℕ) (r : R) (β : relCechFamily R p pair) : awCapShortComplexMap_τ₂ R pair p q (r • β) = r • awCapShortComplexMap_τ₂ R pair p q β

R-linearity in the cohomology class β of the τ₂ component of the Alexander–Whitney cap product short-complex map.

theorem FullyRelativeCapProduct.awCapShortComplexMap_τ₃_smul (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p q : ℕ) (r : R) (β : relCechFamily R p pair) : awCapShortComplexMap_τ₃ R pair p q (r • β) = r • awCapShortComplexMap_τ₃ R pair p q β

R-linearity in the cohomology class β of the τ₃ component of the Alexander–Whitney cap product short-complex map.

theorem FullyRelativeCapProduct.awCapShortComplexMap_add (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p q : ℕ) (β₁ β₂ : relCechFamily R p pair) : awCapShortComplexMap R pair p q (β₁ + β₂) = awCapShortComplexMap R pair p q β₁ + awCapShortComplexMap R pair p q β₂

The Alexander–Whitney cap product short-complex map is additive in the cohomology class β.

theorem FullyRelativeCapProduct.awCapShortComplexMap_smul (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p q : ℕ) (r : R) (β : relCechFamily R p pair) : awCapShortComplexMap R pair p q (r • β) = r • awCapShortComplexMap R pair p q β

The Alexander–Whitney cap product short-complex map is R-linear in the cohomology class β.

noncomputable def FullyRelativeCapProduct.awCapDescendsToHomology (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p q : ℕ) (β : relCechFamily R p pair) : ↑(relSingularHomology R (TopCat.of ↑pair.U.carrier) (Subtype.val ⁻¹' Kᶜ) (p + q)) →ₗ[R] ↑(relSingularHomology R (TopCat.of ↑(pair.U.carrier \ L)) (Subtype.val ⁻¹' Kᶜ) q)

The map on relative homology obtained by passing the Alexander–Whitney cap product short-complex map to homology, giving a linear map H_{p+q}(U, U ∩ Kᶜ) → H_q(U \ L, (U \ L) ∩ Kᶜ) depending on a cohomology class β of the neighbourhood pair.

theorem FullyRelativeCapProduct.awCapDescendsToHomology_add (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p q : ℕ) (β₁ β₂ : relCechFamily R p pair) (c : ↑(relSingularHomology R (TopCat.of ↑pair.U.carrier) (Subtype.val ⁻¹' Kᶜ) (p + q))) : (awCapDescendsToHomology R pair p q (β₁ + β₂)) c = (awCapDescendsToHomology R pair p q β₁) c + (awCapDescendsToHomology R pair p q β₂) c

Additivity of awCapDescendsToHomology in the cohomology class β.

theorem FullyRelativeCapProduct.awCapDescendsToHomology_smul (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p q : ℕ) (r : R) (β : relCechFamily R p pair) (c : ↑(relSingularHomology R (TopCat.of ↑pair.U.carrier) (Subtype.val ⁻¹' Kᶜ) (p + q))) : (awCapDescendsToHomology R pair p q (r • β)) c = r • (awCapDescendsToHomology R pair p q β) c

R-linearity of awCapDescendsToHomology in the cohomology class β.

noncomputable def FullyRelativeCapProduct.relCapProductOnNbhd (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair : OpenNbhdPair K L) (p q : ℕ) : relCechFamily R p pair →ₗ[R] ↑(relSingularHomology R (TopCat.of ↑pair.U.carrier) (Subtype.val ⁻¹' Kᶜ) (p + q)) →ₗ[R] ↑(relSingularHomology R (TopCat.of ↑(pair.U.carrier \ L)) (Subtype.val ⁻¹' Kᶜ) q)

The fully relative cap product at a single neighbourhood pair, packaged as an R-linear map sending a cohomology class β in H^p(U, V; R) to the linear map H_{p+q}(U, U ∩ Kᶜ) → H_q(U \ L, (U \ L) ∩ Kᶜ) given by awCapDescendsToHomology.

def FullyRelativeCapProduct.excisionOpenIncl (X : TopCat) (U : TopologicalSpace.Opens ↑X) : TopCat.of ↑U.carrier ⟶ X

The inclusion U ↪ X of an open subspace into X, in TopCat.

def FullyRelativeCapProduct.excisionSubspaceIncl (X : TopCat) (K : Set ↑X) (U : TopologicalSpace.Opens ↑X) : TopCat.of ↑(Subtype.val ⁻¹' Kᶜ) ⟶ TopCat.of ↑Kᶜ

The inclusion U ∩ Kᶜ ↪ Kᶜ of subspaces of X, used to set up the excision map for the pair (X, Kᶜ) relative to an open neighbourhood of K.

theorem FullyRelativeCapProduct.excisionPairIncl_comm (R : Type) [CommRing R] (X : TopCat) (K : Set ↑X) (U : TopologicalSpace.Opens ↑X) : CategoryTheory.CategoryStruct.comp (inclChainMap R (TopCat.of ↑U.carrier) (Subtype.val ⁻¹' Kᶜ)) (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj (ModuleCat.of R R)).map (excisionOpenIncl X U)) = CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj (ModuleCat.of R R)).map (excisionSubspaceIncl X K U)) (inclChainMap R X Kᶜ)

Commutativity of the chain-level square used to build the excision map of pairs (U, U ∩ Kᶜ) → (X, Kᶜ).

noncomputable def FullyRelativeCapProduct.excisionPairChainMap (R : Type) [CommRing R] (X : TopCat) (K : Set ↑X) (U : TopologicalSpace.Opens ↑X) : relSingChainCx R (TopCat.of ↑U.carrier) (Subtype.val ⁻¹' Kᶜ) ⟶ relSingChainCx R X Kᶜ

The relative chain map S_*(U, U ∩ Kᶜ; R) → S_*(X, Kᶜ; R) induced by the inclusion of pairs (U, U ∩ Kᶜ) → (X, Kᶜ); this is the chain-level excision map.

noncomputable def FullyRelativeCapProduct.excisionForwardHomol (R : Type) [CommRing R] (X : TopCat) (K : Set ↑X) (U : TopologicalSpace.Opens ↑X) (n : ℕ) : relSingularHomology R (TopCat.of ↑U.carrier) (Subtype.val ⁻¹' Kᶜ) n ⟶ relSingularHomology R X Kᶜ n

The induced map on relative homology H_n(U, U ∩ Kᶜ; R) → H_n(X, Kᶜ; R) coming from the excision inclusion of pairs.

theorem FullyRelativeCapProduct.excisionPairChainMap_quasiIsoAt_forget₂ (R : Type) [CommRing R] (X : TopCat) (K : Set ↑X) (U : TopologicalSpace.Opens ↑X) (hK : K ⊆ ↑U) (n : ℕ) : QuasiIsoAt (((CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).mapHomologicalComplex (ComplexShape.down ℕ)).map (excisionPairChainMap R X K U)) n

Excision at the level of abelian groups: after forgetting the R-module structure, the chain map excisionPairChainMap is a quasi-iso at degree n.

theorem FullyRelativeCapProduct.excisionPairChainMap_quasiIsoAt (R : Type) [CommRing R] (X : TopCat) (K : Set ↑X) (U : TopologicalSpace.Opens ↑X) (hK : K ⊆ ↑U) (n : ℕ) : QuasiIsoAt (excisionPairChainMap R X K U) n

Excision in R-modules: the chain map excisionPairChainMap is a quasi-iso at degree n, obtained from the abelian-group version by transport along the forgetful functor (which preserves homology).

theorem FullyRelativeCapProduct.excisionForwardHomol_isIso (R : Type) [CommRing R] (X : TopCat) (K : Set ↑X) (U : TopologicalSpace.Opens ↑X) (hK : K ⊆ ↑U) (n : ℕ) : CategoryTheory.IsIso (excisionForwardHomol R X K U n)

The excision map on homology H_n(U, U ∩ Kᶜ; R) → H_n(X, Kᶜ; R) is an isomorphism when K ⊆ U.

noncomputable def FullyRelativeCapProduct.excisionInverseHomol (R : Type) [CommRing R] (X : TopCat) (K : Set ↑X) (U : TopologicalSpace.Opens ↑X) (hK : K ⊆ ↑U) (n : ℕ) : ↑(relSingularHomology R X Kᶜ n) →ₗ[R] ↑(relSingularHomology R (TopCat.of ↑U.carrier) (Subtype.val ⁻¹' Kᶜ) n)

The inverse of the excision isomorphism, providing a linear map H_n(X, Kᶜ; R) → H_n(U, U ∩ Kᶜ; R) that lifts a relative homology class on (X, Kᶜ) to a class supported in the open neighbourhood U of K.

def FullyRelativeCapProduct.localityBigIncl (X : TopCat) {K : Set ↑X} (L : Set ↑X) (pair : OpenNbhdPair K L) : TopCat.of ↑(pair.U.carrier \ L) ⟶ TopCat.of ↑Lᶜ

The inclusion U \ L ↪ Lᶜ as a morphism in TopCat, used to compare (U \ L, (U \ L) ∩ Kᶜ) with (Lᶜ, Lᶜ ∩ Kᶜ).

def FullyRelativeCapProduct.localitySubIncl (X : TopCat) (K L : Set ↑X) (pair : OpenNbhdPair K L) : TopCat.of ↑(Subtype.val ⁻¹' Kᶜ) ⟶ TopCat.of ↑(complementInComplement X K L)

The inclusion (U \ L) ∩ Kᶜ ↪ Lᶜ ∩ Kᶜ, viewed as a morphism in TopCat between the relativizing subspaces.

theorem FullyRelativeCapProduct.localityIncl_comm_topcat (X : TopCat) (K L : Set ↑X) (pair : OpenNbhdPair K L) : CategoryTheory.CategoryStruct.comp (subtypeIncl (TopCat.of ↑(pair.U.carrier \ L)) (Subtype.val ⁻¹' Kᶜ)) (localityBigIncl X L pair) = CategoryTheory.CategoryStruct.comp (localitySubIncl X K L pair) (subtypeIncl (TopCat.of ↑Lᶜ) (complementInComplement X K L))

Commutativity of the square of inclusions relating the pair (U \ L, (U \ L) ∩ Kᶜ) to (Lᶜ, Lᶜ ∩ Kᶜ), in TopCat.

theorem FullyRelativeCapProduct.localityIncl_comm_chain (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (pair : OpenNbhdPair K L) : CategoryTheory.CategoryStruct.comp (inclChainMap R (TopCat.of ↑(pair.U.carrier \ L)) (Subtype.val ⁻¹' Kᶜ)) (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj (ModuleCat.of R R)).map (localityBigIncl X L pair)) = CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj (ModuleCat.of R R)).map (localitySubIncl X K L pair)) (inclChainMap R (TopCat.of ↑Lᶜ) (complementInComplement X K L))

Chain-level version of localityIncl_comm_topcat: the induced square of chain maps between singular chain complexes commutes.

noncomputable def FullyRelativeCapProduct.localityInclChainMap (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (pair : OpenNbhdPair K L) : relSingChainCx R (TopCat.of ↑(pair.U.carrier \ L)) (Subtype.val ⁻¹' Kᶜ) ⟶ relSingChainCx R (TopCat.of ↑Lᶜ) (complementInComplement X K L)

The induced map of relative singular chain complexes S_*(U \ L, (U \ L) ∩ Kᶜ; R) → S_*(Lᶜ, Lᶜ ∩ Kᶜ; R) coming from the inclusions of pairs.

noncomputable def FullyRelativeCapProduct.localityForwardHomol (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (pair : OpenNbhdPair K L) (q : ℕ) : ↑(relSingularHomology R (TopCat.of ↑(pair.U.carrier \ L)) (Subtype.val ⁻¹' Kᶜ) q) →ₗ[R] ↑(relSingularHomology R (TopCat.of ↑Lᶜ) (complementInComplement X K L) q)

The induced map on relative homology H_q(U \ L, (U \ L) ∩ Kᶜ; R) → H_q(Lᶜ, Lᶜ ∩ Kᶜ; R), which is the second ingredient (after excision) of the local construction of the fully relative cap product.

noncomputable def FullyRelativeCapProduct.nbhdCapProduct (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (hLK : L ⊆ K) (hK : IsClosed K) (hL : IsClosed L) (n p q : ℕ) (hpq : p + q = n) (pair : OpenNbhdPair K L) : relCechFamily R p pair →ₗ[R] ↑(relSingularHomology R X Kᶜ n) →ₗ[R] ↑(relSingularHomology R (TopCat.of ↑Lᶜ) (complementInComplement X K L) q)

The fully relative cap product at a single open neighbourhood pair: given a cohomology class in H^p(U, V; R), it produces an R-linear map H_n(X, Kᶜ; R) → H_q(Lᶜ, Lᶜ ∩ Kᶜ; R) by composing inverse excision, relCapProductOnNbhd, and localityForwardHomol.

def FullyRelativeCapProduct.nbhdSubIncl_n {X : TopCat} {K L : Set ↑X} (pair₁ pair₂ : OpenNbhdPair K L) (h : pair₁ ≤ pair₂) : TopCat.of ↑(Subtype.val ⁻¹' Kᶜ) ⟶ TopCat.of ↑(Subtype.val ⁻¹' Kᶜ)

The induced map of "relativizing" subspaces between two nested neighbourhood pairs at the n-side: U₂ ∩ Kᶜ ↪ U₁ ∩ Kᶜ (recall the pair preorder is reversed, so pair₁ ≤ pair₂ means U₂ ⊆ U₁).

theorem FullyRelativeCapProduct.nbhdIncl_comm_topcat_n {X : TopCat} {K L : Set ↑X} (pair₁ pair₂ : OpenNbhdPair K L) (h : pair₁ ≤ pair₂) : CategoryTheory.CategoryStruct.comp (subtypeIncl (TopCat.of ↑pair₂.U.carrier) (Subtype.val ⁻¹' Kᶜ)) (opensInclusion pair₁.U pair₂.U ⋯) = CategoryTheory.CategoryStruct.comp (nbhdSubIncl_n pair₁ pair₂ h) (subtypeIncl (TopCat.of ↑pair₁.U.carrier) (Subtype.val ⁻¹' Kᶜ))

Compatibility square in TopCat between subspace and open inclusions for nested neighbourhood pairs, on the n-side.

theorem FullyRelativeCapProduct.nbhdIncl_comm_chain_n (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair₁ pair₂ : OpenNbhdPair K L) (h : pair₁ ≤ pair₂) : CategoryTheory.CategoryStruct.comp (inclChainMap R (TopCat.of ↑pair₂.U.carrier) (Subtype.val ⁻¹' Kᶜ)) (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj (ModuleCat.of R R)).map (opensInclusion pair₁.U pair₂.U ⋯)) = CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj (ModuleCat.of R R)).map (nbhdSubIncl_n pair₁ pair₂ h)) (inclChainMap R (TopCat.of ↑pair₁.U.carrier) (Subtype.val ⁻¹' Kᶜ))

Chain-level version of nbhdIncl_comm_topcat_n: the corresponding square of chain maps commutes.

noncomputable def FullyRelativeCapProduct.nbhdInclChainMap_n (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair₁ pair₂ : OpenNbhdPair K L) (h : pair₁ ≤ pair₂) : relSingChainCx R (TopCat.of ↑pair₂.U.carrier) (Subtype.val ⁻¹' Kᶜ) ⟶ relSingChainCx R (TopCat.of ↑pair₁.U.carrier) (Subtype.val ⁻¹' Kᶜ)

The chain map between relative chain complexes S_*(U₂, U₂ ∩ Kᶜ) → S_*(U₁, U₁ ∩ Kᶜ) induced by passing to a smaller pair (on the n-side).

noncomputable def FullyRelativeCapProduct.nbhdHomologyInclusion_n (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair₁ pair₂ : OpenNbhdPair K L) (h : pair₁ ≤ pair₂) (n : ℕ) : ↑(relSingularHomology R (TopCat.of ↑pair₂.U.carrier) (Subtype.val ⁻¹' Kᶜ) n) →ₗ[R] ↑(relSingularHomology R (TopCat.of ↑pair₁.U.carrier) (Subtype.val ⁻¹' Kᶜ) n)

The map on relative homology H_n(U₂, U₂ ∩ Kᶜ; R) → H_n(U₁, U₁ ∩ Kᶜ; R) induced by passing to a smaller pair (on the n-side).

def FullyRelativeCapProduct.nbhdBigIncl_q {X : TopCat} {K L : Set ↑X} (pair₁ pair₂ : OpenNbhdPair K L) (h : pair₁ ≤ pair₂) : TopCat.of ↑(pair₂.U.carrier \ L) ⟶ TopCat.of ↑(pair₁.U.carrier \ L)

The inclusion U₂ \ L ↪ U₁ \ L for two nested neighbourhood pairs, as a morphism in TopCat.

def FullyRelativeCapProduct.nbhdSubIncl_q {X : TopCat} {K L : Set ↑X} (pair₁ pair₂ : OpenNbhdPair K L) (h : pair₁ ≤ pair₂) : TopCat.of ↑(Subtype.val ⁻¹' Kᶜ) ⟶ TopCat.of ↑(Subtype.val ⁻¹' Kᶜ)

The inclusion (U₂ \ L) ∩ Kᶜ ↪ (U₁ \ L) ∩ Kᶜ for two nested neighbourhood pairs, as a morphism in TopCat (on the q-side).

theorem FullyRelativeCapProduct.nbhdIncl_comm_topcat_q {X : TopCat} {K L : Set ↑X} (pair₁ pair₂ : OpenNbhdPair K L) (h : pair₁ ≤ pair₂) : CategoryTheory.CategoryStruct.comp (subtypeIncl (TopCat.of ↑(pair₂.U.carrier \ L)) (Subtype.val ⁻¹' Kᶜ)) (nbhdBigIncl_q pair₁ pair₂ h) = CategoryTheory.CategoryStruct.comp (nbhdSubIncl_q pair₁ pair₂ h) (subtypeIncl (TopCat.of ↑(pair₁.U.carrier \ L)) (Subtype.val ⁻¹' Kᶜ))

Compatibility square in TopCat between subspace and big-pair inclusions for nested neighbourhood pairs, on the q-side.

theorem FullyRelativeCapProduct.nbhdIncl_comm_chain_q (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair₁ pair₂ : OpenNbhdPair K L) (h : pair₁ ≤ pair₂) : CategoryTheory.CategoryStruct.comp (inclChainMap R (TopCat.of ↑(pair₂.U.carrier \ L)) (Subtype.val ⁻¹' Kᶜ)) (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj (ModuleCat.of R R)).map (nbhdBigIncl_q pair₁ pair₂ h)) = CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj (ModuleCat.of R R)).map (nbhdSubIncl_q pair₁ pair₂ h)) (inclChainMap R (TopCat.of ↑(pair₁.U.carrier \ L)) (Subtype.val ⁻¹' Kᶜ))

Chain-level version of nbhdIncl_comm_topcat_q: the corresponding square of chain maps commutes on the q-side.

noncomputable def FullyRelativeCapProduct.nbhdInclChainMap_q (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair₁ pair₂ : OpenNbhdPair K L) (h : pair₁ ≤ pair₂) : relSingChainCx R (TopCat.of ↑(pair₂.U.carrier \ L)) (Subtype.val ⁻¹' Kᶜ) ⟶ relSingChainCx R (TopCat.of ↑(pair₁.U.carrier \ L)) (Subtype.val ⁻¹' Kᶜ)

The chain map between relative chain complexes S_*(U₂ \ L, (U₂ \ L) ∩ Kᶜ) → S_*(U₁ \ L, (U₁ \ L) ∩ Kᶜ) induced by passing to a smaller pair (on the q-side).

noncomputable def FullyRelativeCapProduct.nbhdHomologyInclusion_q (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair₁ pair₂ : OpenNbhdPair K L) (h : pair₁ ≤ pair₂) (q : ℕ) : ↑(relSingularHomology R (TopCat.of ↑(pair₂.U.carrier \ L)) (Subtype.val ⁻¹' Kᶜ) q) →ₗ[R] ↑(relSingularHomology R (TopCat.of ↑(pair₁.U.carrier \ L)) (Subtype.val ⁻¹' Kᶜ) q)

The map on relative homology H_q(U₂ \ L, (U₂ \ L) ∩ Kᶜ; R) → H_q(U₁ \ L, (U₁ \ L) ∩ Kᶜ; R) induced by passing to a smaller pair (on the q-side).

theorem FullyRelativeCapProduct.excisionInverseHomol_compatible (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair₁ pair₂ : OpenNbhdPair K L) (h : pair₁ ≤ pair₂) (n : ℕ) (y : ↑(relSingularHomology R X Kᶜ n)) : (excisionInverseHomol R X K pair₁.U ⋯ n) y = (nbhdHomologyInclusion_n R pair₁ pair₂ h n) ((excisionInverseHomol R X K pair₂.U ⋯ n) y)

Compatibility of inverse excision with the transition maps between nested neighbourhood pairs: lifting y ∈ H_n(X, Kᶜ; R) to a class in pair₁.U agrees with first lifting to pair₂.U and then transporting to pair₁.U via nbhdHomologyInclusion_n.

theorem FullyRelativeCapProduct.relCapProductOnNbhd_naturality (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair₁ pair₂ : OpenNbhdPair K L) (h : pair₁ ≤ pair₂) (p q : ℕ) (x : relCechFamily R p pair₁) (z : ↑(relSingularHomology R (TopCat.of ↑pair₂.U.carrier) (Subtype.val ⁻¹' Kᶜ) (p + q))) : (nbhdHomologyInclusion_q R pair₁ pair₂ h q) (((relCapProductOnNbhd R pair₂ p q) ((relCechTransition R p pair₁ pair₂ h) x)) z) = ((relCapProductOnNbhd R pair₁ p q) x) ((nbhdHomologyInclusion_n R pair₁ pair₂ h (p + q)) z)

Naturality of relCapProductOnNbhd with respect to refinement of neighbourhood pairs: capping with the restricted Čech class and then including on the q-side equals first including on the n-side and then capping.

theorem FullyRelativeCapProduct.localityForwardHomol_compatible (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (pair₁ pair₂ : OpenNbhdPair K L) (h : pair₁ ≤ pair₂) (q : ℕ) (w : ↑(relSingularHomology R (TopCat.of ↑(pair₂.U.carrier \ L)) (Subtype.val ⁻¹' Kᶜ) q)) : (localityForwardHomol R X K L pair₂ q) w = (localityForwardHomol R X K L pair₁ q) ((nbhdHomologyInclusion_q R pair₁ pair₂ h q) w)

Compatibility of localityForwardHomol with refinement of neighbourhood pairs: the value at pair₂ agrees with the value at pair₁ after using the inclusion nbhdHomologyInclusion_q.

theorem FullyRelativeCapProduct.nbhdCapProduct_composite_naturality (R : Type) [CommRing R] {X : TopCat} {K L : Set ↑X} (hLK : L ⊆ K) (hK : IsClosed K) (hL : IsClosed L) (p q : ℕ) (pair₁ pair₂ : OpenNbhdPair K L) (h : pair₁ ≤ pair₂) (x : relCechFamily R p pair₁) (y : ↑(relSingularHomology R X Kᶜ (p + q))) : (localityForwardHomol R X K L pair₂ q) (((relCapProductOnNbhd R pair₂ p q) ((relCechTransition R p pair₁ pair₂ h) x)) ((excisionInverseHomol R X K pair₂.U ⋯ (p + q)) y)) = (localityForwardHomol R X K L pair₁ q) (((relCapProductOnNbhd R pair₁ p q) x) ((excisionInverseHomol R X K pair₁.U ⋯ (p + q)) y))

The full composite naturality of the neighbourhood-pair cap product: combines excisionInverseHomol_compatible, relCapProductOnNbhd_naturality, and localityForwardHomol_compatible so that the result at pair₂ agrees with the result at pair₁ for a fixed y ∈ H_{p+q}(X, Kᶜ; R).

theorem FullyRelativeCapProduct.nbhdCapProduct_compatible (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (hLK : L ⊆ K) (hK : IsClosed K) (hL : IsClosed L) (n p q : ℕ) (hpq : p + q = n) (pair₁ pair₂ : OpenNbhdPair K L) (h : pair₁ ≤ pair₂) (x : relCechFamily R p pair₁) : (nbhdCapProduct R X K L hLK hK hL n p q hpq pair₂) ((relCechTransition R p pair₁ pair₂ h) x) = (nbhdCapProduct R X K L hLK hK hL n p q hpq pair₁) x

Compatibility of nbhdCapProduct with the transition maps of the neighbourhood-pair directed system, which is what is required to pass the cap product to a well-defined map on the direct limit Ȟ^p(K, L; R).

noncomputable def FullyRelativeCapProduct.fullyRelativeCapProduct (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (hLK : L ⊆ K) (hK : IsClosed K) (hL : IsClosed L) (n p q : ℕ) (hpq : p + q = n) : CategoryTheory.MonoidalCategoryStruct.tensorObj (cechCohomologyRel R X K L p) (relSingularHomology R X Kᶜ n) ⟶ relSingularHomology R (TopCat.of ↑Lᶜ) (complementInComplement X K L) q

The fully relative cap product Ȟ^p(K, L; R) ⊗ H_n(X, Kᶜ; R) → H_q(Lᶜ, Lᶜ ∩ Kᶜ; R) for p + q = n, obtained by assembling the neighbourhood-pair cap products nbhdCapProduct into a map out of the direct-limit description of Ȟ^p(K, L; R). This is the existence half of Theorem 36.1.

noncomputable def FullyRelativeCapProduct.awAbsCapShortComplexMap (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (U : CechCohomology.OpenNeighborhoods K) (p q : ℕ) (α : CechCohomology.cechFamily R K p U) : HomologicalComplex.sc (relSingChainCx R (TopCat.of ↑(↑U).carrier) (Subtype.val ⁻¹' Kᶜ)) (p + q) ⟶ HomologicalComplex.sc (relSingChainCx R (TopCat.of ↑(↑U).carrier) (Subtype.val ⁻¹' Kᶜ)) q

The absolute (single-subspace) version of the Alexander–Whitney cap product short-complex map: starting from a Čech class α for an open neighbourhood U of K, it gives a map of short complexes from the slice of S_*(U, U ∩ Kᶜ) at (p+q) to the slice at q.

theorem FullyRelativeCapProduct.awAbsCapShortComplexMap_add (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (U : CechCohomology.OpenNeighborhoods K) (p q : ℕ) (α₁ α₂ : CechCohomology.cechFamily R K p U) : awAbsCapShortComplexMap R U p q (α₁ + α₂) = awAbsCapShortComplexMap R U p q α₁ + awAbsCapShortComplexMap R U p q α₂

Additivity of awAbsCapShortComplexMap in the Čech cohomology class α.

theorem FullyRelativeCapProduct.awAbsCapShortComplexMap_smul (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (U : CechCohomology.OpenNeighborhoods K) (p q : ℕ) (r : R) (α : CechCohomology.cechFamily R K p U) : awAbsCapShortComplexMap R U p q (r • α) = r • awAbsCapShortComplexMap R U p q α

R-linearity of awAbsCapShortComplexMap in the Čech class α.

noncomputable def FullyRelativeCapProduct.awCapOnNbhd_descent (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (U : CechCohomology.OpenNeighborhoods K) (p q : ℕ) (α : CechCohomology.cechFamily R K p U) : ↑(relSingularHomology R (TopCat.of ↑(↑U).carrier) (Subtype.val ⁻¹' Kᶜ) (p + q)) →ₗ[R] ↑(relSingularHomology R (TopCat.of ↑(↑U).carrier) (Subtype.val ⁻¹' Kᶜ) q)

Passage to homology of awAbsCapShortComplexMap: gives the absolute cap-with-Čech-class map H_{p+q}(U, U ∩ Kᶜ) → H_q(U, U ∩ Kᶜ).

theorem FullyRelativeCapProduct.awCapOnNbhd_descent_add (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (U : CechCohomology.OpenNeighborhoods K) (p q : ℕ) (α₁ α₂ : CechCohomology.cechFamily R K p U) (c : ↑(relSingularHomology R (TopCat.of ↑(↑U).carrier) (Subtype.val ⁻¹' Kᶜ) (p + q))) : (awCapOnNbhd_descent R U p q (α₁ + α₂)) c = (awCapOnNbhd_descent R U p q α₁) c + (awCapOnNbhd_descent R U p q α₂) c

Additivity of awCapOnNbhd_descent in the Čech class α.

theorem FullyRelativeCapProduct.awCapOnNbhd_descent_smul (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (U : CechCohomology.OpenNeighborhoods K) (p q : ℕ) (r : R) (α : CechCohomology.cechFamily R K p U) (c : ↑(relSingularHomology R (TopCat.of ↑(↑U).carrier) (Subtype.val ⁻¹' Kᶜ) (p + q))) : (awCapOnNbhd_descent R U p q (r • α)) c = r • (awCapOnNbhd_descent R U p q α) c

R-linearity of awCapOnNbhd_descent in the Čech class α.

noncomputable def FullyRelativeCapProduct.absCapOnNbhd (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (U : CechCohomology.OpenNeighborhoods K) (p q : ℕ) : CechCohomology.cechFamily R K p U →ₗ[R] ↑(relSingularHomology R (TopCat.of ↑(↑U).carrier) (Subtype.val ⁻¹' Kᶜ) (p + q)) →ₗ[R] ↑(relSingularHomology R (TopCat.of ↑(↑U).carrier) (Subtype.val ⁻¹' Kᶜ) q)

The absolute cap product at a single open neighbourhood, packaged as an R-linear map from H^p(U, U ∩ Kᶜ; R) (the Čech family at U) into the space of linear maps H_{p+q}(U, U ∩ Kᶜ) → H_q(U, U ∩ Kᶜ).

noncomputable def FullyRelativeCapProduct.absCapProductOnNbhd (R : Type) [CommRing R] (X : TopCat) (K : Set ↑X) (_hK : IsClosed K) (n p q : ℕ) (hpq : p + q = n) (U : CechCohomology.OpenNeighborhoods K) : CechCohomology.cechFamily R K p U →ₗ[R] ↑(relSingularHomology R X Kᶜ n) →ₗ[R] ↑(relSingularHomology R X Kᶜ q)

The absolute cap product at a single neighbourhood U, producing a map H_n(X, Kᶜ; R) → H_q(X, Kᶜ; R) from a Čech cohomology class for U. Built by composing inverse excision, the local cap product, and forward excision.

noncomputable def FullyRelativeCapProduct.absNbhdHomologyIncl (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (U₁ U₂ : CechCohomology.OpenNeighborhoods K) (_h : U₁ ≤ U₂) (n : ℕ) : ↑(relSingularHomology R (TopCat.of ↑(↑U₂).carrier) (Subtype.val ⁻¹' Kᶜ) n) →ₗ[R] ↑(relSingularHomology R (TopCat.of ↑(↑U₁).carrier) (Subtype.val ⁻¹' Kᶜ) n)

The transition map on relative homology between two nested open neighbourhoods of K, defined as inverse excision into U₁ composed with forward excision out of U₂.

theorem FullyRelativeCapProduct.absNbhdExcisionInverse_compatible (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (U₁ U₂ : CechCohomology.OpenNeighborhoods K) (h : U₁ ≤ U₂) (n : ℕ) (y : ↑(relSingularHomology R X Kᶜ n)) : (excisionInverseHomol R X K ↑U₁ ⋯ n) y = (absNbhdHomologyIncl R U₁ U₂ h n) ((excisionInverseHomol R X K ↑U₂ ⋯ n) y)

Compatibility of excisionInverseHomol with the transition map absNbhdHomologyIncl between nested open neighbourhoods of K.

theorem FullyRelativeCapProduct.absCapOnNbhd_naturality (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (U₁ U₂ : CechCohomology.OpenNeighborhoods K) (h : U₁ ≤ U₂) (p q : ℕ) (x : CechCohomology.cechFamily R K p U₁) (z : ↑(relSingularHomology R (TopCat.of ↑(↑U₂).carrier) (Subtype.val ⁻¹' Kᶜ) (p + q))) : (absNbhdHomologyIncl R U₁ U₂ h q) (((absCapOnNbhd R U₂ p q) ((CechCohomology.cechTransition R K p U₁ U₂ h) x)) z) = ((absCapOnNbhd R U₁ p q) x) ((absNbhdHomologyIncl R U₁ U₂ h (p + q)) z)

Naturality of absCapOnNbhd with respect to refinement of open neighbourhoods of K.

theorem FullyRelativeCapProduct.absExcisionForward_compatible (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (U₁ U₂ : CechCohomology.OpenNeighborhoods K) (h : U₁ ≤ U₂) (q : ℕ) (w : ↑(relSingularHomology R (TopCat.of ↑(↑U₂).carrier) (Subtype.val ⁻¹' Kᶜ) q)) : (ModuleCat.Hom.hom (excisionForwardHomol R X K (↑U₂) q)) w = (ModuleCat.Hom.hom (excisionForwardHomol R X K (↑U₁) q)) ((absNbhdHomologyIncl R U₁ U₂ h q) w)

Compatibility of the forward excision map with the transition absNbhdHomologyIncl: the value at U₂ agrees with the value at U₁ after inclusion.

theorem FullyRelativeCapProduct.absCapProductOnNbhd_composite_naturality (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (hK : IsClosed K) (p q : ℕ) (U₁ U₂ : CechCohomology.OpenNeighborhoods K) (h : U₁ ≤ U₂) (x : CechCohomology.cechFamily R K p U₁) (y : ↑(relSingularHomology R X Kᶜ (p + q))) : (ModuleCat.Hom.hom (excisionForwardHomol R X K (↑U₂) q)) (((absCapOnNbhd R U₂ p q) ((CechCohomology.cechTransition R K p U₁ U₂ h) x)) ((excisionInverseHomol R X K ↑U₂ ⋯ (p + q)) y)) = (ModuleCat.Hom.hom (excisionForwardHomol R X K (↑U₁) q)) (((absCapOnNbhd R U₁ p q) x) ((excisionInverseHomol R X K ↑U₁ ⋯ (p + q)) y))

The composite naturality statement assembling absExcisionForward_compatible, absCapOnNbhd_naturality and absNbhdExcisionInverse_compatible for the absolute cap product.

theorem FullyRelativeCapProduct.absCapProductOnNbhd_compatible (R : Type) [CommRing R] (X : TopCat) (K : Set ↑X) (hK : IsClosed K) (n p q : ℕ) (hpq : p + q = n) (U₁ U₂ : CechCohomology.OpenNeighborhoods K) (h : U₁ ≤ U₂) (x : CechCohomology.cechFamily R K p U₁) : (absCapProductOnNbhd R X K hK n p q hpq U₂) ((CechCohomology.cechTransition R K p U₁ U₂ h) x) = (absCapProductOnNbhd R X K hK n p q hpq U₁) x

Compatibility of absCapProductOnNbhd with the Čech transition maps, which lets it descend to the direct limit Ȟ^p(K; R).

noncomputable def FullyRelativeCapProduct.cechCapAbsolute (R : Type) [CommRing R] (X : TopCat) (K : Set ↑X) (hK : IsClosed K) (n p q : ℕ) (hpq : p + q = n) : CategoryTheory.MonoidalCategoryStruct.tensorObj (cechCohomology R X K p) (relSingularHomology R X Kᶜ n) ⟶ relSingularHomology R X Kᶜ q

The absolute cap product Ȟ^p(K; R) ⊗ H_n(X, Kᶜ; R) → H_q(X, Kᶜ; R) for p + q = n, obtained by descending absCapProductOnNbhd to the direct-limit description of Ȟ^p(K; R).

noncomputable def FullyRelativeCapProduct.cechCapL (R : Type) [CommRing R] (X : TopCat) (L : Set ↑X) (hL : IsClosed L) (n p q : ℕ) (hpq : p + q = n) : CategoryTheory.MonoidalCategoryStruct.tensorObj (cechCohomology R X L p) (relSingularHomology R X Lᶜ n) ⟶ relSingularHomology R X Lᶜ q

The absolute cap product for the subspace L: Ȟ^p(L; R) ⊗ H_n(X, Lᶜ; R) → H_q(X, Lᶜ; R). Same construction as cechCapAbsolute, but applied to L rather than K.

noncomputable def FullyRelativeCapProduct.absToRelHomol (R : Type) [CommRing R] (X : TopCat) (K : Set ↑X) (n : ℕ) : absSingularHomology R X n ⟶ relSingularHomology R X Kᶜ n

The natural map H_n(X; R) → H_n(X, Kᶜ; R) from absolute to relative singular homology, induced by the cokernel projection of the relativizing chain map.

noncomputable def FullyRelativeCapProduct.relToAbsChainMap (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) : relSingChainCx R (TopCat.of ↑Lᶜ) (complementInComplement X K L) ⟶ singChainCx R (TopCat.of ↑Lᶜ)

A chain-level splitting/section of relative chains S_*(Lᶜ, Lᶜ ∩ Kᶜ; R) → S_*(Lᶜ; R), used to construct the comparison map between the relative and absolute homology groups appearing in Theorem 36.1.

noncomputable def FullyRelativeCapProduct.relComplementToAbs (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (q : ℕ) : relSingularHomology R (TopCat.of ↑Lᶜ) (complementInComplement X K L) q ⟶ absSingularHomology R X q

The composite map H_q(Lᶜ, Lᶜ ∩ Kᶜ; R) → H_q(X; R) obtained by first applying relToAbsChainMap and then including Lᶜ ↪ X.

noncomputable def FullyRelativeCapProduct.awCapAbsShortComplexMap (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (U : CechCohomology.OpenNeighborhoods K) (p q : ℕ) (α : CechCohomology.cechFamily R K p U) : HomologicalComplex.sc (singChainCx R X) (p + q) ⟶ HomologicalComplex.sc (singChainCx R X) q

The Alexander–Whitney cap product short-complex map at the level of absolute singular chains on X, parametrized by a Čech class α on a neighbourhood U of K.

theorem FullyRelativeCapProduct.awCapAbsShortComplexMap_add (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (U : CechCohomology.OpenNeighborhoods K) (p q : ℕ) (α₁ α₂ : CechCohomology.cechFamily R K p U) : awCapAbsShortComplexMap R U p q (α₁ + α₂) = awCapAbsShortComplexMap R U p q α₁ + awCapAbsShortComplexMap R U p q α₂

Additivity of awCapAbsShortComplexMap in the Čech class α.

theorem FullyRelativeCapProduct.awCapAbsShortComplexMap_smul (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (U : CechCohomology.OpenNeighborhoods K) (p q : ℕ) (r : R) (α : CechCohomology.cechFamily R K p U) : awCapAbsShortComplexMap R U p q (r • α) = r • awCapAbsShortComplexMap R U p q α

R-linearity of awCapAbsShortComplexMap in the Čech class α.

theorem FullyRelativeCapProduct.awCapAbsShortComplexMap_naturality (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (U₁ U₂ : CechCohomology.OpenNeighborhoods K) (h : U₁ ≤ U₂) (p q : ℕ) (x : CechCohomology.cechFamily R K p U₁) : awCapAbsShortComplexMap R U₂ p q ((CechCohomology.cechTransition R K p U₁ U₂ h) x) = awCapAbsShortComplexMap R U₁ p q x

Naturality of awCapAbsShortComplexMap along the Čech transition maps; allows the absolute cap product on absolute homology to descend to the direct limit.

noncomputable def FullyRelativeCapProduct.awCapDescendsToAbsHomology (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (U : CechCohomology.OpenNeighborhoods K) (p q : ℕ) (α : CechCohomology.cechFamily R K p U) : ↑(absSingularHomology R X (p + q)) →ₗ[R] ↑(absSingularHomology R X q)

Passage of awCapAbsShortComplexMap to absolute singular homology: gives a linear map H_{p+q}(X; R) → H_q(X; R) parametrized by a Čech cohomology class α on a neighbourhood U of K.

theorem FullyRelativeCapProduct.awCapDescendsToAbsHomology_add (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (U : CechCohomology.OpenNeighborhoods K) (p q : ℕ) (α₁ α₂ : CechCohomology.cechFamily R K p U) (z : ↑(absSingularHomology R X (p + q))) : (awCapDescendsToAbsHomology R U p q (α₁ + α₂)) z = (awCapDescendsToAbsHomology R U p q α₁) z + (awCapDescendsToAbsHomology R U p q α₂) z

Additivity of awCapDescendsToAbsHomology in the Čech class α.

theorem FullyRelativeCapProduct.awCapDescendsToAbsHomology_smul (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (U : CechCohomology.OpenNeighborhoods K) (p q : ℕ) (r : R) (α : CechCohomology.cechFamily R K p U) (z : ↑(absSingularHomology R X (p + q))) : (awCapDescendsToAbsHomology R U p q (r • α)) z = r • (awCapDescendsToAbsHomology R U p q α) z

R-linearity of awCapDescendsToAbsHomology in the Čech class α.

noncomputable def FullyRelativeCapProduct.absCapOnNbhdAbsHomol (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (U : CechCohomology.OpenNeighborhoods K) (p q : ℕ) : CechCohomology.cechFamily R K p U →ₗ[R] ↑(absSingularHomology R X (p + q)) →ₗ[R] ↑(absSingularHomology R X q)

The absolute cap product on absolute singular homology at a single neighbourhood U, packaged as an R-linear map from the Čech family to the space of linear maps H_{p+q}(X; R) → H_q(X; R).

theorem FullyRelativeCapProduct.absCapOnNbhdAbsHomol_naturality (R : Type) [CommRing R] {X : TopCat} {K : Set ↑X} (p q : ℕ) (U₁ U₂ : CechCohomology.OpenNeighborhoods K) (h : U₁ ≤ U₂) (x : CechCohomology.cechFamily R K p U₁) (z : ↑(absSingularHomology R X (p + q))) : ((absCapOnNbhdAbsHomol R U₂ p q) ((CechCohomology.cechTransition R K p U₁ U₂ h) x)) z = ((absCapOnNbhdAbsHomol R U₁ p q) x) z

Naturality of absCapOnNbhdAbsHomol along the Čech transition maps: needed to descend the absolute cap product on absolute homology to the direct limit Ȟ^p(K; R).

noncomputable def FullyRelativeCapProduct.absCapProductOnNbhdAbs (R : Type) [CommRing R] (X : TopCat) (K : Set ↑X) (_hK : IsClosed K) (n p q : ℕ) (hpq : p + q = n) (U : CechCohomology.OpenNeighborhoods K) : CechCohomology.cechFamily R K p U →ₗ[R] ↑(absSingularHomology R X n) →ₗ[R] ↑(absSingularHomology R X q)

n-indexed packaging of absCapOnNbhdAbsHomol for use in the descent to the direct limit, substituting hpq : p + q = n.

theorem FullyRelativeCapProduct.absCapProductOnNbhdAbs_compatible (R : Type) [CommRing R] (X : TopCat) (K : Set ↑X) (hK : IsClosed K) (n p q : ℕ) (hpq : p + q = n) (U₁ U₂ : CechCohomology.OpenNeighborhoods K) (h : U₁ ≤ U₂) (x : CechCohomology.cechFamily R K p U₁) : (absCapProductOnNbhdAbs R X K hK n p q hpq U₂) ((CechCohomology.cechTransition R K p U₁ U₂ h) x) = (absCapProductOnNbhdAbs R X K hK n p q hpq U₁) x

Compatibility of absCapProductOnNbhdAbs with Čech transition maps, used to descend to the direct limit.

noncomputable def FullyRelativeCapProduct.cechCapAbsK (R : Type) [CommRing R] (X : TopCat) (K : Set ↑X) (hK : IsClosed K) (n p q : ℕ) (hpq : p + q = n) : CategoryTheory.MonoidalCategoryStruct.tensorObj (cechCohomology R X K p) (absSingularHomology R X n) ⟶ absSingularHomology R X q

The cap product with K-Čech cohomology landing in absolute singular homology: Ȟ^p(K; R) ⊗ H_n(X; R) → H_q(X; R) for p + q = n.

noncomputable def FullyRelativeCapProduct.cechCapAbsL (R : Type) [CommRing R] (X : TopCat) (L : Set ↑X) (hL : IsClosed L) (n p q : ℕ) (hpq : p + q = n) : CategoryTheory.MonoidalCategoryStruct.tensorObj (cechCohomology R X L p) (absSingularHomology R X n) ⟶ absSingularHomology R X q

The cap product with L-Čech cohomology landing in absolute singular homology: Ȟ^p(L; R) ⊗ H_n(X; R) → H_q(X; R) for p + q = n.

noncomputable def FullyRelativeCapProduct.fullyRelativeCapProductAbs (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (hLK : L ⊆ K) (hK : IsClosed K) (hL : IsClosed L) (n p q : ℕ) (hpq : p + q = n) : CategoryTheory.MonoidalCategoryStruct.tensorObj (cechCohomologyRel R X K L p) (absSingularHomology R X n) ⟶ relSingularHomology R (TopCat.of ↑Lᶜ) (complementInComplement X K L) q

The fully relative cap product applied to a class in absolute homology: Ȟ^p(K, L; R) ⊗ H_n(X; R) → H_q(Lᶜ, Lᶜ ∩ Kᶜ; R), obtained by first sending H_n(X; R) to H_n(X, Kᶜ; R) and then capping.

structure FullyRelativeCapProduct.FullyRelativeCapProductData (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (hLK : L ⊆ K) (hK : IsClosed K) (hL : IsClosed L) (n : ℕ) : Type

All data witnessing Theorem 36.1: a fully relative cap product Ȟ^p(K, L; R) ⊗ H_n(X, Kᶜ; R) → H_q(Lᶜ, Lᶜ ∩ Kᶜ; R) together with the two commuting ladders ("first" using H_n(X, Kᶜ) and "second" using H_n(X)) involving the long exact sequences of the pairs (K, L) in Čech cohomology and the relative homology long exact sequences in singular homology.

• capProduct (p q : ℕ) (_hpq : p + q = n) : CategoryTheory.MonoidalCategoryStruct.tensorObj (cechCohomologyRel R X K L p) (relSingularHomology R X Kᶜ n) ⟶ relSingularHomology R (TopCat.of ↑Lᶜ) (complementInComplement X K L) q
• firstLadder_restrict (p q : ℕ) (hpq : p + q = n) : CategoryTheory.CategoryStruct.comp (self.capProduct p q hpq) (homolTripleInclusion R X K L q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (cechCohomRestrict R X K L p) (relSingularHomology R X Kᶜ n)) (cechCapAbsolute R X K hK n p q hpq)
• firstLadder_subspace (p q : ℕ) (hpq : p + q = n) : CategoryTheory.CategoryStruct.comp (cechCapAbsolute R X K hK n p q hpq) (homolRestriction R X K L q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (cechCohomToSubspace R X K L p) (homolRestriction R X K L n)) (cechCapL R X L hL n p q hpq)
• firstLadder_coboundary (p q : ℕ) (hpq : p + (q + 1) = n) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (cechCohomCoboundary R X K L p) (relSingularHomology R X Kᶜ n)) (self.capProduct (p + 1) q ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (cechCohomology R X L p) (homolRestriction R X K L n)) (CategoryTheory.CategoryStruct.comp (cechCapL R X L hL n p (q + 1) hpq) (homolTripleBoundary R X K L q))
• secondLadder_restrict (p q : ℕ) (hpq : p + q = n) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (cechCohomRestrict R X K L p) (absSingularHomology R X n)) (cechCapAbsK R X K hK n p q hpq) = CategoryTheory.CategoryStruct.comp (fullyRelativeCapProductAbs R X K L hLK hK hL n p q hpq) (relComplementToAbs R X K L q)
• secondLadder_subspace (p q : ℕ) (hpq : p + q = n) : cechCapAbsK R X K hK n p q hpq = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (cechCohomToSubspace R X K L p) (absSingularHomology R X n)) (cechCapAbsL R X L hL n p q hpq)
• secondLadder_coboundary (p q : ℕ) (hpq : p + (q + 1) = n) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (cechCohomCoboundary R X K L p) (absSingularHomology R X n)) (fullyRelativeCapProductAbs R X K L hLK hK hL n (p + 1) q ⋯) = CategoryTheory.CategoryStruct.comp (cechCapAbsL R X L hL n p (q + 1) hpq) (CategoryTheory.CategoryStruct.comp (absToRelHomol R X L (q + 1)) (homolTripleBoundary R X K L q))

theorem FullyRelativeCapProduct.theorem_36_1_firstLadder_restrict (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (hLK : L ⊆ K) (hK : IsClosed K) (hL : IsClosed L) (n p q : ℕ) (hpq : p + q = n) : CategoryTheory.CategoryStruct.comp (fullyRelativeCapProduct R X K L hLK hK hL n p q hpq) (homolTripleInclusion R X K L q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (cechCohomRestrict R X K L p) (relSingularHomology R X Kᶜ n)) (cechCapAbsolute R X K hK n p q hpq)

First commutative square (restriction) in the first ladder of Theorem 36.1: capping with Ȟ^p(K, L; R) and projecting H_q(Lᶜ, Lᶜ ∩ Kᶜ) into H_q(X, Kᶜ) agrees with restricting Ȟ^p(K, L; R) → Ȟ^p(K; R) and then applying the absolute cap product.

theorem FullyRelativeCapProduct.theorem_36_1_firstLadder_subspace (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (hLK : L ⊆ K) (hK : IsClosed K) (hL : IsClosed L) (n p q : ℕ) (hpq : p + q = n) : CategoryTheory.CategoryStruct.comp (cechCapAbsolute R X K hK n p q hpq) (homolRestriction R X K L q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (cechCohomToSubspace R X K L p) (homolRestriction R X K L n)) (cechCapL R X L hL n p q hpq)

Second commutative square (subspace) in the first ladder of Theorem 36.1: the absolute cap product with K followed by restricting Kᶜ → Lᶜ agrees with restricting both K → L (in Čech cohomology) and Kᶜ → Lᶜ (in singular homology) and then capping with L.

theorem FullyRelativeCapProduct.theorem_36_1_firstLadder_coboundary (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (hLK : L ⊆ K) (hK : IsClosed K) (hL : IsClosed L) (n p q : ℕ) (hpq : p + (q + 1) = n) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (cechCohomCoboundary R X K L p) (relSingularHomology R X Kᶜ n)) (fullyRelativeCapProduct R X K L hLK hK hL n (p + 1) q ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (cechCohomology R X L p) (homolRestriction R X K L n)) (CategoryTheory.CategoryStruct.comp (cechCapL R X L hL n p (q + 1) hpq) (homolTripleBoundary R X K L q))

Coboundary commutative square in the first ladder of Theorem 36.1: the Čech coboundary Ȟ^p(L; R) → Ȟ^{p+1}(K, L; R) is matched by the boundary H_{q+1}(X, Lᶜ; R) → H_q(Lᶜ, Lᶜ ∩ Kᶜ; R) of the long exact sequence of the triple.

theorem FullyRelativeCapProduct.theorem_36_1_secondLadder_restrict (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (hLK : L ⊆ K) (hK : IsClosed K) (hL : IsClosed L) (n p q : ℕ) (hpq : p + q = n) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (cechCohomRestrict R X K L p) (absSingularHomology R X n)) (cechCapAbsK R X K hK n p q hpq) = CategoryTheory.CategoryStruct.comp (fullyRelativeCapProductAbs R X K L hLK hK hL n p q hpq) (relComplementToAbs R X K L q)

First commutative square (restriction) in the second ladder of Theorem 36.1, where the homology variable lies in H_n(X) rather than H_n(X, Kᶜ).

theorem FullyRelativeCapProduct.theorem_36_1_secondLadder_subspace (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (hLK : L ⊆ K) (hK : IsClosed K) (hL : IsClosed L) (n p q : ℕ) (hpq : p + q = n) : cechCapAbsK R X K hK n p q hpq = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (cechCohomToSubspace R X K L p) (absSingularHomology R X n)) (cechCapAbsL R X L hL n p q hpq)

Second commutative square (subspace) in the second ladder of Theorem 36.1: cap with Ȟ^p(K) agrees with first restricting K → L and then capping with Ȟ^p(L), when the homology variable lies in H_n(X).

theorem FullyRelativeCapProduct.theorem_36_1_secondLadder_coboundary (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (hLK : L ⊆ K) (hK : IsClosed K) (hL : IsClosed L) (n p q : ℕ) (hpq : p + (q + 1) = n) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (cechCohomCoboundary R X K L p) (absSingularHomology R X n)) (fullyRelativeCapProductAbs R X K L hLK hK hL n (p + 1) q ⋯) = CategoryTheory.CategoryStruct.comp (cechCapAbsL R X L hL n p (q + 1) hpq) (CategoryTheory.CategoryStruct.comp (absToRelHomol R X L (q + 1)) (homolTripleBoundary R X K L q))

Coboundary commutative square in the second ladder of Theorem 36.1: the Čech coboundary Ȟ^p(L) → Ȟ^{p+1}(K, L) is matched by the composite H_{q+1}(X, Lᶜ) → H_q(Lᶜ, Lᶜ ∩ Kᶜ) of the long exact sequence of the triple.

noncomputable def FullyRelativeCapProduct.theorem_36_1 (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (hLK : L ⊆ K) (hK : IsClosed K) (hL : IsClosed L) (n : ℕ) : FullyRelativeCapProductData R X K L hLK hK hL n

Theorem 36.1. For closed subspaces L ⊆ K of X, there is a fully relative cap product ∩ : Ȟ^p(K, L; R) ⊗ H_n(X, X - K; R) → H_q(X - L, X - K; R), p + q = n, such that for any x_K ∈ H_n(X, X - K) the ladder involving the long exact sequences of the pairs (K, L) in Čech cohomology and the corresponding relative singular homology long exact sequences commutes (with x_L the restriction of x_K to H_n(X, X - L)), and for any x ∈ H_n(X) the corresponding ladder also commutes (with x_K the restriction of x to H_n(X, X - K)). Packaged as a FullyRelativeCapProductData.

def MayerVietorisHypothesis (X : Type u_1) [TopologicalSpace X] (A B : Set X) : Prop

The standing hypothesis for the Čech/singular Mayer–Vietoris compatibility theorem: either X is a normal space and A, B are closed in X, or X is Hausdorff and A, B are compact.

structure MayerVietorisLadder (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (n : ℕ) (x_union : ↑(FullyRelativeCapProduct.relSingularHomology R X (A ∪ B)ᶜ n)) : Type

Data witnessing the Čech/singular Mayer–Vietoris compatibility ladder of Theorem 36.2: a Mayer–Vietoris sequence in Čech cohomology of A, B, A ∪ B, A ∩ B, a Mayer–Vietoris sequence in relative singular homology of their complements, exactness of both sequences, "cap rungs" connecting them indexed by subsets S ∈ {A, B, A ∪ B, A ∩ B} for each (p, q) with p + q = n, and three commutative squares expressing compatibility with the union-to-sum, sum-to-intersection, and connecting morphisms.

• topUnionToSum (p : ℕ) : FullyRelativeCapProduct.cechCohomology R X (A ∪ B) p ⟶ FullyRelativeCapProduct.cechCohomology R X A p ⊞ FullyRelativeCapProduct.cechCohomology R X B p
• topSumToInter (p : ℕ) : FullyRelativeCapProduct.cechCohomology R X A p ⊞ FullyRelativeCapProduct.cechCohomology R X B p ⟶ FullyRelativeCapProduct.cechCohomology R X (A ∩ B) p
• topConnecting (p : ℕ) : FullyRelativeCapProduct.cechCohomology R X (A ∩ B) p ⟶ FullyRelativeCapProduct.cechCohomology R X (A ∪ B) (p + 1)
• botUnionToSum (q : ℕ) : FullyRelativeCapProduct.relSingularHomology R X (A ∪ B)ᶜ q ⟶ FullyRelativeCapProduct.relSingularHomology R X Aᶜ q ⊞ FullyRelativeCapProduct.relSingularHomology R X Bᶜ q
• botSumToInter (q : ℕ) : FullyRelativeCapProduct.relSingularHomology R X Aᶜ q ⊞ FullyRelativeCapProduct.relSingularHomology R X Bᶜ q ⟶ FullyRelativeCapProduct.relSingularHomology R X (A ∩ B)ᶜ q
• botConnecting (q : ℕ) : FullyRelativeCapProduct.relSingularHomology R X (A ∩ B)ᶜ q ⟶ FullyRelativeCapProduct.relSingularHomology R X (A ∪ B)ᶜ (q - 1)
• capRung (p q : ℕ) (S : Set ↑X) : p + q = n → (FullyRelativeCapProduct.cechCohomology R X S p ⟶ FullyRelativeCapProduct.relSingularHomology R X Sᶜ q)
• top_exact_sum (p : ℕ) : Function.Exact ⇑(ModuleCat.Hom.hom (self.topUnionToSum p)) ⇑(ModuleCat.Hom.hom (self.topSumToInter p))
• top_exact_inter (p : ℕ) : Function.Exact ⇑(ModuleCat.Hom.hom (self.topSumToInter p)) ⇑(ModuleCat.Hom.hom (self.topConnecting p))
• top_exact_union (p : ℕ) : Function.Exact ⇑(ModuleCat.Hom.hom (self.topConnecting p)) ⇑(ModuleCat.Hom.hom (self.topUnionToSum (p + 1)))
• bot_exact_sum (q : ℕ) : Function.Exact ⇑(ModuleCat.Hom.hom (self.botUnionToSum q)) ⇑(ModuleCat.Hom.hom (self.botSumToInter q))
• bot_exact_inter (q : ℕ) : Function.Exact ⇑(ModuleCat.Hom.hom (self.botSumToInter q)) ⇑(ModuleCat.Hom.hom (self.botConnecting q))
• bot_exact_union (q : ℕ) : Function.Exact ⇑(ModuleCat.Hom.hom (self.botConnecting q)) ⇑(ModuleCat.Hom.hom (self.botUnionToSum (q - 1)))
• comm_sq1 (p q : ℕ) (hpq : p + q = n) : CategoryTheory.CategoryStruct.comp (self.capRung p q (A ∪ B) hpq) (self.botUnionToSum q) = CategoryTheory.CategoryStruct.comp (self.topUnionToSum p) (CategoryTheory.Limits.biprod.map (self.capRung p q A hpq) (self.capRung p q B hpq))
• comm_sq2 (p q : ℕ) (hpq : p + q = n) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (self.capRung p q A hpq) (self.capRung p q B hpq)) (self.botSumToInter q) = CategoryTheory.CategoryStruct.comp (self.topSumToInter p) (self.capRung p q (A ∩ B) hpq)
• comm_sq3 (p q : ℕ) (hpq : p + q = n) (hpq' : p + 1 + (q - 1) = n) : CategoryTheory.CategoryStruct.comp (self.topConnecting p) (self.capRung (p + 1) (q - 1) (A ∪ B) hpq') = CategoryTheory.CategoryStruct.comp (self.capRung p q (A ∩ B) hpq) (self.botConnecting q)

structure CechMVSequence (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) : Type

Abstract data of a Mayer–Vietoris long exact sequence in Čech cohomology for the cover A, B of A ∪ B: a union-to-sum map, a sum-to-intersection map, a degree-raising connecting morphism, and the three exactness conditions making the resulting sequence long exact.

• unionToSum (p : ℕ) : FullyRelativeCapProduct.cechCohomology R X (A ∪ B) p ⟶ FullyRelativeCapProduct.cechCohomology R X A p ⊞ FullyRelativeCapProduct.cechCohomology R X B p
• sumToInter (p : ℕ) : FullyRelativeCapProduct.cechCohomology R X A p ⊞ FullyRelativeCapProduct.cechCohomology R X B p ⟶ FullyRelativeCapProduct.cechCohomology R X (A ∩ B) p
• connecting (p : ℕ) : FullyRelativeCapProduct.cechCohomology R X (A ∩ B) p ⟶ FullyRelativeCapProduct.cechCohomology R X (A ∪ B) (p + 1)
• exact_sum (p : ℕ) : Function.Exact ⇑(ModuleCat.Hom.hom (self.unionToSum p)) ⇑(ModuleCat.Hom.hom (self.sumToInter p))
• exact_inter (p : ℕ) : Function.Exact ⇑(ModuleCat.Hom.hom (self.sumToInter p)) ⇑(ModuleCat.Hom.hom (self.connecting p))
• exact_union (p : ℕ) : Function.Exact ⇑(ModuleCat.Hom.hom (self.connecting p)) ⇑(ModuleCat.Hom.hom (self.unionToSum (p + 1)))

structure SingularMVSequence (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) : Type

Abstract data of a Mayer–Vietoris long exact sequence in relative singular homology for the cover A, B of A ∪ B (taken in the complements): a union-to-sum map, a sum-to-intersection map, a degree-lowering connecting morphism, and the three exactness conditions.

• unionToSum (q : ℕ) : FullyRelativeCapProduct.relSingularHomology R X (A ∪ B)ᶜ q ⟶ FullyRelativeCapProduct.relSingularHomology R X Aᶜ q ⊞ FullyRelativeCapProduct.relSingularHomology R X Bᶜ q
• sumToInter (q : ℕ) : FullyRelativeCapProduct.relSingularHomology R X Aᶜ q ⊞ FullyRelativeCapProduct.relSingularHomology R X Bᶜ q ⟶ FullyRelativeCapProduct.relSingularHomology R X (A ∩ B)ᶜ q
• connecting (q : ℕ) : FullyRelativeCapProduct.relSingularHomology R X (A ∩ B)ᶜ q ⟶ FullyRelativeCapProduct.relSingularHomology R X (A ∪ B)ᶜ (q - 1)
• exact_sum (q : ℕ) : Function.Exact ⇑(ModuleCat.Hom.hom (self.unionToSum q)) ⇑(ModuleCat.Hom.hom (self.sumToInter q))
• exact_inter (q : ℕ) : Function.Exact ⇑(ModuleCat.Hom.hom (self.sumToInter q)) ⇑(ModuleCat.Hom.hom (self.connecting q))
• exact_union (q : ℕ) : Function.Exact ⇑(ModuleCat.Hom.hom (self.connecting q)) ⇑(ModuleCat.Hom.hom (self.unionToSum (q - 1)))

structure MVCapProductData (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (n : ℕ) (x_union : ↑(FullyRelativeCapProduct.relSingularHomology R X (A ∪ B)ᶜ n)) (cechMV : CechMVSequence R X A B) (singMV : SingularMVSequence R X A B) : Type

The "cap rung" data connecting a Čech Mayer–Vietoris sequence to a singular Mayer–Vietoris sequence in the presence of a fixed homology class x_union ∈ H_n(X, (A ∪ B)ᶜ): cap product maps for each subset S ∈ {A, B, A ∪ B, A ∩ B} and (p, q) with p + q = n, plus the three commutative squares expressing Mayer–Vietoris naturality.

• capRung (p q : ℕ) (S : Set ↑X) : p + q = n → (FullyRelativeCapProduct.cechCohomology R X S p ⟶ FullyRelativeCapProduct.relSingularHomology R X Sᶜ q)
• comm_sq1 (p q : ℕ) (hpq : p + q = n) : CategoryTheory.CategoryStruct.comp (self.capRung p q (A ∪ B) hpq) (singMV.unionToSum q) = CategoryTheory.CategoryStruct.comp (cechMV.unionToSum p) (CategoryTheory.Limits.biprod.map (self.capRung p q A hpq) (self.capRung p q B hpq))
• comm_sq2 (p q : ℕ) (hpq : p + q = n) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (self.capRung p q A hpq) (self.capRung p q B hpq)) (singMV.sumToInter q) = CategoryTheory.CategoryStruct.comp (cechMV.sumToInter p) (self.capRung p q (A ∩ B) hpq)
• comm_sq3 (p q : ℕ) (hpq : p + q = n) (hpq' : p + 1 + (q - 1) = n) : CategoryTheory.CategoryStruct.comp (cechMV.connecting p) (self.capRung (p + 1) (q - 1) (A ∪ B) hpq') = CategoryTheory.CategoryStruct.comp (self.capRung p q (A ∩ B) hpq) (singMV.connecting q)

noncomputable def cechMV_unionToSum (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (p : ℕ) : FullyRelativeCapProduct.cechCohomology R X (A ∪ B) p ⟶ FullyRelativeCapProduct.cechCohomology R X A p ⊞ FullyRelativeCapProduct.cechCohomology R X B p

The Mayer–Vietoris union-to-sum map in Čech cohomology, Ȟ^p(A ∪ B; R) → Ȟ^p(A; R) ⊕ Ȟ^p(B; R), given by pairing the two restriction maps.

noncomputable def cechMV_sumToInter (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (p : ℕ) : FullyRelativeCapProduct.cechCohomology R X A p ⊞ FullyRelativeCapProduct.cechCohomology R X B p ⟶ FullyRelativeCapProduct.cechCohomology R X (A ∩ B) p

The Mayer–Vietoris sum-to-intersection map in Čech cohomology, Ȟ^p(A; R) ⊕ Ȟ^p(B; R) → Ȟ^p(A ∩ B; R), given by the difference of the restriction maps.

noncomputable def cechMV_connecting_aux (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (hyp : MayerVietorisHypothesis (↑X) A B) (p : ℕ) : FullyRelativeCapProduct.cechCohomology R X (A ∩ B) p ⟶ FullyRelativeCapProduct.cechCohomology R X (A ∪ B) (p + 1)

The Mayer–Vietoris connecting morphism in Čech cohomology, Ȟ^p(A ∩ B; R) → Ȟ^{p+1}(A ∪ B; R), witnessing the long exact sequence under the Mayer–Vietoris hypothesis.

theorem cechMV_exact_sum_aux (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (hyp : MayerVietorisHypothesis (↑X) A B) (p : ℕ) : Function.Exact ⇑(ModuleCat.Hom.hom (cechMV_unionToSum R X A B p)) ⇑(ModuleCat.Hom.hom (cechMV_sumToInter R X A B p))

Exactness at the sum Ȟ^p(A; R) ⊕ Ȟ^p(B; R) of the Čech Mayer–Vietoris sequence: the union-to-sum map and sum-to-intersection map are exact.

theorem cechMV_exact_inter_aux (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (hyp : MayerVietorisHypothesis (↑X) A B) (p : ℕ) : Function.Exact ⇑(ModuleCat.Hom.hom (cechMV_sumToInter R X A B p)) ⇑(ModuleCat.Hom.hom (cechMV_connecting_aux R X A B hyp p))

Exactness at the intersection Ȟ^p(A ∩ B; R) of the Čech Mayer–Vietoris sequence: the sum-to-intersection map and the connecting morphism are exact.

theorem cechMV_exact_union_aux (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (hyp : MayerVietorisHypothesis (↑X) A B) (p : ℕ) : Function.Exact ⇑(ModuleCat.Hom.hom (cechMV_connecting_aux R X A B hyp p)) ⇑(ModuleCat.Hom.hom (cechMV_unionToSum R X A B (p + 1)))

Exactness at the union Ȟ^{p+1}(A ∪ B; R) of the Čech Mayer–Vietoris sequence: the connecting morphism and the next union-to-sum map are exact.

noncomputable def cechMV_sequence_data (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (hyp : MayerVietorisHypothesis (↑X) A B) : { mv : CechMVSequence R X A B // (∀ (p : ℕ), mv.unionToSum p = cechMV_unionToSum R X A B p) ∧ ∀ (p : ℕ), mv.sumToInter p = cechMV_sumToInter R X A B p }

Packages the Čech Mayer–Vietoris sequence under the Mayer–Vietoris hypothesis, bundled with witnesses that the bundled union-to-sum and sum-to-intersection morphisms agree with cechMV_unionToSum and cechMV_sumToInter.

theorem cechMV_sequence_exact (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (hyp : MayerVietorisHypothesis (↑X) A B) (p : ℕ) : ∃ (δ : FullyRelativeCapProduct.cechCohomology R X (A ∩ B) p ⟶ FullyRelativeCapProduct.cechCohomology R X (A ∪ B) (p + 1)), Function.Exact ⇑(ModuleCat.Hom.hom (cechMV_unionToSum R X A B p)) ⇑(ModuleCat.Hom.hom (cechMV_sumToInter R X A B p)) ∧ Function.Exact ⇑(ModuleCat.Hom.hom (cechMV_sumToInter R X A B p)) ⇑(ModuleCat.Hom.hom δ) ∧ Function.Exact ⇑(ModuleCat.Hom.hom δ) ⇑(ModuleCat.Hom.hom (cechMV_unionToSum R X A B (p + 1)))

Existence of a connecting morphism δ making the Čech Mayer–Vietoris sequence exact at all three positions, extracted from cechMV_sequence_data.

noncomputable def cechMV_connecting (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (hyp : MayerVietorisHypothesis (↑X) A B) (p : ℕ) : FullyRelativeCapProduct.cechCohomology R X (A ∩ B) p ⟶ FullyRelativeCapProduct.cechCohomology R X (A ∪ B) (p + 1)

The chosen Čech Mayer–Vietoris connecting morphism extracted from cechMV_sequence_exact.

theorem cechMV_exact_sum (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (hyp : MayerVietorisHypothesis (↑X) A B) (p : ℕ) : Function.Exact ⇑(ModuleCat.Hom.hom (cechMV_unionToSum R X A B p)) ⇑(ModuleCat.Hom.hom (cechMV_sumToInter R X A B p))

Exactness of the Čech Mayer–Vietoris sequence at the sum position.

theorem cechMV_exact_inter (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (hyp : MayerVietorisHypothesis (↑X) A B) (p : ℕ) : Function.Exact ⇑(ModuleCat.Hom.hom (cechMV_sumToInter R X A B p)) ⇑(ModuleCat.Hom.hom (cechMV_connecting R X A B hyp p))

Exactness of the Čech Mayer–Vietoris sequence at the intersection position.

theorem cechMV_exact_union (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (hyp : MayerVietorisHypothesis (↑X) A B) (p : ℕ) : Function.Exact ⇑(ModuleCat.Hom.hom (cechMV_connecting R X A B hyp p)) ⇑(ModuleCat.Hom.hom (cechMV_unionToSum R X A B (p + 1)))

Exactness of the Čech Mayer–Vietoris sequence at the union position (after the connecting morphism).

noncomputable def cechMV_of_hyp (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (hyp : MayerVietorisHypothesis (↑X) A B) : CechMVSequence R X A B

The full Čech Mayer–Vietoris sequence as a CechMVSequence, packaging together the union-to-sum, sum-to-intersection, and connecting morphisms along with the three exactness statements.

noncomputable def singularMV_unionToSum (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (_hyp : MayerVietorisHypothesis (↑X) A B) (q : ℕ) : FullyRelativeCapProduct.relSingularHomology R X (A ∪ B)ᶜ q ⟶ FullyRelativeCapProduct.relSingularHomology R X Aᶜ q ⊞ FullyRelativeCapProduct.relSingularHomology R X Bᶜ q

The Mayer–Vietoris union-to-sum map in relative singular homology of the complements, H_q(X, (A ∪ B)ᶜ) → H_q(X, Aᶜ) ⊕ H_q(X, Bᶜ), given by pairing the two restriction maps.

noncomputable def singularMV_sumToInter (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (_hyp : MayerVietorisHypothesis (↑X) A B) (q : ℕ) : FullyRelativeCapProduct.relSingularHomology R X Aᶜ q ⊞ FullyRelativeCapProduct.relSingularHomology R X Bᶜ q ⟶ FullyRelativeCapProduct.relSingularHomology R X (A ∩ B)ᶜ q

The Mayer–Vietoris sum-to-intersection map in relative singular homology of the complements, H_q(X, Aᶜ) ⊕ H_q(X, Bᶜ) → H_q(X, (A ∩ B)ᶜ), given by the difference of the restriction maps.

noncomputable def singularMV_connecting (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (hyp : MayerVietorisHypothesis (↑X) A B) (q : ℕ) : FullyRelativeCapProduct.relSingularHomology R X (A ∩ B)ᶜ q ⟶ FullyRelativeCapProduct.relSingularHomology R X (A ∪ B)ᶜ (q - 1)

The Mayer–Vietoris connecting morphism in relative singular homology of the complements, H_q(X, (A ∩ B)ᶜ) → H_{q-1}(X, (A ∪ B)ᶜ), witnessing the long exact sequence under the Mayer–Vietoris hypothesis.

theorem singularMV_exact_sum (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (hyp : MayerVietorisHypothesis (↑X) A B) (q : ℕ) : Function.Exact ⇑(ModuleCat.Hom.hom (singularMV_unionToSum R X A B hyp q)) ⇑(ModuleCat.Hom.hom (singularMV_sumToInter R X A B hyp q))

Exactness at the sum H_q(X, Aᶜ) ⊕ H_q(X, Bᶜ) of the singular Mayer–Vietoris sequence.

theorem singularMV_exact_inter (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (hyp : MayerVietorisHypothesis (↑X) A B) (q : ℕ) : Function.Exact ⇑(ModuleCat.Hom.hom (singularMV_sumToInter R X A B hyp q)) ⇑(ModuleCat.Hom.hom (singularMV_connecting R X A B hyp q))

Exactness at the intersection H_q(X, (A ∩ B)ᶜ) of the singular Mayer–Vietoris sequence.

theorem singularMV_exact_union (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (hyp : MayerVietorisHypothesis (↑X) A B) (q : ℕ) : Function.Exact ⇑(ModuleCat.Hom.hom (singularMV_connecting R X A B hyp q)) ⇑(ModuleCat.Hom.hom (singularMV_unionToSum R X A B hyp (q - 1)))

Exactness at the union H_{q-1}(X, (A ∪ B)ᶜ) of the singular Mayer–Vietoris sequence (after the connecting morphism).

noncomputable def singularMV_of_hyp (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (hyp : MayerVietorisHypothesis (↑X) A B) : SingularMVSequence R X A B

The full singular Mayer–Vietoris sequence as a SingularMVSequence, packaging the union-to-sum, sum-to-intersection, and connecting morphisms together with the three exactness statements.

noncomputable def awCapAbsShortComplexMapS (R : Type) [CommRing R] (X : TopCat) (S : Set ↑X) (U : CechCohomology.OpenNeighborhoods S) (p q : ℕ) (α : CechCohomology.cechFamily R S p U) : HomologicalComplex.sc (FullyRelativeCapProduct.relSingChainCx R (TopCat.of ↑(↑U).carrier) (Subtype.val ⁻¹' Sᶜ)) (p + q) ⟶ HomologicalComplex.sc (FullyRelativeCapProduct.relSingChainCx R (TopCat.of ↑(↑U).carrier) (Subtype.val ⁻¹' Sᶜ)) q

The Alexander–Whitney cap product short-complex map at the level of relative singular chains on a neighbourhood U of S, modulo the chains on the complement Sᶜ, parametrized by a Čech class α.

theorem awCapAbsShortComplexMapS_add (R : Type) [CommRing R] (X : TopCat) (S : Set ↑X) (U : CechCohomology.OpenNeighborhoods S) (p q : ℕ) (α₁ α₂ : CechCohomology.cechFamily R S p U) : awCapAbsShortComplexMapS R X S U p q (α₁ + α₂) = awCapAbsShortComplexMapS R X S U p q α₁ + awCapAbsShortComplexMapS R X S U p q α₂

Additivity of awCapAbsShortComplexMapS in the Čech class α.

theorem awCapAbsShortComplexMapS_smul (R : Type) [CommRing R] (X : TopCat) (S : Set ↑X) (U : CechCohomology.OpenNeighborhoods S) (p q : ℕ) (r : R) (α : CechCohomology.cechFamily R S p U) : awCapAbsShortComplexMapS R X S U p q (r • α) = r • awCapAbsShortComplexMapS R X S U p q α

R-linearity of awCapAbsShortComplexMapS in the Čech class α.

noncomputable def awCapDescendsToHomologyAbs (R : Type) [CommRing R] (X : TopCat) (S : Set ↑X) (U : CechCohomology.OpenNeighborhoods S) (p q : ℕ) (α : CechCohomology.cechFamily R S p U) : ↑(FullyRelativeCapProduct.relSingularHomology R (TopCat.of ↑(↑U).carrier) (Subtype.val ⁻¹' Sᶜ) (p + q)) →ₗ[R] ↑(FullyRelativeCapProduct.relSingularHomology R (TopCat.of ↑(↑U).carrier) (Subtype.val ⁻¹' Sᶜ) q)

Passage of awCapAbsShortComplexMapS to relative singular homology of the neighbourhood: gives an R-linear map H_{p+q}(U, Sᶜ ∩ U) → H_q(U, Sᶜ ∩ U) parametrized by the Čech class.

theorem awCapDescendsToHomologyAbs_add (R : Type) [CommRing R] (X : TopCat) (S : Set ↑X) (U : CechCohomology.OpenNeighborhoods S) (p q : ℕ) (α₁ α₂ : CechCohomology.cechFamily R S p U) (c : ↑(FullyRelativeCapProduct.relSingularHomology R (TopCat.of ↑(↑U).carrier) (Subtype.val ⁻¹' Sᶜ) (p + q))) : (awCapDescendsToHomologyAbs R X S U p q (α₁ + α₂)) c = (awCapDescendsToHomologyAbs R X S U p q α₁) c + (awCapDescendsToHomologyAbs R X S U p q α₂) c

Additivity of awCapDescendsToHomologyAbs in the Čech class α.

theorem awCapDescendsToHomologyAbs_smul (R : Type) [CommRing R] (X : TopCat) (S : Set ↑X) (U : CechCohomology.OpenNeighborhoods S) (p q : ℕ) (r : R) (α : CechCohomology.cechFamily R S p U) (c : ↑(FullyRelativeCapProduct.relSingularHomology R (TopCat.of ↑(↑U).carrier) (Subtype.val ⁻¹' Sᶜ) (p + q))) : (awCapDescendsToHomologyAbs R X S U p q (r • α)) c = r • (awCapDescendsToHomologyAbs R X S U p q α) c

R-linearity of awCapDescendsToHomologyAbs in the Čech class α.

noncomputable def absCapOnNbhdHomol (R : Type) [CommRing R] (X : TopCat) (S : Set ↑X) (U : CechCohomology.OpenNeighborhoods S) (p q : ℕ) : CechCohomology.cechFamily R S p U →ₗ[R] ↑(FullyRelativeCapProduct.relSingularHomology R (TopCat.of ↑(↑U).carrier) (Subtype.val ⁻¹' Sᶜ) (p + q)) →ₗ[R] ↑(FullyRelativeCapProduct.relSingularHomology R (TopCat.of ↑(↑U).carrier) (Subtype.val ⁻¹' Sᶜ) q)

The cap product on relative singular homology of a neighbourhood U of S, packaged as an R-linear map from the Čech family to the space of linear maps H_{p+q}(U, Sᶜ ∩ U) → H_q(U, Sᶜ ∩ U).

noncomputable def inclusionForwardHomol (R : Type) [CommRing R] (X : TopCat) (S : Set ↑X) (U : CechCohomology.OpenNeighborhoods S) (q : ℕ) : ↑(FullyRelativeCapProduct.relSingularHomology R (TopCat.of ↑(↑U).carrier) (Subtype.val ⁻¹' Sᶜ) q) →ₗ[R] ↑(FullyRelativeCapProduct.relSingularHomology R X Sᶜ q)

The map induced on relative singular homology by the inclusion of a neighbourhood U of S into X: H_q(U, Sᶜ ∩ U) → H_q(X, Sᶜ).

noncomputable def absNbhdHomologyInclusion (R : Type) [CommRing R] (X : TopCat) (S : Set ↑X) (U₁ U₂ : CechCohomology.OpenNeighborhoods S) (_h : U₁ ≤ U₂) (n : ℕ) : ↑(FullyRelativeCapProduct.relSingularHomology R (TopCat.of ↑(↑U₂).carrier) (Subtype.val ⁻¹' Sᶜ) n) →ₗ[R] ↑(FullyRelativeCapProduct.relSingularHomology R (TopCat.of ↑(↑U₁).carrier) (Subtype.val ⁻¹' Sᶜ) n)

The transition map on relative singular homology between two neighbourhoods U₁ ≤ U₂ of S, obtained as the composition of the inclusion-induced map U₂ → X with the inverse of the excision isomorphism for U₁.

theorem absNbhdExcisionInverseHomol_compatible (R : Type) [CommRing R] (X : TopCat) (S : Set ↑X) (U₁ U₂ : CechCohomology.OpenNeighborhoods S) (h : U₁ ≤ U₂) (n : ℕ) (y : ↑(FullyRelativeCapProduct.relSingularHomology R X Sᶜ n)) : (FullyRelativeCapProduct.excisionInverseHomol R X S ↑U₁ ⋯ n) y = (absNbhdHomologyInclusion R X S U₁ U₂ h n) ((FullyRelativeCapProduct.excisionInverseHomol R X S ↑U₂ ⋯ n) y)

Compatibility of the excision inverse isomorphisms across two neighbourhoods U₁ ≤ U₂: factoring the inverse for U₁ through U₂ via absNbhdHomologyInclusion.

theorem absCapOnNbhdHomol_naturality (R : Type) [CommRing R] (X : TopCat) (S : Set ↑X) (U₁ U₂ : CechCohomology.OpenNeighborhoods S) (h : U₁ ≤ U₂) (p q : ℕ) (x : CechCohomology.cechFamily R S p U₁) (z : ↑(FullyRelativeCapProduct.relSingularHomology R (TopCat.of ↑(↑U₂).carrier) (Subtype.val ⁻¹' Sᶜ) (p + q))) : (absNbhdHomologyInclusion R X S U₁ U₂ h q) (((absCapOnNbhdHomol R X S U₂ p q) ((CechCohomology.cechTransition R S p U₁ U₂ h) x)) z) = ((absCapOnNbhdHomol R X S U₁ p q) x) ((absNbhdHomologyInclusion R X S U₁ U₂ h (p + q)) z)

Naturality of absCapOnNbhdHomol along the Čech transition maps and the neighbourhood inclusion: needed to descend the cap product on neighbourhood homology to the Čech direct limit.

theorem absNbhdInclusionForwardHomol_compatible (R : Type) [CommRing R] (X : TopCat) (S : Set ↑X) (U₁ U₂ : CechCohomology.OpenNeighborhoods S) (h : U₁ ≤ U₂) (q : ℕ) (w : ↑(FullyRelativeCapProduct.relSingularHomology R (TopCat.of ↑(↑U₂).carrier) (Subtype.val ⁻¹' Sᶜ) q)) : (inclusionForwardHomol R X S U₂ q) w = (inclusionForwardHomol R X S U₁ q) ((absNbhdHomologyInclusion R X S U₁ U₂ h q) w)

Compatibility of inclusionForwardHomol across two neighbourhoods U₁ ≤ U₂: the inclusion-induced map for U₂ factors through absNbhdHomologyInclusion followed by the inclusion-induced map for U₁.

theorem absNbhdCapRung_composite_naturality (R : Type) [CommRing R] (X : TopCat) (S : Set ↑X) (p q : ℕ) (U₁ U₂ : CechCohomology.OpenNeighborhoods S) (h : U₁ ≤ U₂) (x : CechCohomology.cechFamily R S p U₁) (y : ↑(FullyRelativeCapProduct.relSingularHomology R X Sᶜ (p + q))) : (inclusionForwardHomol R X S U₂ q) (((absCapOnNbhdHomol R X S U₂ p q) ((CechCohomology.cechTransition R S p U₁ U₂ h) x)) ((FullyRelativeCapProduct.excisionInverseHomol R X S ↑U₂ ⋯ (p + q)) y)) = (inclusionForwardHomol R X S U₁ q) (((absCapOnNbhdHomol R X S U₁ p q) x) ((FullyRelativeCapProduct.excisionInverseHomol R X S ↑U₁ ⋯ (p + q)) y))

Naturality of the composite "inclusion-cap-excise" cap rung across two neighbourhoods U₁ ≤ U₂, combining the three naturality lemmas above. Used to descend the cap rung to the Čech direct limit.

noncomputable def absNbhdCapRung (R : Type) [CommRing R] (X : TopCat) (S : Set ↑X) (n p q : ℕ) (hpq : p + q = n) (x_S : ↑(FullyRelativeCapProduct.relSingularHomology R X Sᶜ n)) (U : CechCohomology.OpenNeighborhoods S) : CechCohomology.cechFamily R S p U →ₗ[R] ↑(FullyRelativeCapProduct.relSingularHomology R X Sᶜ q)

The neighbourhood-level cap product "rung" at a fixed class x_S ∈ H_n(X, Sᶜ): pulled back via excision to the neighbourhood U, capped with a Čech p-cocycle, and pushed forward to X, yielding a linear map Ȟ-family(U, S, p) → H_q(X, Sᶜ) (p + q = n).

theorem absNbhdCapRung_compatible (R : Type) [CommRing R] (X : TopCat) (S : Set ↑X) (n p q : ℕ) (hpq : p + q = n) (x_S : ↑(FullyRelativeCapProduct.relSingularHomology R X Sᶜ n)) (U₁ U₂ : CechCohomology.OpenNeighborhoods S) (h : U₁ ≤ U₂) (x : CechCohomology.cechFamily R S p U₁) : (absNbhdCapRung R X S n p q hpq x_S U₂) ((CechCohomology.cechTransition R S p U₁ U₂ h) x) = (absNbhdCapRung R X S n p q hpq x_S U₁) x

Compatibility of absNbhdCapRung with Čech transition maps across two neighbourhoods U₁ ≤ U₂, used to descend the cap rung to the Čech direct limit Ȟ^p(S; R).

noncomputable def cechCapRung (R : Type) [CommRing R] (X : TopCat) (S : Set ↑X) (n p q : ℕ) (hpq : p + q = n) (x_S : ↑(FullyRelativeCapProduct.relSingularHomology R X Sᶜ n)) : FullyRelativeCapProduct.cechCohomology R X S p ⟶ FullyRelativeCapProduct.relSingularHomology R X Sᶜ q

The cap product "rung" Ȟ^p(S; R) → H_q(X, Sᶜ; R) at a fixed class x_S ∈ H_n(X, Sᶜ), obtained by descending the neighbourhood-level cap rung absNbhdCapRung along the Čech direct limit (p + q = n).

theorem cechCapRung_naturality (R : Type) [CommRing R] (X : TopCat) (K L : Set ↑X) (n p q : ℕ) (hpq : p + q = n) (x_K : ↑(FullyRelativeCapProduct.relSingularHomology R X Kᶜ n)) : CategoryTheory.CategoryStruct.comp (FullyRelativeCapProduct.cechCohomToSubspace R X K L p) (cechCapRung R X L n p q hpq ((ModuleCat.Hom.hom (FullyRelativeCapProduct.homolRestriction R X K L n)) x_K)) = CategoryTheory.CategoryStruct.comp (cechCapRung R X K n p q hpq x_K) (FullyRelativeCapProduct.homolRestriction R X K L q)

Naturality of cechCapRung along an inclusion L ⊆ K of closed subsets: capping with the restricted class on L agrees with capping on K and then restricting the resulting homology class.

theorem cechCapRung_naturality_connecting (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (hyp : MayerVietorisHypothesis (↑X) A B) (n p q : ℕ) (hpq : p + q = n) (hpq' : p + 1 + (q - 1) = n) (x_union : ↑(FullyRelativeCapProduct.relSingularHomology R X (A ∪ B)ᶜ n)) : CategoryTheory.CategoryStruct.comp (cechMV_connecting R X A B hyp p) (cechCapRung R X (A ∪ B) n (p + 1) (q - 1) hpq' ((ModuleCat.Hom.hom (FullyRelativeCapProduct.homolRestriction R X (A ∪ B) (A ∪ B) n)) x_union)) = CategoryTheory.CategoryStruct.comp (cechCapRung R X (A ∩ B) n p q hpq ((ModuleCat.Hom.hom (FullyRelativeCapProduct.homolRestriction R X (A ∪ B) (A ∩ B) n)) x_union)) (singularMV_connecting R X A B hyp q)

Compatibility of cechCapRung with the Mayer–Vietoris connecting morphisms: the Čech coboundary Ȟ^p(A ∩ B) → Ȟ^{p+1}(A ∪ B) followed by capping with x_{A ∪ B} equals capping with x_{A ∩ B} followed by the singular connecting morphism.

theorem cechCapRung_naturality_unionToSum (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (hyp : MayerVietorisHypothesis (↑X) A B) (n p q : ℕ) (hpq : p + q = n) (x_union : ↑(FullyRelativeCapProduct.relSingularHomology R X (A ∪ B)ᶜ n)) : CategoryTheory.CategoryStruct.comp (cechCapRung R X (A ∪ B) n p q hpq ((ModuleCat.Hom.hom (FullyRelativeCapProduct.homolRestriction R X (A ∪ B) (A ∪ B) n)) x_union)) (singularMV_unionToSum R X A B hyp q) = CategoryTheory.CategoryStruct.comp (cechMV_unionToSum R X A B p) (CategoryTheory.Limits.biprod.map (cechCapRung R X A n p q hpq ((ModuleCat.Hom.hom (FullyRelativeCapProduct.homolRestriction R X (A ∪ B) A n)) x_union)) (cechCapRung R X B n p q hpq ((ModuleCat.Hom.hom (FullyRelativeCapProduct.homolRestriction R X (A ∪ B) B n)) x_union)))

Compatibility of cechCapRung with the Mayer–Vietoris union-to-sum maps: capping on A ∪ B followed by the singular union-to-sum map equals the Čech union-to-sum map followed by separately capping on A and B.

theorem cechCapRung_naturality_sumToInter (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (hyp : MayerVietorisHypothesis (↑X) A B) (n p q : ℕ) (hpq : p + q = n) (x_union : ↑(FullyRelativeCapProduct.relSingularHomology R X (A ∪ B)ᶜ n)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (cechCapRung R X A n p q hpq ((ModuleCat.Hom.hom (FullyRelativeCapProduct.homolRestriction R X (A ∪ B) A n)) x_union)) (cechCapRung R X B n p q hpq ((ModuleCat.Hom.hom (FullyRelativeCapProduct.homolRestriction R X (A ∪ B) B n)) x_union))) (singularMV_sumToInter R X A B hyp q) = CategoryTheory.CategoryStruct.comp (cechMV_sumToInter R X A B p) (cechCapRung R X (A ∩ B) n p q hpq ((ModuleCat.Hom.hom (FullyRelativeCapProduct.homolRestriction R X (A ∪ B) (A ∩ B) n)) x_union))

Compatibility of cechCapRung with the Mayer–Vietoris sum-to-intersection maps: separately capping on A, B followed by the singular sum-to-intersection map equals the Čech sum-to-intersection map followed by capping on A ∩ B.

theorem mvCapProduct_comm_sq1 (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (n : ℕ) (x_union : ↑(FullyRelativeCapProduct.relSingularHomology R X (A ∪ B)ᶜ n)) (hyp : MayerVietorisHypothesis (↑X) A B) (p q : ℕ) (hpq : p + q = n) : CategoryTheory.CategoryStruct.comp (cechCapRung R X (A ∪ B) n p q hpq ((ModuleCat.Hom.hom (FullyRelativeCapProduct.homolRestriction R X (A ∪ B) (A ∪ B) n)) x_union)) ((singularMV_of_hyp R X A B hyp).unionToSum q) = CategoryTheory.CategoryStruct.comp ((cechMV_of_hyp R X A B hyp).unionToSum p) (CategoryTheory.Limits.biprod.map (cechCapRung R X A n p q hpq ((ModuleCat.Hom.hom (FullyRelativeCapProduct.homolRestriction R X (A ∪ B) A n)) x_union)) (cechCapRung R X B n p q hpq ((ModuleCat.Hom.hom (FullyRelativeCapProduct.homolRestriction R X (A ∪ B) B n)) x_union)))

First commutative square of the Mayer–Vietoris cap-product ladder: cap on A ∪ B followed by the singular union-to-sum equals the Čech union-to-sum followed by the cap on A and B. Bundled form of cechCapRung_naturality_unionToSum.

theorem mvCapProduct_comm_sq2 (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (n : ℕ) (x_union : ↑(FullyRelativeCapProduct.relSingularHomology R X (A ∪ B)ᶜ n)) (hyp : MayerVietorisHypothesis (↑X) A B) (p q : ℕ) (hpq : p + q = n) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (cechCapRung R X A n p q hpq ((ModuleCat.Hom.hom (FullyRelativeCapProduct.homolRestriction R X (A ∪ B) A n)) x_union)) (cechCapRung R X B n p q hpq ((ModuleCat.Hom.hom (FullyRelativeCapProduct.homolRestriction R X (A ∪ B) B n)) x_union))) ((singularMV_of_hyp R X A B hyp).sumToInter q) = CategoryTheory.CategoryStruct.comp ((cechMV_of_hyp R X A B hyp).sumToInter p) (cechCapRung R X (A ∩ B) n p q hpq ((ModuleCat.Hom.hom (FullyRelativeCapProduct.homolRestriction R X (A ∪ B) (A ∩ B) n)) x_union))

Second commutative square of the Mayer–Vietoris cap-product ladder: cap on A and B followed by the singular sum-to-intersection equals the Čech sum-to-intersection followed by the cap on A ∩ B. Bundled form of cechCapRung_naturality_sumToInter.

theorem mvCapProduct_comm_sq3 (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (n : ℕ) (x_union : ↑(FullyRelativeCapProduct.relSingularHomology R X (A ∪ B)ᶜ n)) (hyp : MayerVietorisHypothesis (↑X) A B) (p q : ℕ) (hpq : p + q = n) (hpq' : p + 1 + (q - 1) = n) : CategoryTheory.CategoryStruct.comp ((cechMV_of_hyp R X A B hyp).connecting p) (cechCapRung R X (A ∪ B) n (p + 1) (q - 1) hpq' ((ModuleCat.Hom.hom (FullyRelativeCapProduct.homolRestriction R X (A ∪ B) (A ∪ B) n)) x_union)) = CategoryTheory.CategoryStruct.comp (cechCapRung R X (A ∩ B) n p q hpq ((ModuleCat.Hom.hom (FullyRelativeCapProduct.homolRestriction R X (A ∪ B) (A ∩ B) n)) x_union)) ((singularMV_of_hyp R X A B hyp).connecting q)

Third commutative square of the Mayer–Vietoris cap-product ladder: the Čech connecting morphism followed by capping on A ∪ B equals capping on A ∩ B followed by the singular connecting morphism. Bundled form of cechCapRung_naturality_connecting.

noncomputable def mvCapProduct_of_hyp (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (n : ℕ) (hyp : MayerVietorisHypothesis (↑X) A B) (x_union : ↑(FullyRelativeCapProduct.relSingularHomology R X (A ∪ B)ᶜ n)) : MVCapProductData R X A B n x_union (cechMV_of_hyp R X A B hyp) (singularMV_of_hyp R X A B hyp)

Assembles the MVCapProductData connecting the Čech and singular Mayer–Vietoris sequences at a fixed class x_union ∈ H_n(X, (A ∪ B)ᶜ): cap rungs for each subset and the three compatibility squares.

noncomputable def cechSingular_mayerVietoris_ladder (R : Type) [CommRing R] (X : TopCat) (A B : Set ↑X) (n : ℕ) (hyp : MayerVietorisHypothesis (↑X) A B) (x_union : ↑(FullyRelativeCapProduct.relSingularHomology R X (A ∪ B)ᶜ n)) : MayerVietorisLadder R X A B n x_union

Theorem 36.2. Let A, B be closed in a normal space or compact in a Hausdorff space X. Then for any class x_{A ∪ B} ∈ H_n(X, X - (A ∪ B)) there is a commutative ladder of Mayer–Vietoris sequences connecting the Čech cohomology Mayer–Vietoris sequence of A, B, A ∪ B, A ∩ B to the singular homology Mayer–Vietoris sequence of their complements, in which the classes x_A, x_B, x_{A ∩ B} arise as restrictions of x_{A ∪ B} and the cap-product rungs are indexed by subsets S ∈ {A, B, A ∪ B, A ∩ B} and (p, q) with p + q = n. Packaged as a MayerVietorisLadder.