def CechCohomology.IsCofinalMap {I : Type u_1} {J : Type u_2} [LE I] (φ : J → I) : Prop

A map φ : J → I between preorders is cofinal if every i : I is $\le$ some φ j. Used to recognise when pulling a directed system back along φ gives the same direct limit.

def CechCohomology.pullbackBondingMap {ι : Type u_1} [Preorder ι] {κ : Type u_2} [Preorder κ] (G : ι → Type u_3) [(i : ι) → AddCommGroup (G i)] (f : (i j : ι) → i ≤ j → G i →+ G j) (φ : κ →o ι) (j₁ j₂ : κ) (h : j₁ ≤ j₂) : G (φ j₁) →+ G (φ j₂)

Pullback of the bonding maps of a directed system (G, f) along a monotone map φ : κ →o ι: the pulled-back system has fibres G (φ j) and bonding maps f (φ j₁) (φ j₂) (φ.monotone h).

noncomputable def CechCohomology.cofinalMap {ι : Type u_1} [Preorder ι] [DecidableEq ι] {κ : Type u_2} [Preorder κ] [DecidableEq κ] (G : ι → Type u_3) [(i : ι) → AddCommGroup (G i)] (f : (i j : ι) → i ≤ j → G i →+ G j) (φ : κ →o ι) : AddCommGroup.DirectLimit (fun (j : κ) => G (φ j)) (pullbackBondingMap G f φ) →+ AddCommGroup.DirectLimit G f

The canonical map from the direct limit of the pulled-back system over κ to the direct limit over ι of the original system, induced by the universal property of direct limits.

noncomputable def CechCohomology.cofinalMapEquiv {ι : Type u_1} [Preorder ι] [IsDirectedOrder ι] [DecidableEq ι] [Nonempty ι] {κ : Type u_2} [Preorder κ] [IsDirectedOrder κ] [DecidableEq κ] [Nonempty κ] (G : ι → Type u_3) [(i : ι) → AddCommGroup (G i)] (f : (i j : ι) → i ≤ j → G i →+ G j) [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] (φ : κ →o ι) (hcof : ∀ (i : ι), ∃ (j : κ), i ≤ φ j) : AddCommGroup.DirectLimit (fun (j : κ) => G (φ j)) (pullbackBondingMap G f φ) ≃+ AddCommGroup.DirectLimit G f

Lemma 35.7 (cofinal maps and direct limits). If φ : κ →o ι is cofinal (every i : ι is ≤ φ j for some j : κ), then the induced map between direct limits is an additive equivalence: the limit over a cofinal subset recovers the full limit.

theorem CechCohomology.cofinal_neighborhood_left {X : Type u_1} [TopologicalSpace X] {A B U V : Set X} (hU : IsOpen U) (hV : IsOpen V) (hABU : A ∪ B ⊆ U) (hBV : B ⊆ V) (hVU : V ⊆ U) : ∃ (W : Set X) (Y : Set X), IsOpen W ∧ IsOpen Y ∧ A ⊆ W ∧ B ⊆ Y ∧ W ∪ Y ⊆ U ∧ Y ⊆ V

Cofinality (left half) of the Mayer–Vietoris diagram. Given open neighborhoods U ⊇ A ∪ B, V ⊇ B with V ⊆ U, we can find open neighborhoods W of A and Y of B such that W ∪ Y ⊆ U and Y ⊆ V — trivially, take W := U, Y := V.

theorem CechCohomology.inter_inter_union_subset_of_disjoint {X : Type u_1} {U S V T : Set X} (hST : Disjoint S T) : U ∩ S ∩ (V ∪ T) ⊆ V

Auxiliary set-theoretic lemma: if S and T are disjoint, then (U ∩ S) ∩ (V ∪ T) ⊆ V. Used to verify the inclusion W ∩ Y ⊆ V in the normal/compact cofinality arguments.

theorem CechCohomology.cofinal_neighborhood_right_normal {X : Type u_1} [TopologicalSpace X] [NormalSpace X] {A B : Set X} (hA : IsClosed A) (hB : IsClosed B) {U V : Set X} (hU : IsOpen U) (hV : IsOpen V) (hAU : A ⊆ U) (hABV : A ∩ B ⊆ V) : ∃ (W : Set X) (Y : Set X), IsOpen W ∧ IsOpen Y ∧ A ⊆ W ∧ B ⊆ Y ∧ W ⊆ U ∧ W ∩ Y ⊆ V

Cofinality (right half) for a normal space. Given closed disjoint A, B and open U ⊇ A, V ⊇ A ∩ B, normality produces open W ⊇ A, Y ⊇ B with W ⊆ U and W ∩ Y ⊆ V. Proven by separating A from B ∩ Vᶜ via normal_separation.

theorem CechCohomology.cofinal_neighborhood_right_compact {X : Type u_1} [TopologicalSpace X] [T2Space X] {A B : Set X} (hA : IsCompact A) (hB : IsCompact B) {U V : Set X} (hU : IsOpen U) (hV : IsOpen V) (hAU : A ⊆ U) (hABV : A ∩ B ⊆ V) : ∃ (W : Set X) (Y : Set X), IsOpen W ∧ IsOpen Y ∧ A ⊆ W ∧ B ⊆ Y ∧ W ⊆ U ∧ W ∩ Y ⊆ V

Cofinality (right half) for a Hausdorff space. The compact analogue of cofinal_neighborhood_right_normal: for compact A, B in a Hausdorff space, the same separation conclusion holds, using SeparatedNhds.of_isCompact_isCompact.

theorem CechCohomology.neighborhood_maps_cofinal_normal {X : Type u_1} [TopologicalSpace X] [NormalSpace X] {A B : Set X} (hA : IsClosed A) (hB : IsClosed B) : (∀ (U V : Set X), IsOpen U → IsOpen V → A ∪ B ⊆ U → B ⊆ V → V ⊆ U → ∃ (W : Set X) (Y : Set X), IsOpen W ∧ IsOpen Y ∧ A ⊆ W ∧ B ⊆ Y ∧ W ∪ Y ⊆ U ∧ Y ⊆ V) ∧ ∀ (U V : Set X), IsOpen U → IsOpen V → A ⊆ U → A ∩ B ⊆ V → ∃ (W : Set X) (Y : Set X), IsOpen W ∧ IsOpen Y ∧ A ⊆ W ∧ B ⊆ Y ∧ W ⊆ U ∧ W ∩ Y ⊆ V

Lemma 35.8 (cofinality for Mayer–Vietoris, normal case). For closed subsets A, B of a normal space, the two cofinality conditions (cofinal_neighborhood_left and cofinal_neighborhood_right_normal) both hold; this is the input needed to deduce excision (and hence Mayer–Vietoris) from the abstract cofinality machinery.

theorem CechCohomology.neighborhood_maps_cofinal_compact {X : Type u_1} [TopologicalSpace X] [T2Space X] {A B : Set X} (hA : IsCompact A) (hB : IsCompact B) : (∀ (U V : Set X), IsOpen U → IsOpen V → A ∪ B ⊆ U → B ⊆ V → V ⊆ U → ∃ (W : Set X) (Y : Set X), IsOpen W ∧ IsOpen Y ∧ A ⊆ W ∧ B ⊆ Y ∧ W ∪ Y ⊆ U ∧ Y ⊆ V) ∧ ∀ (U V : Set X), IsOpen U → IsOpen V → A ⊆ U → A ∩ B ⊆ V → ∃ (W : Set X) (Y : Set X), IsOpen W ∧ IsOpen Y ∧ A ⊆ W ∧ B ⊆ Y ∧ W ⊆ U ∧ W ∩ Y ⊆ V

Compact analogue of neighborhood_maps_cofinal_normal: the same conjunction of cofinality conditions holds for compact subsets of a Hausdorff space.

theorem CechCohomology.addCommGroup_directLimit_map_exact {ι : Type u_1} [DecidableEq ι] [Preorder ι] [IsDirectedOrder ι] [Nonempty ι] {G : ι → Type u_2} [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i ≤ j → G i →+ G j} [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)] {G' : ι → Type u_3} [(i : ι) → AddCommGroup (G' i)] {f' : (i j : ι) → i ≤ j → G' i →+ G' j} [DirectedSystem G' fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h)] {G'' : ι → Type u_4} [(i : ι) → AddCommGroup (G'' i)] {f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j} [DirectedSystem G'' fun (i j : ι) (h : i ≤ j) => ⇑(f'' i j h)] (p : (i : ι) → G i →+ G' i) (hp : ∀ (i j : ι) (h : i ≤ j), (p j).comp (f i j h) = (f' i j h).comp (p i)) (q : (i : ι) → G' i →+ G'' i) (hq : ∀ (i j : ι) (h : i ≤ j), (q j).comp (f' i j h) = (f'' i j h).comp (q i)) (exact_at : ∀ (i : ι), Function.Exact ⇑(p i) ⇑(q i)) : Function.Exact ⇑(AddCommGroup.DirectLimit.map p hp) ⇑(AddCommGroup.DirectLimit.map q hq)

Exactness is preserved under direct limits of abelian groups: given two composable, pointwise-exact natural transformations of directed systems of abelian groups, the induced sequence of direct limits is again exact.

@[reducible, inline]

noncomputable abbrev CechCohomology.singChain : CategoryTheory.Functor TopCat (ChainComplex (ModuleCat ℤ) ℕ)

The functor sending a space Y to its integral singular chain complex $S_\bullet(Y; \mathbb{Z})$ as a chain complex of ℤ-modules.

noncomputable def CechCohomology.singCohom (Y : TopCat) (p : ℕ) : ModuleCat ℤ

$p$-th integral singular cohomology $H^p(Y; \mathbb{Z})$ of a space Y, computed by dualising singChain Y and taking the p-th cohomology.

def CechCohomology.CechCohom (X : Type) [TopologicalSpace X] (K : Set X) (p : ℕ) : Type

Čech cohomology $\check{H}^p(X, K; \mathbb{Z})$ of a subset K ⊆ X, defined as the direct limit (cechCohomology) of singular cohomology over open neighborhoods of K.

@[implicit_reducible]

noncomputable instance CechCohomology.CechCohom.addCommGroup (X : Type) [TopologicalSpace X] (K : Set X) (p : ℕ) : AddCommGroup (CechCohom X K p)

The additive group structure on CechCohom X K p, inherited from the underlying module.

noncomputable def CechCohomology.CechCohom.restrict (X : Type) [TopologicalSpace X] {K L : Set X} (h : L ⊆ K) (p : ℕ) : CechCohom X K p →+ CechCohom X L p

The restriction homomorphism $\check{H}^p(X, K) \to \check{H}^p(X, L)$ for $L \subseteq K$, induced functorially by precomposition with open neighborhoods.

noncomputable def CechCohomology.mvRestrict (X : Type) [TopologicalSpace X] (A B : Set X) (p : ℕ) : CechCohom X (A ∪ B) p →+ CechCohom X A p × CechCohom X B p

Mayer–Vietoris restriction map: a class on A ∪ B restricts to a pair of classes on A and B.

noncomputable def CechCohomology.mvDiff (X : Type) [TopologicalSpace X] (A B : Set X) (p : ℕ) : CechCohom X A p × CechCohom X B p →+ CechCohom X (A ∩ B) p

Mayer–Vietoris difference map: a pair of classes on A and B produces the difference of their restrictions to A ∩ B.

noncomputable def CechCohomology.mvConnecting (X : Type) [TopologicalSpace X] [NormalSpace X] {A B : Set X} (hA : IsClosed A) (hB : IsClosed B) (p : ℕ) : CechCohom X (A ∩ B) p →+ CechCohom X (A ∪ B) (p + 1)

Mayer–Vietoris connecting homomorphism (normal case) $\check{H}^p(X, A \cap B) \to \check{H}^{p+1}(X, A \cup B)$ for closed A, B in a normal space.

theorem CechCohomology.mvExact_connecting_restrict (X : Type) [TopologicalSpace X] [NormalSpace X] {A B : Set X} (hA : IsClosed A) (hB : IsClosed B) (p : ℕ) : Function.Exact ⇑(mvConnecting X hA hB p) ⇑(mvRestrict X A B (p + 1))

Exactness at $\check{H}^p(X, A \cup B)$: $\mathrm{im}(\delta) = \ker(\mathrm{restrict})$.

theorem CechCohomology.mvExact_restrict_diff (X : Type) [TopologicalSpace X] [NormalSpace X] {A B : Set X} (hA : IsClosed A) (hB : IsClosed B) (p : ℕ) : Function.Exact ⇑(mvRestrict X A B p) ⇑(mvDiff X A B p)

Exactness at $\check{H}^p(X, A) \oplus \check{H}^p(X, B)$: $\mathrm{im}(\mathrm{restrict}) = \ker(\mathrm{diff})$.

theorem CechCohomology.mvExact_diff_connecting (X : Type) [TopologicalSpace X] [NormalSpace X] {A B : Set X} (hA : IsClosed A) (hB : IsClosed B) (p : ℕ) : Function.Exact ⇑(mvDiff X A B p) ⇑(mvConnecting X hA hB p)

Exactness at $\check{H}^p(X, A \cap B)$: $\mathrm{im}(\mathrm{diff}) = \ker(\delta)$.

noncomputable def CechCohomology.mvConnecting_compact (X : Type) [TopologicalSpace X] [T2Space X] {A B : Set X} (hA : IsCompact A) (hB : IsCompact B) (p : ℕ) : CechCohom X (A ∩ B) p →+ CechCohom X (A ∪ B) (p + 1)

Compact analogue of mvConnecting for compact A, B in a Hausdorff space.

theorem CechCohomology.mvExact_connecting_restrict_compact (X : Type) [TopologicalSpace X] [T2Space X] {A B : Set X} (hA : IsCompact A) (hB : IsCompact B) (p : ℕ) : Function.Exact ⇑(mvConnecting_compact X hA hB p) ⇑(mvRestrict X A B (p + 1))

Compact analogue of mvExact_connecting_restrict.

theorem CechCohomology.mvExact_restrict_diff_compact (X : Type) [TopologicalSpace X] [T2Space X] {A B : Set X} (hA : IsCompact A) (hB : IsCompact B) (p : ℕ) : Function.Exact ⇑(mvRestrict X A B p) ⇑(mvDiff X A B p)

Compact analogue of mvExact_restrict_diff.

theorem CechCohomology.mvExact_diff_connecting_compact (X : Type) [TopologicalSpace X] [T2Space X] {A B : Set X} (hA : IsCompact A) (hB : IsCompact B) (p : ℕ) : Function.Exact ⇑(mvDiff X A B p) ⇑(mvConnecting_compact X hA hB p)

Compact analogue of mvExact_diff_connecting.

theorem CechCohomology.mayerVietoris (X : Type) [TopologicalSpace X] [NormalSpace X] {A B : Set X} (hA : IsClosed A) (hB : IsClosed B) (p : ℕ) : Function.Exact ⇑(mvConnecting X hA hB p) ⇑(mvRestrict X A B (p + 1)) ∧ Function.Exact ⇑(mvRestrict X A B p) ⇑(mvDiff X A B p) ∧ Function.Exact ⇑(mvDiff X A B p) ⇑(mvConnecting X hA hB p)

Corollary 35.9 (Mayer–Vietoris). For closed subsets A, B of a normal space X, the sequence $\cdots \to \check{H}^p(X, A \cup B) \to \check{H}^p(X, A) \oplus \check{H}^p(X, B) \to \check{H}^p(X, A \cap B) \to \check{H}^{p+1}(X, A \cup B) \to \cdots$ is exact.

structure CechCohomology.RelNbhdPair {X : Type} [TopologicalSpace X] (K L : Set X) : Type

A relative neighborhood pair for L ⊆ K ⊆ X: a pair of open sets U ⊇ K, V ⊇ L with V ≤ U. The directed system indexed by these pairs is used to define relative Čech cohomology.

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

@[implicit_reducible]

instance CechCohomology.relNbhdPair_preorder {X : Type} [TopologicalSpace X] {K L : Set X} : Preorder (RelNbhdPair K L)

Preorder on relative neighborhood pairs: p ≤ q iff q.U ⊆ p.U and q.V ⊆ p.V (smaller neighborhoods correspond to larger elements).

instance CechCohomology.relNbhdPair_directed {X : Type} [TopologicalSpace X] {K L : Set X} : IsDirected (RelNbhdPair K L) fun (x1 x2 : RelNbhdPair K L) => x1 ≤ x2

The preorder of relative neighborhood pairs is directed: any two pairs admit a common refinement obtained by intersecting their components.

instance CechCohomology.relNbhdPair_nonempty {X : Type} [TopologicalSpace X] {K L : Set X} : Nonempty (RelNbhdPair K L)

The preorder of relative neighborhood pairs is nonempty: the pair (⊤, ⊤) (the whole space, the whole space) is always a valid neighborhood pair.

def CechCohomology.relNbhdInclusion {X : Type} [TopologicalSpace X] {K L : Set X} (pair : RelNbhdPair K L) : TopCat.of ↑pair.V.carrier ⟶ TopCat.of ↑pair.U.carrier

Continuous inclusion $V \hookrightarrow U$ associated to a relative neighborhood pair (U, V), viewed as a morphism in TopCat.

noncomputable def CechCohomology.relSingCohomOfPair {X : Type} [TopologicalSpace X] {K L : Set X} (pair : RelNbhdPair K L) (p : ℕ) : ModuleCat ℤ

Relative singular cohomology $H^p(U, V; \mathbb{Z})$ of the pair of open sets (U, V) associated to a relative neighborhood pair.

def CechCohomology.relCechFam {X : Type} [TopologicalSpace X] (K L : Set X) (p : ℕ) (pair : RelNbhdPair K L) : Type

Index-wise family $\mathrm{pair} \mapsto H^p(U_{\mathrm{pair}}, V_{\mathrm{pair}})$ whose direct limit will define relative Čech cohomology.

@[implicit_reducible]

noncomputable instance CechCohomology.relCechFam_addCommGroup {X : Type} [TopologicalSpace X] {K L : Set X} (p : ℕ) (pair : RelNbhdPair K L) : AddCommGroup (relCechFam K L p pair)

The additive group structure on each fibre of relCechFam.

def CechCohomology.opensInclusion {X : Type} [TopologicalSpace X] {U₁ U₂ : TopologicalSpace.Opens X} (h : U₂ ≤ U₁) : TopCat.of ↑U₂.carrier ⟶ TopCat.of ↑U₁.carrier

Continuous inclusion U₂ ↪ U₁ of opens (with U₂ ≤ U₁) viewed as a morphism in TopCat.

theorem CechCohomology.opensInclusion_comm {X : Type} [TopologicalSpace X] {K L : Set X} (pair₁ pair₂ : RelNbhdPair K L) (h : pair₁ ≤ pair₂) : CategoryTheory.CategoryStruct.comp (opensInclusion ⋯) (relNbhdInclusion pair₁) = CategoryTheory.CategoryStruct.comp (relNbhdInclusion pair₂) (opensInclusion ⋯)

Naturality square for opens inclusions: the two ways of composing the inclusions $V_2 \hookrightarrow V_1 \hookrightarrow U_1$ and $V_2 \hookrightarrow U_2 \hookrightarrow U_1$ agree.

theorem CechCohomology.restrictionCochainMap_comp (R : Type) [CommRing R] (G : ModuleCat R) {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) : SingularCohomology.restrictionCochainMap R G (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (SingularCohomology.restrictionCochainMap R G g) (SingularCohomology.restrictionCochainMap R G f)

The cochain-restriction operation is contravariantly functorial in composition of continuous maps.

theorem CechCohomology.restrictionCochainMap_square {X : Type} [TopologicalSpace X] {K L : Set X} (pair₁ pair₂ : RelNbhdPair K L) (h : pair₁ ≤ pair₂) : CategoryTheory.CategoryStruct.comp (SingularCohomology.restrictionCochainMap ℤ (ModuleCat.of ℤ ℤ) (relNbhdInclusion pair₁)) (SingularCohomology.restrictionCochainMap ℤ (ModuleCat.of ℤ ℤ) (opensInclusion ⋯)) = CategoryTheory.CategoryStruct.comp (SingularCohomology.restrictionCochainMap ℤ (ModuleCat.of ℤ ℤ) (opensInclusion ⋯)) (SingularCohomology.restrictionCochainMap ℤ (ModuleCat.of ℤ ℤ) (relNbhdInclusion pair₂))

Commutativity of restriction cochain maps along the square of inclusions associated to pair₁ ≤ pair₂: derives from opensInclusion_comm and the contravariant functoriality of restriction.

noncomputable def CechCohomology.relCochainComplexMap {X : Type} [TopologicalSpace X] {K L : Set X} (pair₁ pair₂ : RelNbhdPair K L) (h : pair₁ ≤ pair₂) : SingularCohomology.relativeSingularCochainComplex ℤ (ModuleCat.of ℤ ℤ) (relNbhdInclusion pair₁) ⟶ SingularCohomology.relativeSingularCochainComplex ℤ (ModuleCat.of ℤ ℤ) (relNbhdInclusion pair₂)

Transition map of relative singular cochain complexes induced by pair₁ ≤ pair₂: the canonical map between kernels of the restriction cochain maps coming from the commuting square.

noncomputable def CechCohomology.relCohomTransitionModMap {X : Type} [TopologicalSpace X] {K L : Set X} (pair₁ pair₂ : RelNbhdPair K L) (h : pair₁ ≤ pair₂) (p : ℕ) : relSingCohomOfPair pair₁ p ⟶ relSingCohomOfPair pair₂ p

Transition map between relative singular cohomology groups $H^p(U_1, V_1) \to H^p(U_2, V_2)$ for pair₁ ≤ pair₂, obtained by taking $p$-th homology of relCochainComplexMap.

noncomputable def CechCohomology.relCechTransitionMap {X : Type} [TopologicalSpace X] {K L : Set X} (p : ℕ) (pair₁ pair₂ : RelNbhdPair K L) (h : pair₁ ≤ pair₂) : relCechFam K L p pair₁ →+ relCechFam K L p pair₂

Bonding map of the directed system relCechFam K L p: the underlying additive group hom of relCohomTransitionModMap.

instance CechCohomology.relCechFam_directedSystem_axioms {X : Type} [TopologicalSpace X] {K L : Set X} (p : ℕ) : DirectedSystem (relCechFam K L p) fun (pair₁ pair₂ : RelNbhdPair K L) (h : pair₁ ≤ pair₂) => ⇑(relCechTransitionMap p pair₁ pair₂ h)

relCechFam K L p together with relCechTransitionMap is a directed system: identities act as identities, and composition of bondings respects composition of inclusions.

instance CechCohomology.relCechFam_directedSystem {X : Type} [TopologicalSpace X] {K L : Set X} (p : ℕ) : DirectedSystem (relCechFam K L p) fun (pair₁ pair₂ : RelNbhdPair K L) (h : pair₁ ≤ pair₂) => ⇑(relCechTransitionMap p pair₁ pair₂ h)

Convenience instance form of relCechFam_directedSystem_axioms.

noncomputable def CechCohomology.CechCohomRel (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) : Type

Relative Čech cohomology $\check{H}^p(X, K, L)$: the direct limit over relative neighborhood pairs of (K, L) of the relative singular cohomology $H^p(U, V; \mathbb{Z})$.

@[implicit_reducible]

noncomputable instance CechCohomology.CechCohomRel.addCommGroup (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) : AddCommGroup (CechCohomRel X K L p)

Additive group structure on CechCohomRel X K L p from the direct limit.

def CechCohomology.RelNbhdPair.restrict {X : Type} [TopologicalSpace X] {K₁ K₂ L₁ L₂ : Set X} (h₁ : L₁ ⊆ K₁) (h₂ : L₂ ⊆ K₂) (pair : RelNbhdPair K₁ K₂) : RelNbhdPair L₁ L₂

Restriction of a relative neighborhood pair along inclusions L₁ ⊆ K₁, L₂ ⊆ K₂: a neighborhood pair of (K₁, K₂) is also one of (L₁, L₂).

noncomputable def CechCohomology.CechCohomRel.inclusionMap (X : Type) [TopologicalSpace X] {K₁ K₂ L₁ L₂ : Set X} (h₁ : L₁ ⊆ K₁) (h₂ : L₂ ⊆ K₂) (p : ℕ) : CechCohomRel X K₁ K₂ p →+ CechCohomRel X L₁ L₂ p

Inclusion-induced homomorphism on relative Čech cohomology $\check{H}^p(X, K_1, K_2) \to \check{H}^p(X, L_1, L_2)$ for $L_1 \subseteq K_1$, $L_2 \subseteq K_2$, defined by restricting each neighborhood pair via RelNbhdPair.restrict.

theorem CechCohomology.singularCohomExcisionSurj {X : Type} [TopologicalSpace X] {K L : Set X} (pair₁ pair₂ : RelNbhdPair K L) (h : pair₁ ≤ pair₂) (p : ℕ) (x : relCechFam K L p pair₂) : ∃ (y : relCechFam K L p pair₁), (relCechTransitionMap p pair₁ pair₂ h) y = x

Surjectivity input to excision: every class in $H^p(U_2, V_2)$ comes from $H^p(U_1, V_1)$ when pair₁ ≤ pair₂.

theorem CechCohomology.excisionSurjectivityHelper {X : Type} [TopologicalSpace X] {A B : Set X} (hcof₂ : ∀ (U V : Set X), IsOpen U → IsOpen V → A ⊆ U → A ∩ B ⊆ V → ∃ (W : Set X) (Y : Set X), IsOpen W ∧ IsOpen Y ∧ A ⊆ W ∧ B ⊆ Y ∧ W ⊆ U ∧ W ∩ Y ⊆ V) (p : ℕ) (q : RelNbhdPair B (A ∩ B)) (x : relCechFam B (A ∩ B) p q) : ∃ (pair : RelNbhdPair (A ∪ B) A) (y : relCechFam (A ∪ B) A p pair), (CechCohomRel.inclusionMap X ⋯ ⋯ p) ((AddCommGroup.DirectLimit.of (relCechFam (A ∪ B) A p) (fun (pair₁ pair₂ : RelNbhdPair (A ∪ B) A) (h : pair₁ ≤ pair₂) => relCechTransitionMap p pair₁ pair₂ h) pair) y) = (AddCommGroup.DirectLimit.of (relCechFam B (A ∩ B) p) (fun (pair₁ pair₂ : RelNbhdPair B (A ∩ B)) (h : pair₁ ≤ pair₂) => relCechTransitionMap p pair₁ pair₂ h) q) x

Surjectivity step in excision: under the cofinality hypothesis separating A and B, every class on a neighborhood of (B, A ∩ B) lifts through the inclusion-induced map from neighborhoods of (A ∪ B, A).

theorem CechCohomology.singularCohomExcisionInjective {X : Type} [TopologicalSpace X] {K L : Set X} (pair₁ pair₂ : RelNbhdPair K L) (h : pair₁ ≤ pair₂) (hExc : ∃ (W : Set X) (Y : Set X), IsOpen W ∧ IsOpen Y ∧ ↑pair₁.U = W ∪ Y ∧ ↑pair₁.V = W ∧ ↑pair₂.U = Y ∧ ↑pair₂.V = W ∩ Y) (p : ℕ) (x : relCechFam K L p pair₁) (hx : (relCechTransitionMap p pair₁ pair₂ h) x = 0) : x = 0

Injectivity input to excision: in the excisive configuration $U_1 = W \cup Y$, $V_1 = W$, $U_2 = Y$, $V_2 = W \cap Y$, a relative cohomology class that vanishes under restriction was already zero.

theorem CechCohomology.excisionInjectivityHelper {X : Type} [TopologicalSpace X] {A B : Set X} (hcof₁ : ∀ (U V : Set X), IsOpen U → IsOpen V → A ∪ B ⊆ U → B ⊆ V → V ⊆ U → ∃ (W : Set X) (Y : Set X), IsOpen W ∧ IsOpen Y ∧ A ⊆ W ∧ B ⊆ Y ∧ W ∪ Y ⊆ U ∧ Y ⊆ V) (hcof₂ : ∀ (U V : Set X), IsOpen U → IsOpen V → A ⊆ U → A ∩ B ⊆ V → ∃ (W : Set X) (Y : Set X), IsOpen W ∧ IsOpen Y ∧ A ⊆ W ∧ B ⊆ Y ∧ W ⊆ U ∧ W ∩ Y ⊆ V) (p : ℕ) (pair : RelNbhdPair (A ∪ B) A) (x : relCechFam (A ∪ B) A p pair) (hx : (CechCohomRel.inclusionMap X ⋯ ⋯ p) ((AddCommGroup.DirectLimit.of (relCechFam (A ∪ B) A p) (fun (pair₁ pair₂ : RelNbhdPair (A ∪ B) A) (h : pair₁ ≤ pair₂) => relCechTransitionMap p pair₁ pair₂ h) pair) x) = 0) : (AddCommGroup.DirectLimit.of (relCechFam (A ∪ B) A p) (fun (pair₁ pair₂ : RelNbhdPair (A ∪ B) A) (h : pair₁ ≤ pair₂) => relCechTransitionMap p pair₁ pair₂ h) pair) x = 0

Injectivity step in excision: given both cofinality hypotheses, a class on a neighborhood pair of (A ∪ B, A) mapping to zero in the limit over neighborhood pairs of (B, A ∩ B) was already zero in the source limit.

theorem CechCohomology.excisionFromCofinality (X : Type) [TopologicalSpace X] {A B : Set X} (hcof : (∀ (U V : Set X), IsOpen U → IsOpen V → A ∪ B ⊆ U → B ⊆ V → V ⊆ U → ∃ (W : Set X) (Y : Set X), IsOpen W ∧ IsOpen Y ∧ A ⊆ W ∧ B ⊆ Y ∧ W ∪ Y ⊆ U ∧ Y ⊆ V) ∧ ∀ (U V : Set X), IsOpen U → IsOpen V → A ⊆ U → A ∩ B ⊆ V → ∃ (W : Set X) (Y : Set X), IsOpen W ∧ IsOpen Y ∧ A ⊆ W ∧ B ⊆ Y ∧ W ⊆ U ∧ W ∩ Y ⊆ V) (p : ℕ) : Function.Bijective ⇑(CechCohomRel.inclusionMap X ⋯ ⋯ p)

Abstract excision: whenever the two cofinality conditions hold, the inclusion-induced map $\check{H}^p(X, A \cup B, A) \to \check{H}^p(X, B, A \cap B)$ is bijective.

theorem CechCohomology.cechCohomologyExcision_bijective (X : Type) [TopologicalSpace X] [NormalSpace X] {A B : Set X} (hA : IsClosed A) (hB : IsClosed B) (p : ℕ) : Function.Bijective ⇑(CechCohomRel.inclusionMap X ⋯ ⋯ p)

Bijectivity form of excision (normal case): for closed A, B in a normal Hausdorff space, the inclusion $(B, A \cap B) \hookrightarrow (A \cup B, A)$ induces a bijection on relative Čech cohomology.

noncomputable def CechCohomology.cechCohomologyExcision (X : Type) [TopologicalSpace X] [NormalSpace X] {A B : Set X} (hA : IsClosed A) (hB : IsClosed B) (p : ℕ) : CechCohomRel X (A ∪ B) A p ≃+ CechCohomRel X B (A ∩ B) p

Theorem 35.3 (Excision). For closed A, B in a normal Hausdorff space, the additive equivalence $\check{H}^p(X, A \cup B, A) \xrightarrow{\sim} \check{H}^p(X, B, A \cap B)$ induced by inclusion.

theorem CechCohomology.cechCohomologyExcision_compact_bijective (X : Type) [TopologicalSpace X] [T2Space X] {A B : Set X} (hA : IsCompact A) (hB : IsCompact B) (p : ℕ) : Function.Bijective ⇑(CechCohomRel.inclusionMap X ⋯ ⋯ p)

Bijectivity form of excision (compact case): for compact A, B in a Hausdorff space, the inclusion-induced map on relative Čech cohomology is bijective.

noncomputable def CechCohomology.relToAbs (X : Type) [TopologicalSpace X] {K L : Set X} (hLK : L ⊆ K) (p : ℕ) : CechCohomRel X K L p →+ CechCohom X K p

Map $\check{H}^p(X, K, L) \to \check{H}^p(X, K)$ from relative to absolute Čech cohomology of a pair (first arrow of the long exact sequence).

noncomputable def CechCohomology.lesRestrict (X : Type) [TopologicalSpace X] {K L : Set X} (hLK : L ⊆ K) (p : ℕ) : CechCohom X K p →+ CechCohom X L p

Restriction $\check{H}^p(X, K) \to \check{H}^p(X, L)$ for $L \subseteq K$ (second arrow of the long exact sequence).

noncomputable def CechCohomology.connecting (X : Type) [TopologicalSpace X] {K L : Set X} (hLK : L ⊆ K) (p : ℕ) : CechCohom X L p →+ CechCohomRel X K L (p + 1)

Connecting homomorphism $\check{H}^p(X, L) \to \check{H}^{p+1}(X, K, L)$ in the long exact sequence of the pair $(K, L)$.

def CechCohomology.lesIndexType (X : Type) [TopologicalSpace X] (K L : Set X) : Type

Index type for the long-exact-sequence directed systems: a synonym for RelNbhdPair K L.

@[implicit_reducible]

instance CechCohomology.lesIndexPreorder (X : Type) [TopologicalSpace X] (K L : Set X) : Preorder (lesIndexType X K L)

Preorder on the LES index type, inherited from relNbhdPair_preorder.

instance CechCohomology.lesIndexDirected (X : Type) [TopologicalSpace X] (K L : Set X) : IsDirectedOrder (lesIndexType X K L)

Directedness of the LES index type.

@[implicit_reducible]

noncomputable instance CechCohomology.lesIndexDecEq (X : Type) [TopologicalSpace X] (K L : Set X) : DecidableEq (lesIndexType X K L)

Classical decidable equality on the LES index type.

instance CechCohomology.lesIndexNonempty (X : Type) [TopologicalSpace X] (K L : Set X) : Nonempty (lesIndexType X K L)

Nonemptiness of the LES index type.

def CechCohomology.relFamily (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) : lesIndexType X K L → Type

Relative cohomology family $i \mapsto H^p(U_i, V_i)$ for the pointwise long exact sequence.

@[implicit_reducible]

noncomputable instance CechCohomology.relFamily_acg (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) (i : lesIndexType X K L) : AddCommGroup (relFamily X K L p i)

Additive group structure on each fibre of relFamily.

def CechCohomology.absKFamily (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) : lesIndexType X K L → Type

Absolute cohomology family $i \mapsto H^p(U_i)$ — middle term of the pointwise LES.

@[implicit_reducible]

noncomputable instance CechCohomology.absKFamily_acg (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) (i : lesIndexType X K L) : AddCommGroup (absKFamily X K L p i)

Additive group structure on each fibre of absKFamily.

def CechCohomology.absLFamily (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) : lesIndexType X K L → Type

Absolute cohomology family $i \mapsto H^p(V_i)$ — third term of the pointwise LES.

@[implicit_reducible]

noncomputable instance CechCohomology.absLFamily_acg (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) (i : lesIndexType X K L) : AddCommGroup (absLFamily X K L p i)

Additive group structure on each fibre of absLFamily.

noncomputable def CechCohomology.relBond (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) (i j : lesIndexType X K L) (h : i ≤ j) : relFamily X K L p i →+ relFamily X K L p j

Bonding map for the relative cohomology directed system; re-export of relCechTransitionMap.

instance CechCohomology.relBond_dirSys (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) : DirectedSystem (relFamily X K L p) fun (i j : lesIndexType X K L) (h : i ≤ j) => ⇑(relBond X K L p i j h)

relFamily together with relBond is a directed system.

noncomputable def CechCohomology.absKBond (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) (i j : lesIndexType X K L) (h : i ≤ j) : absKFamily X K L p i →+ absKFamily X K L p j

Bonding map for absKFamily: pullback of singular cohomology along the open inclusion $U_j \hookrightarrow U_i$.

instance CechCohomology.absKBond_dirSys (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) : DirectedSystem (absKFamily X K L p) fun (i j : lesIndexType X K L) (h : i ≤ j) => ⇑(absKBond X K L p i j h)

absKFamily together with absKBond is a directed system.

noncomputable def CechCohomology.absLBond (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) (i j : lesIndexType X K L) (h : i ≤ j) : absLFamily X K L p i →+ absLFamily X K L p j

Bonding map for absLFamily: pullback of singular cohomology along the open inclusion $V_j \hookrightarrow V_i$.

instance CechCohomology.absLBond_dirSys (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) : DirectedSystem (absLFamily X K L p) fun (i j : lesIndexType X K L) (h : i ≤ j) => ⇑(absLBond X K L p i j h)

absLFamily together with absLBond is a directed system.

noncomputable def CechCohomology.ptRelToAbs (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) (i : lesIndexType X K L) : relFamily X K L p i →+ absKFamily X K L p i

Pointwise rel-to-abs map at a single neighborhood pair i = (U, V): $H^p(U, V) \to H^p(U)$, from the kernel inclusion.

noncomputable def CechCohomology.ptRestrict (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) (i : lesIndexType X K L) : absKFamily X K L p i →+ absLFamily X K L p i

Pointwise restriction map at i = (U, V): $H^p(U) \to H^p(V)$, induced by pullback along the inclusion $V \hookrightarrow U$.

instance CechCohomology.restrictionCochainMap_epi {X : Type} [TopologicalSpace X] {K L : Set X} (i : lesIndexType X K L) : CategoryTheory.Epi (SingularCohomology.restrictionCochainMap ℤ (ModuleCat.of ℤ ℤ) (relNbhdInclusion i))

The restriction-of-cochains map associated to a relative neighborhood pair is an epimorphism in the category of cochain complexes of ℤ-modules.

noncomputable def CechCohomology.cochainSES {X : Type} [TopologicalSpace X] {K L : Set X} (i : lesIndexType X K L) : { X₁ := CategoryTheory.Limits.kernel (SingularCohomology.restrictionCochainMap ℤ (ModuleCat.of ℤ ℤ) (relNbhdInclusion i)), X₂ := SingularCohomology.singularCochainComplex ℤ (TopCat.of ↑i.U.carrier) (ModuleCat.of ℤ ℤ), X₃ := SingularCohomology.singularCochainComplex ℤ (TopCat.of ↑i.V.carrier) (ModuleCat.of ℤ ℤ), f := CategoryTheory.Limits.kernel.ι (SingularCohomology.restrictionCochainMap ℤ (ModuleCat.of ℤ ℤ) (relNbhdInclusion i)), g := SingularCohomology.restrictionCochainMap ℤ (ModuleCat.of ℤ ℤ) (relNbhdInclusion i), zero := ⋯ }.ShortExact

Short exact sequence of cochain complexes $0 \to C^\bullet(U, V) \to C^\bullet(U) \to C^\bullet(V) \to 0$ for the neighborhood pair i = (U, V).

noncomputable def CechCohomology.ptConnecting (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) (i : lesIndexType X K L) : absLFamily X K L p i →+ relFamily X K L (p + 1) i

Pointwise connecting homomorphism $H^p(V) \to H^{p+1}(U, V)$ associated to cochainSES i.

theorem CechCohomology.relCochainComplexMap_comp_kernel_ι {X : Type} [TopologicalSpace X] {K L : Set X} (i j : lesIndexType X K L) (h : i ≤ j) : CategoryTheory.CategoryStruct.comp (relCochainComplexMap i j h) (CategoryTheory.Limits.kernel.ι (SingularCohomology.restrictionCochainMap ℤ (ModuleCat.of ℤ ℤ) (relNbhdInclusion j))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (SingularCohomology.restrictionCochainMap ℤ (ModuleCat.of ℤ ℤ) (relNbhdInclusion i))) (SingularCohomology.restrictionCochainMap ℤ (ModuleCat.of ℤ ℤ) (opensInclusion ⋯))

The compatibility square relCochainComplexMap followed by the kernel inclusion equals the kernel inclusion followed by the absolute restriction cochain map.

theorem CechCohomology.ptRelToAbs_nat (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) (i j : lesIndexType X K L) (h : i ≤ j) : (ptRelToAbs X K L p j).comp (relBond X K L p i j h) = (absKBond X K L p i j h).comp (ptRelToAbs X K L p i)

Naturality of ptRelToAbs: the pointwise rel-to-abs maps commute with the bonding maps of relFamily and absKFamily.

theorem CechCohomology.ptRestrict_nat (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) (i j : lesIndexType X K L) (h : i ≤ j) : (ptRestrict X K L p j).comp (absKBond X K L p i j h) = (absLBond X K L p i j h).comp (ptRestrict X K L p i)

Naturality of ptRestrict: pointwise restrictions $H^p(U_i) \to H^p(V_i)$ commute with the bonding maps of absKFamily and absLFamily.

theorem CechCohomology.ptConnecting_nat (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) (i j : lesIndexType X K L) (h : i ≤ j) : (ptConnecting X K L p j).comp (absLBond X K L p i j h) = (relBond X K L (p + 1) i j h).comp (ptConnecting X K L p i)

Naturality of ptConnecting: pointwise connecting homomorphisms commute with the bondings of absLFamily and (shifted) relFamily, via δ-naturality of the homology sequence applied to a morphism of short exact sequences.

theorem CechCohomology.ptExact_relToAbs_restrict (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) (i : lesIndexType X K L) : Function.Exact ⇑(ptRelToAbs X K L p i) ⇑(ptRestrict X K L p i)

Pointwise exactness at the absolute term: at each i, the sequence relFamily → absKFamily → absLFamily is exact, from cochainSES.homology_exact₂.

theorem CechCohomology.ptExact_restrict_connecting (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) (i : lesIndexType X K L) : Function.Exact ⇑(ptRestrict X K L p i) ⇑(ptConnecting X K L p i)

Pointwise exactness at absLFamily: at each i, the sequence absKFamily → absLFamily → relFamily(p+1) is exact, from cochainSES.homology_exact₃.

theorem CechCohomology.ptExact_connecting_relToAbs (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) (i : lesIndexType X K L) : Function.Exact ⇑(ptConnecting X K L p i) ⇑(ptRelToAbs X K L (p + 1) i)

Pointwise exactness at relFamily(p+1): at each i, the sequence absLFamily → relFamily(p+1) → absKFamily(p+1) is exact, from cochainSES.homology_exact₁.

noncomputable def CechCohomology.eqvRel (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) : CechCohomRel X K L p ≃+ AddCommGroup.DirectLimit (relFamily X K L p) (relBond X K L p)

Definitional identification of CechCohomRel X K L p with the direct limit of relFamily.

noncomputable def CechCohomology.eqvAbsK (X : Type) [TopologicalSpace X] (K L : Set X) (hLK : L ⊆ K) (p : ℕ) : CechCohom X K p ≃+ AddCommGroup.DirectLimit (absKFamily X K L p) (absKBond X K L p)

Identification of $\check{H}^p(X, K)$ with the direct limit of absKFamily over relative neighborhood pairs of (K, L): the neighborhoods U_i of K appearing as the first component of RelNbhdPair K L are cofinal among all open neighborhoods of K.

noncomputable def CechCohomology.eqvAbsL (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) : CechCohom X L p ≃+ AddCommGroup.DirectLimit (absLFamily X K L p) (absLBond X K L p)

Identification of $\check{H}^p(X, L)$ with the direct limit of absLFamily over relative neighborhood pairs of (K, L): the neighborhoods V_i of L appearing as the second component are cofinal among all open neighborhoods of L.

theorem CechCohomology.comm_relToAbs (X : Type) [TopologicalSpace X] {K L : Set X} (hLK : L ⊆ K) (p : ℕ) : (relToAbs X hLK p).comp (eqvRel X K L p).symm.toAddMonoidHom = (eqvAbsK X K L hLK p).symm.toAddMonoidHom.comp (AddCommGroup.DirectLimit.map (ptRelToAbs X K L p) ⋯)

Compatibility square: the rel-to-abs map agrees with the direct limit of pointwise rel-to-abs maps under the equivalences eqvRel and eqvAbsK.

theorem CechCohomology.comm_lesRestrict (X : Type) [TopologicalSpace X] {K L : Set X} (hLK : L ⊆ K) (p : ℕ) : (lesRestrict X hLK p).comp (eqvAbsK X K L hLK p).symm.toAddMonoidHom = (eqvAbsL X K L p).symm.toAddMonoidHom.comp (AddCommGroup.DirectLimit.map (ptRestrict X K L p) ⋯)

Compatibility square: the restriction map agrees with the direct limit of pointwise restrictions under eqvAbsK and eqvAbsL.

theorem CechCohomology.comm_connecting (X : Type) [TopologicalSpace X] {K L : Set X} (hLK : L ⊆ K) (p : ℕ) : (connecting X hLK p).comp (eqvAbsL X K L p).symm.toAddMonoidHom = (eqvRel X K L (p + 1)).symm.toAddMonoidHom.comp (AddCommGroup.DirectLimit.map (ptConnecting X K L p) ⋯)

Compatibility square: the connecting map agrees with the direct limit of pointwise connecting maps under eqvAbsL and eqvRel (shifted by one).

theorem CechCohomology.longExactSequence (X : Type) [TopologicalSpace X] {K L : Set X} (_hK : IsClosed K) (_hL : IsClosed L) (hLK : L ⊆ K) (p : ℕ) : Function.Exact ⇑(relToAbs X hLK p) ⇑(lesRestrict X hLK p) ∧ Function.Exact ⇑(lesRestrict X hLK p) ⇑(connecting X hLK p) ∧ Function.Exact ⇑(connecting X hLK p) ⇑(relToAbs X hLK (p + 1))

Theorem 35.2 (Long exact sequence of a pair in Čech cohomology). For closed $L \subseteq K \subseteq X$, the sequence $\cdots \to \check{H}^p(X, K, L) \to \check{H}^p(X, K) \to \check{H}^p(X, L) \to \check{H}^{p+1}(X, K, L) \to \cdots$ is exact. Proved by combining the pointwise short-exact sequences of neighborhood pairs with addCommGroup_directLimit_map_exact and transporting along the equivalences eqvRel, eqvAbsK, eqvAbsL.