Mayer Vietoris SES

def SphereOddDegree.twoSetCover {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) : OpenCoverData X

The open-cover data supplied by two open sets whose union is the whole space.

Equations

• SphereOddDegree.twoSetCover U V hUV = { sets := {↑U, ↑V}, isOpen_mem := ⋯, covers := ⋯ }

theorem SphereOddDegree.twoSetCover_memU {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) : ↑U ∈ (twoSetCover U V hUV).sets

theorem SphereOddDegree.twoSetCover_memV {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) : ↑V ∈ (twoSetCover U V hUV).sets

noncomputable def SphereOddDegree.twoOpenCoverSmallChains (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) : ChainComplex (ModuleCat R) ℕ

The chain complex generated by simplices small for the two-set open cover.

Equations

• SphereOddDegree.twoOpenCoverSmallChains R U V hUV = SphereOddDegree.smallChainComplex R X (SphereOddDegree.twoSetCover U V hUV)

noncomputable def SphereOddDegree.mvInclUVU (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) : subChainComplex R X (↑U ∩ ↑V) ⟶ subChainComplex R X ↑U

Include chains supported in the intersection into chains supported in the first open set.

Equations

• SphereOddDegree.mvInclUVU R U V = SphereOddDegree.subChainInclusion (↑U ∩ ↑V) ↑U ⋯

noncomputable def SphereOddDegree.mvInclUVV (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) : subChainComplex R X (↑U ∩ ↑V) ⟶ subChainComplex R X ↑V

Include chains supported in the intersection into chains supported in the second open set.

Equations

• SphereOddDegree.mvInclUVV R U V = SphereOddDegree.subChainInclusion (↑U ∩ ↑V) ↑V ⋯

noncomputable def SphereOddDegree.mvInclUSmall (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) : subChainComplex R X ↑U ⟶ twoOpenCoverSmallChains R U V hUV

Include chains supported in the first open set into the small-chain complex of the cover.

Equations

• SphereOddDegree.mvInclUSmall R U V hUV = SphereOddDegree.subChainToSmall (SphereOddDegree.twoSetCover U V hUV) ↑U ⋯

noncomputable def SphereOddDegree.mvInclVSmall (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) : subChainComplex R X ↑V ⟶ twoOpenCoverSmallChains R U V hUV

Include chains supported in the second open set into the small-chain complex of the cover.

Equations

• SphereOddDegree.mvInclVSmall R U V hUV = SphereOddDegree.subChainToSmall (SphereOddDegree.twoSetCover U V hUV) ↑V ⋯

theorem SphereOddDegree.mvIncl_comp_eq (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) : CategoryTheory.CategoryStruct.comp (mvInclUVU R U V) (mvInclUSmall R U V hUV) = CategoryTheory.CategoryStruct.comp (mvInclUVV R U V) (mvInclVSmall R U V hUV)

noncomputable def SphereOddDegree.mvLeftChainMap (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) : subChainComplex R X (↑U ∩ ↑V) ⟶ subChainComplex R X ↑U ⊞ subChainComplex R X ↑V

The signed pair of inclusions from the intersection into the two open sets.

Equations

• SphereOddDegree.mvLeftChainMap R U V = CategoryTheory.Limits.biprod.lift (SphereOddDegree.mvInclUVU R U V) (-SphereOddDegree.mvInclUVV R U V)

noncomputable def SphereOddDegree.mvRightChainMap (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) : subChainComplex R X ↑U ⊞ subChainComplex R X ↑V ⟶ twoOpenCoverSmallChains R U V hUV

Add the two inclusions into the small-chain complex of the cover.

Equations

• SphereOddDegree.mvRightChainMap R U V hUV = CategoryTheory.Limits.biprod.desc (SphereOddDegree.mvInclUSmall R U V hUV) (SphereOddDegree.mvInclVSmall R U V hUV)

theorem SphereOddDegree.mvLeft_comp_mvRight (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) : CategoryTheory.CategoryStruct.comp (mvLeftChainMap R U V) (mvRightChainMap R U V hUV) = 0

noncomputable def SphereOddDegree.mvShortComplex (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) : CategoryTheory.ShortComplex (ChainComplex (ModuleCat R) ℕ)

The Mayer–Vietoris short complex of intersection, component, and small chains.

Equations

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

def SphereOddDegree.IsSubVnotU {X : TopCat} (U V : TopologicalSpace.Opens ↑X) {n : ℕ} (σ : singularSimplices X n) : Prop

A simplex lies in the second open set but is not subordinate to the first.

Equations

• SphereOddDegree.IsSubVnotU U V σ = (SphereOddDegree.IsSubordinate (↑V) σ ∧ ¬SphereOddDegree.IsSubordinate (↑U) σ)

theorem SphereOddDegree.keepHom_small_mem_U (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) (k : ℕ) (c : ↑(AffineBarycentricSubdivision.singularChainGroup R X k)) (hc : c ∈ smallChainSubmodule R X (twoSetCover U V hUV) k) : (ModuleCat.Hom.hom (keepHom R X (IsSubordinate ↑U))) c ∈ subChainSubmodule R X (↑U) k

theorem SphereOddDegree.keepHom_small_mem_V (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) (k : ℕ) (c : ↑(AffineBarycentricSubdivision.singularChainGroup R X k)) (hc : c ∈ smallChainSubmodule R X (twoSetCover U V hUV) k) : (ModuleCat.Hom.hom (keepHom R X (IsSubVnotU U V))) c ∈ subChainSubmodule R X (↑V) k

theorem SphereOddDegree.keepHom_split_small (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) (k : ℕ) (c : ↑(AffineBarycentricSubdivision.singularChainGroup R X k)) (hc : c ∈ smallChainSubmodule R X (twoSetCover U V hUV) k) : (ModuleCat.Hom.hom (keepHom R X (IsSubordinate ↑U))) c + (ModuleCat.Hom.hom (keepHom R X (IsSubVnotU U V))) c = c

theorem SphereOddDegree.keepHom_V_mem_UV (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (k : ℕ) (c : ↑(AffineBarycentricSubdivision.singularChainGroup R X k)) (hc : c ∈ subChainSubmodule R X (↑V) k) : (ModuleCat.Hom.hom (keepHom R X (IsSubordinate ↑U))) c ∈ subChainSubmodule R X (↑U ∩ ↑V) k

noncomputable def SphereOddDegree.restrictKeep (R : Type) [CommRing R] {X : TopCat} {n : ℕ} (P : singularSimplices X n → Prop) [DecidablePred P] (p q : Submodule R ↑(AffineBarycentricSubdivision.singularChainGroup R X n)) (hmaps : ∀ c ∈ p, (ModuleCat.Hom.hom (keepHom R X P)) c ∈ q) : ↧↥p ⟶ ↧↥q

Restrict a generator-retaining projection to specified source and target submodules.

Equations

• SphereOddDegree.restrictKeep R P p q hmaps = ModuleCat.ofHom (LinearMap.codRestrict q (ModuleCat.Hom.hom (SphereOddDegree.keepHom R X P) ∘ₗ p.subtype) ⋯)

@[simp]

theorem SphereOddDegree.restrictKeep_val (R : Type) [CommRing R] {X : TopCat} {n : ℕ} (P : singularSimplices X n → Prop) [DecidablePred P] (p q : Submodule R ↑(AffineBarycentricSubdivision.singularChainGroup R X n)) (hmaps : ∀ c ∈ p, (ModuleCat.Hom.hom (keepHom R X P)) c ∈ q) (c : ↥p) : ↑((ModuleCat.Hom.hom (restrictKeep R P p q hmaps)) c) = (ModuleCat.Hom.hom (keepHom R X P)) ↑c

noncomputable def SphereOddDegree.routeU (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) (k : ℕ) : (twoOpenCoverSmallChains R U V hUV).X k ⟶ (subChainComplex R X ↑U).X k

Route the simplices subordinate to the first open set into its chain group.

Equations

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

noncomputable def SphereOddDegree.routeV (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) (k : ℕ) : (twoOpenCoverSmallChains R U V hUV).X k ⟶ (subChainComplex R X ↑V).X k

Route the remaining simplices of the two-set cover into the second open set.

Equations

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

noncomputable def SphereOddDegree.projVtoUV (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (k : ℕ) : (subChainComplex R X ↑V).X k ⟶ (subChainComplex R X (↑U ∩ ↑V)).X k

Retain the simplices of the second open set that also lie in the first.

Equations

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

theorem SphereOddDegree.keepHom_PV_eq_zero_of_mem_U (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (k : ℕ) (c : ↑(AffineBarycentricSubdivision.singularChainGroup R X k)) (hc : c ∈ subChainSubmodule R X (↑U) k) : (ModuleCat.Hom.hom (keepHom R X (IsSubVnotU U V))) c = 0

theorem SphereOddDegree.mvInclU_small_comp_routeU (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) (k : ℕ) : CategoryTheory.CategoryStruct.comp ((mvInclUSmall R U V hUV).f k) (routeU R U V hUV k) = CategoryTheory.CategoryStruct.id ((subChainComplex R X ↑U).X k)

theorem SphereOddDegree.mvInclU_small_comp_routeV (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) (k : ℕ) : CategoryTheory.CategoryStruct.comp ((mvInclUSmall R U V hUV).f k) (routeV R U V hUV k) = 0

theorem SphereOddDegree.mvInclV_small_comp_routeU (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) (k : ℕ) : CategoryTheory.CategoryStruct.comp ((mvInclVSmall R U V hUV).f k) (routeU R U V hUV k) = CategoryTheory.CategoryStruct.comp (projVtoUV R U V k) ((mvInclUVU R U V).f k)

theorem SphereOddDegree.keepHom_split_subV (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) (k : ℕ) (c : ↑(AffineBarycentricSubdivision.singularChainGroup R X k)) (hc : c ∈ subChainSubmodule R X (↑V) k) : (ModuleCat.Hom.hom (keepHom R X (IsSubordinate ↑U))) c + (ModuleCat.Hom.hom (keepHom R X (IsSubVnotU U V))) c = c

theorem SphereOddDegree.mvInclUV_V_comp_projVtoUV (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (k : ℕ) : CategoryTheory.CategoryStruct.comp ((mvInclUVV R U V).f k) (projVtoUV R U V k) = CategoryTheory.CategoryStruct.id ((subChainComplex R X (↑U ∩ ↑V)).X k)

theorem SphereOddDegree.projVtoUV_inclUV_V_add_inclV_routeV (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) (k : ℕ) : CategoryTheory.CategoryStruct.comp (projVtoUV R U V k) ((mvInclUVV R U V).f k) + CategoryTheory.CategoryStruct.comp ((mvInclVSmall R U V hUV).f k) (routeV R U V hUV k) = CategoryTheory.CategoryStruct.id ((subChainComplex R X ↑V).X k)

@[reducible, inline]

noncomputable abbrev SphereOddDegree.mvSplitSC (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) (k : ℕ) : CategoryTheory.ShortComplex (ModuleCat R)

The degreewise module short complex underlying the Mayer–Vietoris construction.

Equations

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

noncomputable def SphereOddDegree.mvSplitting (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) (k : ℕ) : (mvSplitSC R U V hUV k).Splitting

The degreewise splitting obtained by routing each simplex to one open set.

Equations

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

theorem SphereOddDegree.biprodXIso_lift_f (R : Type) [CommRing R] {K L M : ChainComplex (ModuleCat R) ℕ} (a : K ⟶ L) (b : K ⟶ M) (k : ℕ) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.biprod.lift a b).f k) (HomologicalComplex.biprodXIso L M k).hom = CategoryTheory.Limits.biprod.lift (a.f k) (b.f k)

theorem SphereOddDegree.biprodXIso_desc_f (R : Type) [CommRing R] {K L M : ChainComplex (ModuleCat R) ℕ} (a : L ⟶ K) (b : M ⟶ K) (k : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.biprodXIso L M k).hom (CategoryTheory.Limits.biprod.desc (a.f k) (b.f k)) = (CategoryTheory.Limits.biprod.desc a b).f k

noncomputable def SphereOddDegree.mvEvalIso (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) (k : ℕ) : (HomologicalComplex.eval (ModuleCat R) (ComplexShape.down ℕ) k).mapShortComplex.obj (mvShortComplex R U V hUV) ≅ mvSplitSC R U V hUV k

Identify evaluation of the chain short complex with its explicit degreewise form.

Equations

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

theorem SphereOddDegree.mvShortComplex_degreewise_shortExact (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) (k : ℕ) : ((HomologicalComplex.eval (ModuleCat R) (ComplexShape.down ℕ) k).mapShortComplex.obj (mvShortComplex R U V hUV)).ShortExact

theorem SphereOddDegree.mvShortComplex_shortExact (R : Type) [CommRing R] {X : TopCat} (U V : TopologicalSpace.Opens ↑X) (hUV : U ⊔ V = ⊤) : (mvShortComplex R U V hUV).ShortExact