Documentation

TauCeti.AlgebraicTopology.Cohomology.Excision

Excision for relative singular cohomology #

Let (X, B) be a topological pair and A ⊆ X a subset such that the interiors of A and B cover X. The inclusion of pairs (A, A ∩ B) ⟶ (X, B) induces an isomorphism Hⁿ(X, B; R, M) ⟶ Hⁿ(A, A ∩ B; R, M) on relative singular cohomology in every degree, for coefficients R and M in any linear abelian category with coproducts (TopPair.isIso_singularCohomologyMap_excisionMap). Equivalently, excising a set Z whose closure lies in the interior of B does not change relative cohomology (TopPair.isIso_singularCohomologyMap_excisionMap_compl). In particular, for a closed set K and an open neighbourhood U of K, restriction Hⁿ(X, X ∖ K) ⟶ Hⁿ(U, U ∖ K) is an isomorphism (TopPair.isIso_singularCohomologyMap_excisionMap_of_isClosed_subset); this is the form in which cohomology with supports in a compact subset of a Hausdorff space, and hence Poincaré duality, is localised.

All of these follow from the general statement TopPair.quasiIso_singularCochainComplexMap_of_open_cover: a map of topological pairs f : P ⟶ P' which is an embedding on ambient spaces, whose subspace is the full preimage of the subspace of P', and such that the ambient space of P' has an open cover each of whose members lies in the subspace of P' or in the image of f, induces a quasi-isomorphism of relative singular cochain complexes.

The proof dualizes the one for homology in TauCeti.AlgebraicTopology.Singular.Excision, but works with chain homotopy equivalences rather than quasi-isomorphisms, since Hom(-, M) need not preserve quasi-isomorphisms. The inclusion of the chains subordinate to an open cover is a chain homotopy equivalence (TauCeti.smallSingularChainHomotopyEquiv), so restricting cochains to them is a quasi-isomorphism (TauCeti.quasiIso_cochainComplexMap_smallSingularSubcomplex_ι), and this passes to restricted pairs (TopPair.quasiIso_cochainComplexMap_restrictι_smallSingularSubcomplex) by the five lemma for the long exact sequences of the pairs. On the restricted pairs the map induced by f bijects the complementary simplices (TopPair.relativeSimplex_restrictMap_bijective), so it is an isomorphism of relative chain complexes, and hence of relative cochain complexes (SSetPair.isIso_cochainComplexMap_of_relativeSimplex_equiv).

Naturality of the excision isomorphisms in the excision data follows by applying TopPair.singularCohomologyMap to TopPair.interPairMap_comp_excisionMap, and compatibility with the connecting morphism of the pair is TopPair.singularCohomologyδ_naturality applied to the excision map.

References #

source
theorem TopPair.quasiIso_cochainComplexMap_restrictι_smallSingularSubcomplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {ι : Type u_2} (P : TopPair) (U : ι → Set ↑fst) (hU : ∀ (i : ι), IsOpen (U i)) (hcov : ⋃ (i : ι), U i = Set.univ) :
QuasiIso (SSetPair.cochainComplexMap ((toSSetPair.obj P).restrictι (P.smallSingularSubcomplex U)))

The relative small-chain theorem for cochains. Restricting relative singular cochains of a topological pair to the simplices subordinate to an open cover of the ambient space is a quasi-isomorphism.

source
theorem TopPair.quasiIso_singularCochainComplexMap_of_open_cover {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {ι : Type u_2} {P P' : TopPair} (f : P ⟶ P') (hf : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (Hom.fst f))) (hsnd : ∀ (x : ↑fst), (CategoryTheory.ConcreteCategory.hom (Hom.fst f)) x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom map) → x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom map)) (U : ι → Set ↑fst) (hU : ∀ (i : ι), IsOpen (U i)) (hcov : ⋃ (i : ι), U i = Set.univ) (hUf : ∀ (i : ι), U i ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom map) ∨ U i ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (Hom.fst f))) :
QuasiIso (singularCochainComplexMap f)

Excision for relative singular cochains. Let f : P ⟶ P' be a map of topological pairs which is an embedding on ambient spaces and whose subspace is the full preimage of the subspace of P'. If the ambient space of P' has an open cover each of whose members lies in the subspace of P' or in the image of f, then f induces a quasi-isomorphism of relative singular cochain complexes.

source
theorem TopPair.isIso_singularCohomologyMap_of_open_cover {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {ι : Type u_2} {P P' : TopPair} (f : P ⟶ P') (hf : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (Hom.fst f))) (hsnd : ∀ (x : ↑fst), (CategoryTheory.ConcreteCategory.hom (Hom.fst f)) x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom map) → x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom map)) (U : ι → Set ↑fst) (hU : ∀ (i : ι), IsOpen (U i)) (hcov : ⋃ (i : ι), U i = Set.univ) (hUf : ∀ (i : ι), U i ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom map) ∨ U i ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (Hom.fst f))) (n : ℕ) :
CategoryTheory.IsIso (TopPair.singularCohomologyMap f n)

Excision for relative singular cohomology. Under the hypotheses of TopPair.quasiIso_singularCochainComplexMap_of_open_cover, the map of pairs f induces isomorphisms on relative singular cohomology.

source
theorem TopPair.isIso_singularCohomologyMap_excisionMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} (A B : Set ↑X) (h : interior A ∪ interior B = Set.univ) (n : ℕ) :
CategoryTheory.IsIso (TopPair.singularCohomologyMap (excisionMap A B) n)

Excision. If the interiors of A and B cover X, the inclusion of pairs (A, A ∩ B) ⟶ (X, B) induces isomorphisms Hⁿ(X, B) ⟶ Hⁿ(A, A ∩ B) on relative singular cohomology.

source
theorem TopPair.isIso_singularCohomologyMap_excisionMap_compl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} (B Z : Set ↑X) (h : closure Z ⊆ interior B) (n : ℕ) :
CategoryTheory.IsIso (TopPair.singularCohomologyMap (excisionMap Zᶜ B) n)

Excision of a set with closure in the interior of the subspace. If closure Z ⊆ interior B, the inclusion of pairs (X ∖ Z, B ∖ Z) ⟶ (X, B) induces isomorphisms Hⁿ(X, B) ⟶ Hⁿ(X ∖ Z, B ∖ Z) on relative singular cohomology.

source
theorem TopPair.isIso_singularCohomologyMap_excisionMap_of_isClosed_subset {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {U K : Set ↑X} (hU : IsOpen U) (hK : IsClosed K) (hKU : K ⊆ U) (n : ℕ) :
CategoryTheory.IsIso (TopPair.singularCohomologyMap (excisionMap U Kᶜ) n)

Excision onto a neighbourhood. If U is open and contains the closed set K, the inclusion of pairs (U, U ∖ K) ⟶ (X, X ∖ K) induces isomorphisms Hⁿ(X, X ∖ K) ⟶ Hⁿ(U, U ∖ K) on relative singular cohomology.

source
theorem TopPair.isIso_singularCohomologyMap_ofSubsetMap_compl_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) {X : TopCat} {U L₁ L₂ : Set ↑X} (hU : IsOpen U) (hL₁ : IsClosed L₁) (hL₂ : IsClosed L₂) (hL₁U : L₁ ⊆ U) (h : L₂ ⊆ L₁) (n : ℕ) :
CategoryTheory.IsIso (TopPair.singularCohomologyMap (ofSubsetMap (CategoryTheory.CategoryStruct.id ↧↑U) ⋯) n) ↔ CategoryTheory.IsIso (TopPair.singularCohomologyMap (ofSubsetMap (CategoryTheory.CategoryStruct.id X) ⋯) n)

Excision is compatible with shrinking the excised set. Let U be open and let L₂ ⊆ L₁ ⊆ U be closed. The restriction Hⁿ(U, U ∖ L₂) ⟶ Hⁿ(U, U ∖ L₁) is an isomorphism exactly when Hⁿ(X, X ∖ L₂) ⟶ Hⁿ(X, X ∖ L₁) is, since both pairs in U are identified with the corresponding pairs in X by excision.