noncomputable def PoincareDuality.relativeSingularCohomology (R : Type) [CommRing R] (X : Type) [TopologicalSpace X] (A : Set X) (p : ℕ) : ModuleCat R

Relative singular cohomology $H^p(X, A; R)$ of a pair $(X, A)$ with coefficients in $R$, as an object of ModuleCat.{0} R.

noncomputable def PoincareDuality.relativeSingularHomology (R : Type) [CommRing R] (X : Type) [TopologicalSpace X] (A : Set X) (q : ℕ) : ModuleCat R

Relative singular homology $H_q(X, A; R)$ of a pair $(X, A)$ with coefficients in $R$, as an object of ModuleCat.{0} R.

noncomputable def PoincareDuality.relativeSingularHomology_map (R : Type) [CommRing R] {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (A : Set X) (B : Set Y) (hf : ⇑f '' A ⊆ B) (q : ℕ) : relativeSingularHomology R X A q ⟶ relativeSingularHomology R Y B q

Functoriality of relative singular homology: a continuous map of pairs $f : (X, A) \to (Y, B)$ (i.e. $f$ with $f(A) \subseteq B$) induces $f_* : H_q(X, A; R) \to H_q(Y, B; R)$.

theorem PoincareDuality.relativeSingularHomology_map_id (R : Type) [CommRing R] {X : Type} [TopologicalSpace X] (A : Set X) (q : ℕ) (h : ⇑(ContinuousMap.id X) '' A ⊆ A) : relativeSingularHomology_map R (ContinuousMap.id X) A A h q = CategoryTheory.CategoryStruct.id (relativeSingularHomology R X A q)

The map induced by the identity $\mathrm{id}_X$ on relative singular homology is the identity morphism.

theorem PoincareDuality.relativeSingularHomology_map_comp (R : Type) [CommRing R] {X Y Z : Type} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : C(X, Y)) (g : C(Y, Z)) (A : Set X) (B : Set Y) (D : Set Z) (hf : ⇑f '' A ⊆ B) (hg : ⇑g '' B ⊆ D) (hgf : ⇑(g.comp f) '' A ⊆ D) (q : ℕ) : CategoryTheory.CategoryStruct.comp (relativeSingularHomology_map R f A B hf q) (relativeSingularHomology_map R g B D hg q) = relativeSingularHomology_map R (g.comp f) A D hgf q

The functor on pairs preserves composition: $(g \circ f)_* = g_* \circ f_*$ on relative singular homology.

theorem PoincareDuality.relativeSingularHomology_map_congr (R : Type) [CommRing R] {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] (f g : C(X, Y)) (hfg : f = g) (A : Set X) (B : Set Y) (hf : ⇑f '' A ⊆ B) (hg : ⇑g '' A ⊆ B) (q : ℕ) : relativeSingularHomology_map R f A B hf q = relativeSingularHomology_map R g A B hg q

If two maps of pairs $f, g : (X, A) \to (Y, B)$ are equal as continuous maps, the induced maps on relative singular homology agree.

class PoincareDuality.IsROriented (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] : Prop

An $n$-manifold $M$ is IsROriented if it admits an $R$-orientation, i.e. a coherent choice of local-homology generators. This is the prerequisite for talking about a fundamental class and hence Poincaré duality with coefficients in $R$.

• isROrientable : OrientationHomology.IsROrientable n M R

noncomputable def PoincareDuality.restrictToLocalHomology (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (x : M) : relativeSingularHomology R M ∅ n ⟶ relativeSingularHomology R M {x}ᶜ n

The restriction map $H_n(M; R) \to H_n(M, M - \{x\}; R)$ to the local homology at a point $x$, induced by enlarging the relative subset from $\emptyset$ to $\{x\}^c$.

noncomputable def PoincareDuality.restrictAlongToLocalHomology (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K : Set M) (x : M) (hx : x ∈ K) : relativeSingularHomology R M Kᶜ n ⟶ relativeSingularHomology R M {x}ᶜ n

The restriction $H_n(M, M-K; R) \to H_n(M, M-\{x\}; R)$ from the relative homology along a compact subset $K$ to the local homology at a point $x \in K$. This is the map used to detect whether a class in $H_n(M, M-K; R)$ is a fundamental class along $K$.

def PoincareDuality.isLocalHomologyGenerator (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (x : M) (μ : ↑(relativeSingularHomology R M {x}ᶜ n)) : Prop

The predicate "$\mu$ generates the local homology at $x$": the $R$-submodule spanned by $\mu \in H_n(M, M-\{x\}; R)$ is the whole module. An $R$-orientation along $K$ is characterised by producing local generators at every $x \in K$.

noncomputable def PoincareDuality.homologyBridgeToSection37 (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (A : Set M) : OrientationHomology.relativeHomologyModule R n M A ≅ relativeSingularHomology R M A n

Identification of the relative-homology module used in the Section 34 orientation machinery with the relative singular homology used here. Glue isomorphism that lets us transport fundamental-class results across the two presentations.

theorem PoincareDuality.homologyBridge_restriction_comm (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (x : M) (α : ↑(OrientationHomology.relativeHomologyModule R n M ∅)) : (ModuleCat.Hom.hom (restrictToLocalHomology R n M x)) ((CategoryTheory.ConcreteCategory.hom (homologyBridgeToSection37 R n M ∅).hom) α) = (CategoryTheory.ConcreteCategory.hom (homologyBridgeToSection37 R n M {x}ᶜ).hom) ((ModuleCat.Hom.hom (OrientationHomology.restrictionHomologyMap R n M ∅ {x}ᶜ ⋯)) α)

Compatibility of the bridge homologyBridgeToSection37 with restriction to local homology: restricting first and then bridging equals bridging first and then restricting.

theorem PoincareDuality.fundamentalClass_in_relativeHomology (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (h : OrientationHomology.IsROrientable n M R) : ∃ (α : ↑(OrientationHomology.relativeHomologyModule R n M ∅)), ∀ (x : M), R ∙ (ModuleCat.Hom.hom (OrientationHomology.restrictionHomologyMap R n M ∅ {x}ᶜ ⋯)) α = ⊤

Existence of a fundamental class in the Section-34 form: for a compact oriented $n$-manifold $M$, there exists $\alpha \in H_n(M, \emptyset; R)$ whose restriction to each local homology $H_n(M, M-\{x\}; R)$ is a generator.

theorem PoincareDuality.fundamentalClass_of_isROrientable (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (h : OrientationHomology.IsROrientable n M R) : ∃ (μ : ↑(relativeSingularHomology R M ∅ n)), ∀ (x : M), isLocalHomologyGenerator R n M x ((ModuleCat.Hom.hom (restrictToLocalHomology R n M x)) μ)

Existence of a fundamental class $\mu \in H_n(M; R)$ in the present relativeSingularHomology formulation: each local-homology restriction $(\restrictToLocalHomology)(\mu)$ generates $H_n(M, M-\{x\}; R)$ for every $x$.

theorem PoincareDuality.fundamentalClass_unique (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (μ₁ μ₂ : ↑(relativeSingularHomology R M ∅ n)) (h₁ : ∀ (x : M), isLocalHomologyGenerator R n M x ((ModuleCat.Hom.hom (restrictToLocalHomology R n M x)) μ₁)) (h₂ : ∀ (x : M), isLocalHomologyGenerator R n M x ((ModuleCat.Hom.hom (restrictToLocalHomology R n M x)) μ₂)) : μ₁ = μ₂

Uniqueness of the fundamental class: any two classes whose local-homology restrictions are simultaneously generators at every point of a compact connected oriented manifold coincide.

noncomputable def PoincareDuality.cechCohomology (R : Type) [CommRing R] (X : Type) [TopologicalSpace X] (K L : Set X) (p : ℕ) : ModuleCat R

Čech cohomology $\check H^p(X, K, L; R)$ of a triple $(X, K, L)$ used to phrase the fully relative Poincaré duality theorem. Defined as the colimit of relative singular cohomologies $H^p(U, V; R)$ over open neighbourhoods $V \subseteq U$ of $L \subseteq K$.

noncomputable def PoincareDuality.cohomRestriction (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (L : Set M) (p : ℕ) : cechCohomology R M Set.univ L p ⟶ relativeSingularCohomology R M ∅ p

Restriction map $\check H^p(M, M, L; R) \to H^p(M; R)$ from Čech cohomology of the triple $(M, M, L)$ to absolute singular cohomology.

noncomputable def PoincareDuality.cohomToSubspace (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (L : Set M) (p : ℕ) : relativeSingularCohomology R M ∅ p ⟶ cechCohomology R M L ∅ p

Restriction-to-subspace map $H^p(M; R) \to \check H^p(M, L; R)$ used in the Mayer-Vietoris-like long exact sequence underlying Poincaré duality.

noncomputable def PoincareDuality.cohomCoboundary (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (L : Set M) (p : ℕ) : cechCohomology R M L ∅ p ⟶ cechCohomology R M Set.univ L (p + 1)

Coboundary/connecting map $\check H^p(M, L; R) \to \check H^{p+1}(M, M, L; R)$ in the long exact sequence of the triple $(M, M, L)$.

noncomputable def PoincareDuality.homolFromOpen (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (L : Set M) (q : ℕ) : relativeSingularHomology R ↑Lᶜ ∅ q ⟶ relativeSingularHomology R M ∅ q

Inclusion-induced map $H_q(L^c; R) \to H_q(M; R)$, where the open complement $L^c$ is viewed as a topological subspace.

noncomputable def PoincareDuality.homolToRelative (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (L : Set M) (q : ℕ) : relativeSingularHomology R M ∅ q ⟶ relativeSingularHomology R M Lᶜ q

Pair-restriction map $H_q(M; R) \to H_q(M, L^c; R)$ enlarging the relative subset from $\emptyset$ to $L^c$.

noncomputable def PoincareDuality.homolBoundary (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (L : Set M) (q : ℕ) : relativeSingularHomology R M Lᶜ (q + 1) ⟶ relativeSingularHomology R ↑Lᶜ ∅ q

Connecting homomorphism $H_{q+1}(M, L^c; R) \to H_q(L^c; R)$ of the long exact sequence of the pair $(M, L^c)$.

class PoincareDuality.IsROrientedAlong (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K : Set M) : Prop

$M$ is $R$-oriented along $K$ if there is a class $\mu \in H_n(M, M-K; R)$ whose local restriction at every $x \in K$ is a generator. This is the data needed for cap-product Poincaré duality along $K$.

• hasFundamentalClassAlong : ∃ (μ : ↑(relativeSingularHomology R M Kᶜ n)), ∀ (x : M) (hx : x ∈ K), isLocalHomologyGenerator R n M x ((ModuleCat.Hom.hom (restrictAlongToLocalHomology R n M K x hx)) μ)

theorem PoincareDuality.restrictAlongToLocalHomology_univ_eq (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (x : M) (hx : x ∈ Set.univ) : restrictAlongToLocalHomology R n M Set.univ x hx = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (restrictToLocalHomology R n M x)

Compatibility lemma: the restriction $\restrictAlongToLocalHomology$ at $K = M$ equals the absolute restriction-to-local-homology (after the canonical identification $M - M = \emptyset$).

theorem PoincareDuality.isROrientedAlong_univ_of_isROriented (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] : ∃ (μ : ↑(relativeSingularHomology R M Set.univᶜ n)), ∀ (x : M) (hx : x ∈ Set.univ), isLocalHomologyGenerator R n M x ((ModuleCat.Hom.hom (restrictAlongToLocalHomology R n M Set.univ x hx)) μ)

An $R$-oriented compact manifold is $R$-oriented along $M$ (the entire space), with fundamental class transported via the identification $H_n(M, M^c; R) = H_n(M; R)$.

instance PoincareDuality.isROrientedAlong_univ (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] : IsROrientedAlong R n M Set.univ

Instance: any compact $R$-oriented manifold is automatically $R$-oriented along $M = \Set.univ$.

noncomputable def PoincareDuality.relativeSingularHomologyRestrict (R : Type) [CommRing R] (X : Type) [TopologicalSpace X] (A B : Set X) (h : A ⊆ B) (q : ℕ) : ↑(relativeSingularHomology R X A q) → ↑(relativeSingularHomology R X B q)

Subset-monotonicity of the relative-singular-homology functor: an inclusion $A \subseteq B$ induces the natural map $H_q(X, A; R) \to H_q(X, B; R)$.

theorem PoincareDuality.restrictAlongToLocalHomology_comp_restrict (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K L : Set M) (hLK : L ⊆ K) (x : M) (hxL : x ∈ L) (μ : ↑(relativeSingularHomology R M Kᶜ n)) : (ModuleCat.Hom.hom (restrictAlongToLocalHomology R n M L x hxL)) (relativeSingularHomologyRestrict R M Kᶜ Lᶜ ⋯ n μ) = (ModuleCat.Hom.hom (restrictAlongToLocalHomology R n M K x ⋯)) μ

Compatibility of restriction-to-local-homology with the pair-restriction $H_n(M, K^c; R) \to H_n(M, L^c; R)$ along $L \subseteq K$: restricting to local homology at $x \in L$ commutes with the pair restriction, and equals the local restriction from $K$.

theorem PoincareDuality.isROrientedAlong_of_subset (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K L : Set M) (hLK : L ⊆ K) (hOr : IsROrientedAlong R n M K) : IsROrientedAlong R n M L

$R$-orientability descends to subsets: if $M$ is $R$-oriented along $K$ and $L \subseteq K$, then $M$ is $R$-oriented along $L$, via the pair-restriction of fundamental classes.

noncomputable def PoincareDuality.capProductIso_step1_compactConvex (R : Type) [CommRing R] (n : ℕ) (K : Set (EuclideanSpace ℝ (Fin n))) (hK : IsCompact K) (hConv : Convex ℝ K) (hOr : IsROrientedAlong R n (EuclideanSpace ℝ (Fin n)) K) (p q : ℕ) (hpq : p + q = n) : cechCohomology R (EuclideanSpace ℝ (Fin n)) K ∅ p ≅ relativeSingularHomology R (EuclideanSpace ℝ (Fin n)) Kᶜ q

Step 1 of the absolute cap-product iso (Theorem 37.1). For $K \subseteq \mathbb{R}^n$ compact and convex, the cap-product map $\check H^p(\mathbb{R}^n, K; R) \to H_q(\mathbb{R}^n, \mathbb{R}^n - K; R)$ is an isomorphism for $p + q = n$, proved by direct computation using contractibility of $K$.

noncomputable def PoincareDuality.capProductIso_step2_finiteUnionConvex (R : Type) [CommRing R] (n : ℕ) (K : Set (EuclideanSpace ℝ (Fin n))) (hK : IsCompact K) (hFinConvex : ∃ (S : Finset (Set (EuclideanSpace ℝ (Fin n)))), (∀ C ∈ S, IsCompact C ∧ Convex ℝ C) ∧ K = ⋃₀ ↑S) (hOr : IsROrientedAlong R n (EuclideanSpace ℝ (Fin n)) K) (p q : ℕ) (hpq : p + q = n) : cechCohomology R (EuclideanSpace ℝ (Fin n)) K ∅ p ≅ relativeSingularHomology R (EuclideanSpace ℝ (Fin n)) Kᶜ q

Step 2 of Theorem 37.1. Extends Step 1 from compact convex sets to finite unions of compact convex sets, via Mayer-Vietoris and the five lemma.

noncomputable def PoincareDuality.capProductIso_step3_compactEuclidean (R : Type) [CommRing R] (n : ℕ) (K : Set (EuclideanSpace ℝ (Fin n))) (hK : IsCompact K) (hOr : IsROrientedAlong R n (EuclideanSpace ℝ (Fin n)) K) (p q : ℕ) (hpq : p + q = n) : cechCohomology R (EuclideanSpace ℝ (Fin n)) K ∅ p ≅ relativeSingularHomology R (EuclideanSpace ℝ (Fin n)) Kᶜ q

Step 3 of Theorem 37.1. Extends Step 2 to arbitrary compact subsets $K \subseteq \mathbb{R}^n$ by writing $K$ as the decreasing intersection of finite unions of cubes (or compact convex sets), and passing to the colimit.

noncomputable def PoincareDuality.capProductIso_step4_finiteUnionCharts (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K : Set M) (hK : IsCompact K) (hFinChart : ∃ (S : Finset (Set M)), (∀ C ∈ S, IsCompact C ∧ ∃ e ∈ atlas (EuclideanSpace ℝ (Fin n)) M, C ⊆ e.source) ∧ K = ⋃₀ ↑S) (hOr : IsROrientedAlong R n M K) (p q : ℕ) (hpq : p + q = n) : cechCohomology R M K ∅ p ≅ relativeSingularHomology R M Kᶜ q

Step 4 of Theorem 37.1. Generalises Step 3 from $\mathbb{R}^n$ to charted manifolds $M$, for $K$ a finite union of compacts each lying in a single chart, via Mayer-Vietoris on charts and the previous step.

theorem PoincareDuality.compact_decreasingIntersection_finiteUnionCharts (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K : Set M) (hK : IsCompact K) : ∃ (A : ℕ → Set M), (∀ (i : ℕ), IsCompact (A i)) ∧ (∀ (i : ℕ), A (i + 1) ⊆ A i) ∧ K = ⋂ (i : ℕ), A i ∧ ∀ (i : ℕ), ∃ (S : Finset (Set M)), (∀ C ∈ S, IsCompact C ∧ ∃ e ∈ atlas (EuclideanSpace ℝ (Fin n)) M, C ⊆ e.source) ∧ A i = ⋃₀ ↑S

Geometric input for Step 5: every compact $K$ in a charted manifold is the decreasing intersection of compacts $A_i$, each of which is a finite union of compacts contained in single chart neighbourhoods. Allows passing from Step 4 to arbitrary compacts.

noncomputable def PoincareDuality.cechCohomologyRestriction (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (K K' : Set M) (_hKK' : K' ⊆ K) (p : ℕ) : cechCohomology R M K ∅ p ⟶ cechCohomology R M K' ∅ p

Restriction map $\check H^p(M, K; R) \to \check H^p(M, K'; R)$ for $K' \subseteq K$, realised on Čech cohomology by enlarging the open neighbourhood system from $K$ to $K'$.

theorem PoincareDuality.cechCohomologyRestriction_isIso_of_colimit (R : Type) [CommRing R] {n : ℕ} (M : Type) [TopologicalSpace M] [T2Space M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (A : ℕ → Set M) (hA : Antitone A) (hcpt : ∀ (k : ℕ), IsCompact (A k)) (p k : ℕ) : CategoryTheory.IsIso (cechCohomologyRestriction R M (A k) (⋂ (j : ℕ), A j) ⋯ p)

For a Hausdorff manifold and an antitone family $A_k$ of compacts with intersection $A_\infty$, the restriction $\check H^p(M, A_k; R) \to \check H^p(M, A_\infty; R)$ is an iso. The key colimit/continuity statement of Lemma 37.2.

theorem PoincareDuality.cechCohomologyRestriction_eq_iso_hom (R : Type) [CommRing R] {n : ℕ} (M : Type) [TopologicalSpace M] [T2Space M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (A : ℕ → Set M) (hA : Antitone A) (hcpt : ∀ (k : ℕ), IsCompact (A k)) (p k : ℕ) : ∃ (iso : cechCohomology R M (A k) ∅ p ≅ cechCohomology R M (⋂ (j : ℕ), A j) ∅ p), cechCohomologyRestriction R M (A k) (⋂ (j : ℕ), A j) ⋯ p = iso.hom

Packaging form of cechCohomologyRestriction_isIso_of_colimit: the restriction map itself equals the hom-component of an explicit isomorphism.

theorem PoincareDuality.cechCohomologyRestriction_isIso (R : Type) [CommRing R] {n : ℕ} (M : Type) [TopologicalSpace M] [T2Space M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (A : ℕ → Set M) (hA : Antitone A) (hcpt : ∀ (k : ℕ), IsCompact (A k)) (p k : ℕ) : CategoryTheory.IsIso (cechCohomologyRestriction R M (A k) (⋂ (j : ℕ), A j) ⋯ p)

Convenient typeclass form of cechCohomologyRestriction_isIso_of_colimit.

noncomputable def PoincareDuality.cechCohomology_decreasing_compact_iso (R : Type) [CommRing R] {n : ℕ} (M : Type) [TopologicalSpace M] [T2Space M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (A : ℕ → Set M) (hA : Antitone A) (hcpt : ∀ (k : ℕ), IsCompact (A k)) (p k : ℕ) : cechCohomology R M (A k) ∅ p ≅ cechCohomology R M (⋂ (j : ℕ), A j) ∅ p

Iso form of the colimit statement (Lemma 37.2): for an antitone family of compacts $A_k$ with intersection $A_\infty$, the natural map $\check H^p(M, A_k; R) \to \check H^p(M, A_\infty; R)$ is an iso for every $k$.

noncomputable def PoincareDuality.cechCohomology_decreasingCompact_iso (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (A : ℕ → Set M) (hA : Antitone A) (hcpt : ∀ (k : ℕ), IsCompact (A k)) (p k : ℕ) : cechCohomology R M (A k) ∅ p ≅ cechCohomology R M (⋂ (j : ℕ), A j) ∅ p

Public-facing alias for cechCohomology_decreasing_compact_iso.

noncomputable def PoincareDuality.relativeSingularHomology_colimit_decreasingCompact (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (A : ℕ → Set M) (hA : Antitone A) (hcpt : ∀ (k : ℕ), IsCompact (A k)) (q k : ℕ) : relativeSingularHomology R M (⋂ (j : ℕ), A j)ᶜ q ≅ relativeSingularHomology R M (A k)ᶜ q

Homological analogue of the colimit statement: for an antitone family of compacts $A_k$ with intersection $A_\infty$, the pair-homology $H_q(M, A_\infty^c; R)$ is isomorphic to $H_q(M, A_k^c; R)$ for every $k$.

theorem PoincareDuality.isROrientedAlong_of_supset_finiteUnionCharts (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K K' : Set M) (hKK' : K ⊆ K') (hK' : IsCompact K') (hFinChart : ∃ (S : Finset (Set M)), (∀ C ∈ S, IsCompact C ∧ ∃ e ∈ atlas (EuclideanSpace ℝ (Fin n)) M, C ⊆ e.source) ∧ K' = ⋃₀ ↑S) (hOr : IsROrientedAlong R n M K) : IsROrientedAlong R n M K'

Upward extension: if $M$ is $R$-oriented along $K \subseteq K'$ and $K'$ is a finite union of compacts each lying in a single chart, then $M$ is $R$-oriented along $K'$. Used when bootstrapping orientability from arbitrary compacts to chart-finite-union compacts.

noncomputable def PoincareDuality.capProductIso_step5_arbitraryCompact (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K : Set M) (hK : IsCompact K) (hOr : IsROrientedAlong R n M K) (p q : ℕ) (hpq : p + q = n) : cechCohomology R M K ∅ p ≅ relativeSingularHomology R M Kᶜ q

Step 5 of Theorem 37.1. Final step: for arbitrary compact $K$ in a Hausdorff charted manifold $M$, the cap-product map is an iso, obtained as a colimit of Step-4 isos along an antitone family of finite-chart-union approximations to $K$.

noncomputable def PoincareDuality.capProductWithFundamentalClass (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K : Set M) (hK : IsCompact K) (hOr : IsROrientedAlong R n M K) (p q : ℕ) (hpq : p + q = n) : cechCohomology R M K ∅ p ⟶ relativeSingularHomology R M Kᶜ q

The cap-product map $\cap[\mu_K] : \check H^p(M, K; R) \to H_q(M, M-K; R)$ with the fundamental class $\mu_K$ along $K$. Underlies the absolute Poincaré duality iso.

noncomputable def PoincareDuality.absoluteCapProductIso (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K : Set M) (hK : IsCompact K) (hOr : IsROrientedAlong R n M K) (p q : ℕ) (hpq : p + q = n) : cechCohomology R M K ∅ p ≅ relativeSingularHomology R M Kᶜ q

The absolute cap-product iso, packaged: for compact $K \subseteq M$ along which $M$ is $R$-oriented, $\check H^p(M, K; R) \cong H_q(M, M-K; R)$ for $p + q = n$. Wraps Step 5.

theorem PoincareDuality.absoluteCapProductIso_hom_eq_capProduct (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K : Set M) (hK : IsCompact K) (hOr : IsROrientedAlong R n M K) (p q : ℕ) (hpq : p + q = n) : (absoluteCapProductIso R n M K hK hOr p q hpq).hom = capProductWithFundamentalClass R n M K hK hOr p q hpq

The hom component of absoluteCapProductIso is, by construction, the cap-product map $\cap[\mu_K]$.

theorem PoincareDuality.fiveLemma_moduleCat_isIso (R : Type) [CommRing R] {A₁ A₂ A₃ A₄ A₅ B₁ B₂ B₃ B₄ B₅ : ModuleCat R} (f₁ : A₁ ⟶ A₂) (f₂ : A₂ ⟶ A₃) (f₃ : A₃ ⟶ A₄) (f₄ : A₄ ⟶ A₅) (g₁ : B₁ ⟶ B₂) (g₂ : B₂ ⟶ B₃) (g₃ : B₃ ⟶ B₄) (g₄ : B₄ ⟶ B₅) (α : A₁ ⟶ B₁) (β : A₂ ⟶ B₂) (γ : A₃ ⟶ B₃) (δ : A₄ ⟶ B₄) (ε : A₅ ⟶ B₅) (sq₁ : CategoryTheory.CategoryStruct.comp f₁ β = CategoryTheory.CategoryStruct.comp α g₁) (sq₂ : CategoryTheory.CategoryStruct.comp f₂ γ = CategoryTheory.CategoryStruct.comp β g₂) (sq₃ : CategoryTheory.CategoryStruct.comp f₃ δ = CategoryTheory.CategoryStruct.comp γ g₃) (sq₄ : CategoryTheory.CategoryStruct.comp f₄ ε = CategoryTheory.CategoryStruct.comp δ g₄) (hexTopExact : (CategoryTheory.ComposableArrows.mk₄ f₁ f₂ f₃ f₄).Exact) (hexBotExact : (CategoryTheory.ComposableArrows.mk₄ g₁ g₂ g₃ g₄).Exact) (hα : CategoryTheory.Epi α) (hβ : CategoryTheory.IsIso β) (hδ : CategoryTheory.IsIso δ) (hε : CategoryTheory.Mono ε) : CategoryTheory.IsIso γ

Five-lemma for ModuleCat R: given a ladder of two horizontal 4-term exact sequences with α epi, β, δ iso, ε mono, the middle map γ is an iso. Specialisation of the abelian-category five lemma.

noncomputable def PoincareDuality.cechCohomLES_left (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (K L : Set M) (p : ℕ) : ModuleCat R

The "left tail" of the long exact sequence in Čech cohomology of the triple $(M, K, L)$: the $(p-1)$-st term, used as the source of the connecting map $f_4$ and target of $f_1$.

noncomputable def PoincareDuality.cechCohomLES_f₁ (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (K L : Set M) (p : ℕ) : cechCohomLES_left R M K L p ⟶ cechCohomology R M K ∅ p

First map in the Čech-cohomology long exact sequence of the triple $(M, K, L)$: the connecting map into $\check H^p(M, K; R)$.

noncomputable def PoincareDuality.cechCohomLES_f₂ (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (K L : Set M) (p : ℕ) : cechCohomology R M K ∅ p ⟶ cechCohomology R M K L p

Second map in the Čech-cohomology long exact sequence of the triple: pair-extension $\check H^p(M, K; R) \to \check H^p(M, K, L; R)$.

noncomputable def PoincareDuality.cechCohomLES_f₃ (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (K L : Set M) (p : ℕ) : cechCohomology R M K L p ⟶ cechCohomology R M L ∅ p

Third map in the Čech-cohomology long exact sequence of the triple: restriction $\check H^p(M, K, L; R) \to \check H^p(M, L; R)$.

noncomputable def PoincareDuality.cechCohomLES_f₄ (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (K L : Set M) (p : ℕ) : cechCohomology R M L ∅ p ⟶ cechCohomLES_left R M K L (p + 1)

Fourth map (connecting/coboundary) in the Čech-cohomology long exact sequence of the triple: $\check H^p(M, L; R) \to \check H^{p+1}_{\text{left}}(M, K, L; R)$.

noncomputable def PoincareDuality.singHomolLES_right (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (K L : Set M) (q : ℕ) : ModuleCat R

"Right tail" of the singular-homology long exact sequence of the pair $(M, K, L)$: provides the $(q-1)$-st target/source for the connecting maps $g_1$ and $g_4$.

noncomputable def PoincareDuality.singHomolLES_g₁ (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (K L : Set M) (q : ℕ) : singHomolLES_right R M K L (q + 1) ⟶ relativeSingularHomology R M Kᶜ q

First map in the singular-homology long exact sequence of the pair, going from the right tail in degree $q + 1$ into $H_q(M, K^c; R)$.

noncomputable def PoincareDuality.singHomolLES_g₂ (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (K L : Set M) (q : ℕ) : relativeSingularHomology R M Kᶜ q ⟶ relativeSingularHomology R (↑Lᶜ) (Subtype.val ⁻¹' Kᶜ) q

Second map: $H_q(M, K^c; R) \to H_q(L^c, K^c \cap L^c; R)$, restriction along the open inclusion $L^c \hookrightarrow M$.

noncomputable def PoincareDuality.singHomolLES_g₃ (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (K L : Set M) (q : ℕ) : relativeSingularHomology R (↑Lᶜ) (Subtype.val ⁻¹' Kᶜ) q ⟶ relativeSingularHomology R M Lᶜ q

Third map: $H_q(L^c, K^c \cap L^c; R) \to H_q(M, L^c; R)$, the "next" pair-restriction in the LES.

noncomputable def PoincareDuality.singHomolLES_g₄ (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (K L : Set M) (q : ℕ) : relativeSingularHomology R M Lᶜ q ⟶ singHomolLES_right R M K L q

Fourth map (connecting): $H_q(M, L^c; R) \to \text{right tail at }q$.

noncomputable def PoincareDuality.capProductWithClass (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K L : Set M) (p q : ℕ) (hpq : p + q = n) (μ_K : ↑(relativeSingularHomology R M Kᶜ n)) : cechCohomology R M K L p ⟶ relativeSingularHomology R (↑Lᶜ) (Subtype.val ⁻¹' Kᶜ) q

Cap product with a specific class $\mu_K \in H_n(M, K^c; R)$, going $\check H^p(M, K, L; R) \to H_q(L^c, K^c \cap L^c; R)$.

noncomputable def PoincareDuality.capProductRelativePair (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K L : Set M) [IsROrientedAlong R n M K] (p q : ℕ) (hpq : p + q = n) : cechCohomology R M K L p ⟶ relativeSingularHomology R (↑Lᶜ) (Subtype.val ⁻¹' Kᶜ) q

The relative-pair cap-product, specialised to a chosen fundamental class along $K$ witnessed by IsROrientedAlong R n M K. This is the middle map $\gamma$ of the five-lemma ladder.

noncomputable def PoincareDuality.capProductLES_α (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K L : Set M) [IsROrientedAlong R n M K] (p q : ℕ) (hpq : p + q = n) : cechCohomLES_left R M K L p ⟶ singHomolLES_right R M K L (q + 1)

The cap-product map at the leftmost position of the five-lemma ladder used to deduce the fully-relative iso (Theorem 37.1) from the absolute one.

noncomputable def PoincareDuality.capProductLES_ε (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K L : Set M) [IsROrientedAlong R n M K] (p q : ℕ) (hpq : p + q = n) : cechCohomLES_left R M K L (p + 1) ⟶ singHomolLES_right R M K L q

The cap-product map at the rightmost position of the five-lemma ladder for fully relative Poincaré duality.

theorem PoincareDuality.cechCohomLES_comp_f₁_f₂ (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (K L : Set M) (p : ℕ) : CategoryTheory.CategoryStruct.comp (cechCohomLES_f₁ R M K L p) (cechCohomLES_f₂ R M K L p) = 0

Successive maps $f_1, f_2$ of the Čech-cohomology LES compose to zero.

theorem PoincareDuality.cechCohomLES_comp_f₂_f₃ (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (K L : Set M) (p : ℕ) : CategoryTheory.CategoryStruct.comp (cechCohomLES_f₂ R M K L p) (cechCohomLES_f₃ R M K L p) = 0

Successive maps $f_2, f_3$ of the Čech-cohomology LES compose to zero.

theorem PoincareDuality.cechCohomLES_comp_f₃_f₄ (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (K L : Set M) (p : ℕ) : CategoryTheory.CategoryStruct.comp (cechCohomLES_f₃ R M K L p) (cechCohomLES_f₄ R M K L p) = 0

Successive maps $f_3, f_4$ of the Čech-cohomology LES compose to zero.

theorem PoincareDuality.cechCohomLES_exact₁ (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (K L : Set M) (p : ℕ) : { X₁ := cechCohomLES_left R M K L p, X₂ := cechCohomology R M K ∅ p, X₃ := cechCohomology R M K L p, f := cechCohomLES_f₁ R M K L p, g := cechCohomLES_f₂ R M K L p, zero := ⋯ }.Exact

Exactness at position 1 of the Čech-cohomology LES of the triple $(M, K, L)$.

theorem PoincareDuality.cechCohomLES_exact₂ (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (K L : Set M) (p : ℕ) : { X₁ := cechCohomology R M K ∅ p, X₂ := cechCohomology R M K L p, X₃ := cechCohomology R M L ∅ p, f := cechCohomLES_f₂ R M K L p, g := cechCohomLES_f₃ R M K L p, zero := ⋯ }.Exact

Exactness at position 2 of the Čech-cohomology LES of the triple $(M, K, L)$.

theorem PoincareDuality.cechCohomLES_exact₃ (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (K L : Set M) (p : ℕ) : { X₁ := cechCohomology R M K L p, X₂ := cechCohomology R M L ∅ p, X₃ := cechCohomLES_left R M K L (p + 1), f := cechCohomLES_f₃ R M K L p, g := cechCohomLES_f₄ R M K L p, zero := ⋯ }.Exact

Exactness at position 3 of the Čech-cohomology LES of the triple $(M, K, L)$.

theorem PoincareDuality.cechCohomLES_exact (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (K L : Set M) (p : ℕ) : (CategoryTheory.ComposableArrows.mk₄ (cechCohomLES_f₁ R M K L p) (cechCohomLES_f₂ R M K L p) (cechCohomLES_f₃ R M K L p) (cechCohomLES_f₄ R M K L p)).Exact

Combined statement: the 4-term composable arrow $f_1 \to f_2 \to f_3 \to f_4$ is exact, packaging the three positional exactness lemmas.

theorem PoincareDuality.singHomolLES_exact (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (K L : Set M) (q : ℕ) : (CategoryTheory.ComposableArrows.mk₄ (singHomolLES_g₁ R M K L q) (singHomolLES_g₂ R M K L q) (singHomolLES_g₃ R M K L q) (singHomolLES_g₄ R M K L q)).Exact

Exactness of the 4-term composable arrow $g_1 \to g_2 \to g_3 \to g_4$ in singular homology, i.e. of the LES of the pair $(M, K, L)$.

theorem PoincareDuality.fiveLemmaLadder_sq₁ (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K L : Set M) (hKL : L ⊆ K) (hK : IsCompact K) (hL : IsCompact L) [IsROrientedAlong R n M K] (p q : ℕ) (hpq : p + q = n) (isoK : cechCohomology R M K ∅ p ≅ relativeSingularHomology R M Kᶜ q) : CategoryTheory.CategoryStruct.comp (cechCohomLES_f₁ R M K L p) isoK.hom = CategoryTheory.CategoryStruct.comp (capProductLES_α R n M K L p q hpq) (singHomolLES_g₁ R M K L q)

Commutativity of square 1 in the five-lemma ladder for Theorem 37.1: cap-product with the fundamental class intertwines the leftmost connecting maps of the Čech-cohomology and singular-homology LESs.

theorem PoincareDuality.fiveLemmaLadder_sq₂ (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K L : Set M) (hKL : L ⊆ K) (hK : IsCompact K) (hL : IsCompact L) [IsROrientedAlong R n M K] (p q : ℕ) (hpq : p + q = n) (isoK : cechCohomology R M K ∅ p ≅ relativeSingularHomology R M Kᶜ q) : CategoryTheory.CategoryStruct.comp (cechCohomLES_f₂ R M K L p) (capProductRelativePair R n M K L p q hpq) = CategoryTheory.CategoryStruct.comp isoK.hom (singHomolLES_g₂ R M K L q)

Commutativity of square 2 in the five-lemma ladder for Theorem 37.1.

theorem PoincareDuality.fiveLemmaLadder_sq₃ (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K L : Set M) (hKL : L ⊆ K) (hK : IsCompact K) (hL : IsCompact L) [IsROrientedAlong R n M K] (p q : ℕ) (hpq : p + q = n) (isoL : cechCohomology R M L ∅ p ≅ relativeSingularHomology R M Lᶜ q) : CategoryTheory.CategoryStruct.comp (cechCohomLES_f₃ R M K L p) isoL.hom = CategoryTheory.CategoryStruct.comp (capProductRelativePair R n M K L p q hpq) (singHomolLES_g₃ R M K L q)

Commutativity of square 3 in the five-lemma ladder for Theorem 37.1.

theorem PoincareDuality.fiveLemmaLadder_sq₄ (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K L : Set M) (hKL : L ⊆ K) (hK : IsCompact K) (hL : IsCompact L) [IsROrientedAlong R n M K] (p q : ℕ) (hpq : p + q = n) (isoL : cechCohomology R M L ∅ p ≅ relativeSingularHomology R M Lᶜ q) : CategoryTheory.CategoryStruct.comp (cechCohomLES_f₄ R M K L p) (capProductLES_ε R n M K L p q hpq) = CategoryTheory.CategoryStruct.comp isoL.hom (singHomolLES_g₄ R M K L q)

Commutativity of square 4 in the five-lemma ladder for Theorem 37.1.

theorem PoincareDuality.capProductLES_α_epi (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K L : Set M) (hKL : L ⊆ K) (hK : IsCompact K) (hL : IsCompact L) [IsROrientedAlong R n M K] (hOrL : IsROrientedAlong R n M L) (p q : ℕ) (hpq : p + q = n) (isoK : cechCohomology R M K ∅ p ≅ relativeSingularHomology R M Kᶜ q) (isoL : cechCohomology R M L ∅ p ≅ relativeSingularHomology R M Lᶜ q) : CategoryTheory.Epi (capProductLES_α R n M K L p q hpq)

Left-end leftmost cap-product map is epi. The hypothesis epi-ness needed to invoke the five lemma on the cap-product ladder of Theorem 37.1.

theorem PoincareDuality.capProductLES_ε_mono (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K L : Set M) (hKL : L ⊆ K) (hK : IsCompact K) (hL : IsCompact L) [IsROrientedAlong R n M K] (hOrL : IsROrientedAlong R n M L) (p q : ℕ) (hpq : p + q = n) (isoK : cechCohomology R M K ∅ p ≅ relativeSingularHomology R M Kᶜ q) (isoL : cechCohomology R M L ∅ p ≅ relativeSingularHomology R M Lᶜ q) : CategoryTheory.Mono (capProductLES_ε R n M K L p q hpq)

Right-end cap-product map is mono. The mono-ness needed to invoke the five lemma on the cap-product ladder of Theorem 37.1.

noncomputable def PoincareDuality.fiveLemma_capProduct_reduction (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K L : Set M) (hKL : L ⊆ K) (hK : IsCompact K) (hL : IsCompact L) [hOrK : IsROrientedAlong R n M K] (hOrL : IsROrientedAlong R n M L) (p q : ℕ) (hpq : p + q = n) (isoK : cechCohomology R M K ∅ p ≅ relativeSingularHomology R M Kᶜ q) (isoL : cechCohomology R M L ∅ p ≅ relativeSingularHomology R M Lᶜ q) : cechCohomology R M K L p ≅ relativeSingularHomology R (↑Lᶜ) (Subtype.val ⁻¹' Kᶜ) q

The five-lemma reduction: from absolute Poincaré duality isos at $K$ and $L$, deduce the fully relative Poincaré duality iso at the pair $(K, L)$. The combinatorial core of Theorem 37.1.

noncomputable def PoincareDuality.fullyRelativeCapProductIso (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K L : Set M) (hKL : L ⊆ K) (hK : IsCompact K) (hL : IsCompact L) [hOrK : IsROrientedAlong R n M K] (p q : ℕ) (hpq : p + q = n) : cechCohomology R M K L p ≅ relativeSingularHomology R (↑Lᶜ) (Subtype.val ⁻¹' Kᶜ) q

Theorem 37.1 (Fully relative Poincaré duality, iso form). For a Hausdorff charted $n$-manifold $M$ and $L \subseteq K \subseteq M$ both compact with $M$ $R$-oriented along $K$, there is a natural iso $$\check H^p(M, K, L; R) \cong H_q(L^c, K^c \cap L^c; R)\qquad (p + q = n).$$

noncomputable def PoincareDuality.fullyRelativeCapProduct (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K L : Set M) (hKL : L ⊆ K) (hK : IsCompact K) (hL : IsCompact L) [IsROrientedAlong R n M K] (p q : ℕ) (hpq : p + q = n) : cechCohomology R M K L p ⟶ relativeSingularHomology R (↑Lᶜ) (Subtype.val ⁻¹' Kᶜ) q

The fully relative cap-product morphism, i.e. the hom component of fullyRelativeCapProductIso.

theorem PoincareDuality.fullyRelativeCapProduct_isIso (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K L : Set M) (hKL : L ⊆ K) (hK : IsCompact K) (hL : IsCompact L) [IsROrientedAlong R n M K] (p q : ℕ) (hpq : p + q = n) : CategoryTheory.IsIso (fullyRelativeCapProduct R n M K L hKL hK hL p q hpq)

The fully relative cap-product morphism is an iso, by virtue of being the hom of an iso.

noncomputable def PoincareDuality.poincareDualityCompact (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K : Set M) (hK : IsCompact K) [hOr : IsROrientedAlong R n M K] (p q : ℕ) (hpq : p + q = n) : cechCohomology R M K ∅ p ≅ relativeSingularHomology R M Kᶜ q

Compact Poincaré duality (absolute form): for compact $R$-oriented manifold along $K$, $\check H^p(M, K; R) \cong H_q(M, M-K; R)$ for $p + q = n$. Alias for absoluteCapProductIso.

theorem PoincareDuality.corollary_37_4 (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (K : Set M) (hK : IsCompact K) [hOr : IsROrientedAlong R n M K] (p q : ℕ) (hpq : p + q = n) : CategoryTheory.IsIso (absoluteCapProductIso R n M K hK hOr p q hpq).hom

Corollary 37.4. The absolute cap-product iso is, in particular, an iso (so each direction of Poincaré duality is realised by an actual morphism), packaged as a typeclass.

theorem PoincareDuality.cechCohomology_univ_empty_eq (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (p : ℕ) : cechCohomology R M Set.univ ∅ p = relativeSingularCohomology R M ∅ p

Computational identity: when $K = M$ and $L = \emptyset$, the Čech-cohomology module agrees with the absolute singular cohomology module.

noncomputable def PoincareDuality.cohomAbsoluteToCech (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (p : ℕ) : relativeSingularCohomology R M ∅ p ≅ cechCohomology R M Set.univ ∅ p

The canonical iso turning the equality cechCohomology_univ_empty_eq into a categorical isomorphism. Used to phrase $H^p(M; R) \to \check H^p(M, M; R)$ as an iso.

noncomputable def PoincareDuality.relativeSingularHomology_isoOfHomeo (R : Type) [CommRing R] {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ₜ Y) (A : Set X) (B : Set Y) (hAB : ⇑f '' A = B) (q : ℕ) : relativeSingularHomology R X A q ≅ relativeSingularHomology R Y B q

A homeomorphism $f : X \to Y$ of pairs (sending $A$ onto $B$) induces an isomorphism of relative singular homology modules.

noncomputable def PoincareDuality.homolSubtypeUnivToAbsolute (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (q : ℕ) : relativeSingularHomology R (↑∅ᶜ) (Subtype.val ⁻¹' Set.univᶜ) q ≅ relativeSingularHomology R M ∅ q

Identification $H_q(M^c, M^c \cap \emptyset^c; R) \cong H_q(M; R)$ when $M = M^c$ via the empty-complement convention. Glue iso used in capFundamentalAbsolute.

noncomputable def PoincareDuality.capFundamentalAbsolute (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (p q : ℕ) (hpq : p + q = n) : relativeSingularCohomology R M ∅ p ⟶ relativeSingularHomology R M ∅ q

The absolute cap-product $\cap [M] : H^p(M; R) \to H_q(M; R)$ on a compact $R$-oriented manifold, defined as the composite of cohomAbsoluteToCech, fullyRelativeCapProduct at $(K, L) = (M, \emptyset)$, and the homology bridge.

theorem PoincareDuality.capFundamentalAbsolute_eq_compose (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (p q : ℕ) (hpq : p + q = n) : capFundamentalAbsolute R n M p q hpq = CategoryTheory.CategoryStruct.comp (cohomAbsoluteToCech R M p).hom (CategoryTheory.CategoryStruct.comp (fullyRelativeCapProduct R n M Set.univ ∅ ⋯ ⋯ ⋯ p q hpq) (homolSubtypeUnivToAbsolute R M q).hom)

The defining decomposition of capFundamentalAbsolute, made available as a rewrite lemma for downstream proofs.

noncomputable def PoincareDuality.capFundamental (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (L : Set M) (hL : IsClosed L) (p q : ℕ) (hpq : p + q = n) : cechCohomology R M Set.univ L p ⟶ relativeSingularHomology R ↑Lᶜ ∅ q

The "relative" cap-product $\cap [M] : \check H^p(M, M, L; R) \to H_q(L^c; R)$ for $L$ closed, packaged as a single morphism with the codomain $H_q(L^c; R) = H_q(L^c, \emptyset; R)$. Top row of the Poincaré-duality ladder.

noncomputable def PoincareDuality.capFundamentalSubspace (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (L : Set M) (hL : IsClosed L) (p q : ℕ) (hpq : p + q = n) : cechCohomology R M L ∅ p ⟶ relativeSingularHomology R M Lᶜ q

The "subspace" cap-product $\cap [M] : \check H^p(M, L; R) \to H_q(M, L^c; R)$ for $L$ closed, the bottom row of the Poincaré-duality ladder.

structure PoincareDuality.PoincareDualityLadder (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (L : Set M) (hL : IsClosed L) : Prop

Structure packaging the Poincaré-duality "ladder" for a closed subset $L \subseteq M$: the three cap-products capFundamental, capFundamentalAbsolute, capFundamentalSubspace, each an iso, fitting into commutative squares with the connecting maps (restriction, pair inclusion, boundary) of the long exact sequence of the pair $(M, L)$.

• capRelative_isIso (p q : ℕ) (hpq : p + q = n) : CategoryTheory.IsIso (capFundamental R n M L hL p q hpq)
• capAbsolute_isIso (p q : ℕ) (hpq : p + q = n) : CategoryTheory.IsIso (capFundamentalAbsolute R n M p q hpq)
• capSubspace_isIso (p q : ℕ) (hpq : p + q = n) : CategoryTheory.IsIso (capFundamentalSubspace R n M L hL p q hpq)
• comm_restrict (p q : ℕ) (hpq : p + q = n) : CategoryTheory.CategoryStruct.comp (capFundamental R n M L hL p q hpq) (homolFromOpen R M L q) = CategoryTheory.CategoryStruct.comp (cohomRestriction R M L p) (capFundamentalAbsolute R n M p q hpq)
• comm_subspace (p q : ℕ) (hpq : p + q = n) : CategoryTheory.CategoryStruct.comp (capFundamentalAbsolute R n M p q hpq) (homolToRelative R M L q) = CategoryTheory.CategoryStruct.comp (cohomToSubspace R M L p) (capFundamentalSubspace R n M L hL p q hpq)
• comm_boundary (p q : ℕ) (hpq : p + (q + 1) = n) : CategoryTheory.CategoryStruct.comp (capFundamentalSubspace R n M L hL p (q + 1) hpq) (homolBoundary R M L q) = CategoryTheory.CategoryStruct.comp (cohomCoboundary R M L p) (capFundamental R n M L hL (p + 1) q ⋯)

theorem PoincareDuality.capFundamental_eq_compose (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (L : Set M) (hL : IsClosed L) (p q : ℕ) (hpq : p + q = n) : capFundamental R n M L hL p q hpq = CategoryTheory.CategoryStruct.comp (fullyRelativeCapProduct R n M Set.univ L ⋯ ⋯ ⋯ p q hpq) (CategoryTheory.eqToHom ⋯)

The defining decomposition of capFundamental as the composite of fullyRelativeCapProduct (at $(M, L)$) and a glue iso.

theorem PoincareDuality.capFundamentalSubspace_eq_compose (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (L : Set M) (hL : IsClosed L) (p q : ℕ) (hpq : p + q = n) : capFundamentalSubspace R n M L hL p q hpq = (absoluteCapProductIso R n M L ⋯ ⋯ p q hpq).hom

The defining decomposition of capFundamentalSubspace as the hom of absoluteCapProductIso at $K = L$.

theorem PoincareDuality.comm_restrict_naturality (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (L : Set M) (hL : IsClosed L) (p q : ℕ) (hpq : p + q = n) : CategoryTheory.CategoryStruct.comp (capFundamental R n M L hL p q hpq) (homolFromOpen R M L q) = CategoryTheory.CategoryStruct.comp (cohomRestriction R M L p) (capFundamentalAbsolute R n M p q hpq)

Commutativity of the restriction square in the Poincaré-duality ladder: $\cap [M]$ followed by homolFromOpen equals cohomRestriction followed by capFundamentalAbsolute.

theorem PoincareDuality.comm_subspace_naturality (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (L : Set M) (hL : IsClosed L) (p q : ℕ) (hpq : p + q = n) : CategoryTheory.CategoryStruct.comp (capFundamentalAbsolute R n M p q hpq) (homolToRelative R M L q) = CategoryTheory.CategoryStruct.comp (cohomToSubspace R M L p) (capFundamentalSubspace R n M L hL p q hpq)

Commutativity of the subspace square in the Poincaré-duality ladder.

theorem PoincareDuality.comm_boundary_naturality (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (L : Set M) (hL : IsClosed L) (p q : ℕ) (hpq : p + (q + 1) = n) : CategoryTheory.CategoryStruct.comp (capFundamentalSubspace R n M L hL p (q + 1) hpq) (homolBoundary R M L q) = CategoryTheory.CategoryStruct.comp (cohomCoboundary R M L p) (capFundamental R n M L hL (p + 1) q ⋯)

Commutativity of the boundary/connecting square in the Poincaré-duality ladder.

theorem PoincareDuality.capRelative_isIso_of_thm_37_1 (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (L : Set M) (hL : IsClosed L) (p q : ℕ) (hpq : p + q = n) : CategoryTheory.IsIso (capFundamental R n M L hL p q hpq)

capFundamental is an iso, deduced from Theorem 37.1 (fullyRelativeCapProduct_isIso).

theorem PoincareDuality.capAbsolute_isIso_of_thm_37_1 (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (p q : ℕ) (hpq : p + q = n) : CategoryTheory.IsIso (capFundamentalAbsolute R n M p q hpq)

capFundamentalAbsolute is an iso, deduced from Theorem 37.1 at $(K, L) = (M, \emptyset)$.

theorem PoincareDuality.capSubspace_isIso_of_thm_37_1 (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (L : Set M) (hL : IsClosed L) (p q : ℕ) (hpq : p + q = n) : CategoryTheory.IsIso (capFundamentalSubspace R n M L hL p q hpq)

capFundamentalSubspace is an iso, deduced from absoluteCapProductIso at $K = L$.

theorem PoincareDuality.comm_restrict_of_thm_37_1 (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (L : Set M) (hL : IsClosed L) (p q : ℕ) (hpq : p + q = n) : CategoryTheory.CategoryStruct.comp (capFundamental R n M L hL p q hpq) (homolFromOpen R M L q) = CategoryTheory.CategoryStruct.comp (cohomRestriction R M L p) (capFundamentalAbsolute R n M p q hpq)

Alias for comm_restrict_naturality, exposing it as the "restriction square commutes" input to the Poincaré-duality ladder.

theorem PoincareDuality.comm_subspace_of_thm_37_1 (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (L : Set M) (hL : IsClosed L) (p q : ℕ) (hpq : p + q = n) : CategoryTheory.CategoryStruct.comp (capFundamentalAbsolute R n M p q hpq) (homolToRelative R M L q) = CategoryTheory.CategoryStruct.comp (cohomToSubspace R M L p) (capFundamentalSubspace R n M L hL p q hpq)

Alias for comm_subspace_naturality.

theorem PoincareDuality.comm_boundary_of_thm_37_1 (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (L : Set M) (hL : IsClosed L) (p q : ℕ) (hpq : p + (q + 1) = n) : CategoryTheory.CategoryStruct.comp (capFundamentalSubspace R n M L hL p (q + 1) hpq) (homolBoundary R M L q) = CategoryTheory.CategoryStruct.comp (cohomCoboundary R M L p) (capFundamental R n M L hL (p + 1) q ⋯)

Alias for comm_boundary_naturality.

theorem PoincareDuality.corollary_37_3 (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (L : Set M) (hL : IsClosed L) : PoincareDualityLadder R n M L hL

Corollary 37.3. For any closed $L \subseteq M$ in a compact $R$-oriented $n$-manifold, the Poincaré-duality ladder exists: the three cap-products are isos and the three connecting squares commute.

theorem PoincareDuality.capFundamentalAbsolute_isIso (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (p q : ℕ) (hpq : p + q = n) : CategoryTheory.IsIso (capFundamentalAbsolute R n M p q hpq)

The absolute cap-product is an iso, extracted from the ladder at $L = \emptyset$.

noncomputable def PoincareDuality.corollary_37_3_iso (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (L : Set M) (hL : IsClosed L) (p q : ℕ) (hpq : p + q = n) : cechCohomology R M Set.univ L p ≅ relativeSingularHomology R ↑Lᶜ ∅ q

The iso form of Corollary 37.3 for capFundamental: $\check H^p(M, M, L; R) \cong H_q(L^c; R)$ as an explicit isomorphism.

theorem PoincareDuality.capFundamentalAbsolute_isIso' (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (p q : ℕ) (hpq : p + q = n) : CategoryTheory.IsIso (capFundamentalAbsolute R n M p q hpq)

Alternative iso-form proof of capFundamentalAbsolute_isIso, by directly composing the factors of capFundamentalAbsolute_eq_compose.

theorem PoincareDuality.poincare_duality (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (p q : ℕ) (hpq : p + q = n) : CategoryTheory.IsIso (capFundamentalAbsolute R n M p q hpq)

Poincaré duality (categorical form). For a compact $R$-oriented $n$-manifold, the absolute cap-product $\cap [M] : H^p(M; R) \to H_q(M; R)$ is an iso for $p + q = n$.

noncomputable def PoincareDuality.poincareDualityIso (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (p q : ℕ) (hpq : p + q = n) : relativeSingularCohomology R M ∅ p ≅ relativeSingularHomology R M ∅ q

The iso form of Poincaré duality: $H^p(M; R) \cong H_q(M; R)$ as a categorical isomorphism in ModuleCat R.

noncomputable def PoincareDuality.poincareDualityIso' (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (p : ℕ) (hp : p ≤ n) : relativeSingularCohomology R M ∅ p ≅ relativeSingularHomology R M ∅ (n - p)

Variant of poincareDualityIso using the substitution $q = n - p$: $H^p(M; R) \cong H_{n-p}(M; R)$ for $p \le n$.

theorem PoincareDuality.poincareDuality_finrank_eq (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (p q : ℕ) (hpq : p + q = n) : Module.finrank R ↑(relativeSingularCohomology R M ∅ p) = Module.finrank R ↑(relativeSingularHomology R M ∅ q)

Numerical consequence of Poincaré duality: $\dim_R H^p(M; R) = \dim_R H_q(M; R)$ for $p + q = n$, deduced from poincareDualityIso.

noncomputable def PoincareDuality.universalCoefficientFieldIso (F : Type) [Field F] (X : Type) [TopologicalSpace X] (p : ℕ) : relativeSingularCohomology F X ∅ p ≅ relativeSingularHomology F X ∅ p

Over a field $F$, the universal-coefficient theorem yields a (non-canonical) iso $H^p(X; F) \cong H_p(X; F)$, because Ext groups vanish over a field.

structure PoincareDuality.OpenNhdsOfSet {α : Type u} [TopologicalSpace α] (K : Set α) : Type u

An open neighbourhood of a set $K$: an open subset $U \subseteq \alpha$ together with the inclusion $K \subseteq U$. The indexing category for the Čech-cohomology colimit.

• toOpens : TopologicalSpace.Opens α
• subset_carrier : K ⊆ self.toOpens.carrier

@[implicit_reducible]

instance PoincareDuality.OpenNhdsOfSet.instPreorder {α : Type u} [TopologicalSpace α] {K : Set α} : Preorder (OpenNhdsOfSet K)

Reverse-inclusion preorder: $U \le V$ iff $V \subseteq U$, so that the system of neighbourhoods is directed downward.

instance PoincareDuality.OpenNhdsOfSet.instNonempty {α : Type u} [TopologicalSpace α] {K : Set α} : Nonempty (OpenNhdsOfSet K)

$\alpha$ itself is always an open neighbourhood of $K$, so the type is nonempty.

instance PoincareDuality.OpenNhdsOfSet.instIsDirectedLe {α : Type u} [TopologicalSpace α] {K : Set α} : IsDirected (OpenNhdsOfSet K) fun (x1 x2 : OpenNhdsOfSet K) => x1 ≤ x2

The preorder on open neighbourhoods is directed: any two neighbourhoods admit a common refinement (their intersection).

def PoincareDuality.OpenNhdsOfSet.inclusionFunctorOp {α : Type u} [TopologicalSpace α] {K : Set α} : CategoryTheory.Functor (OpenNhdsOfSet K) (TopologicalSpace.Opens α)ᵒᵖ

Forgetful functor OpenNhdsOfSet K ⥤ (Opens α)ᵒᵖ sending $U$ to its underlying open set, contravariantly: the source for Čech-cohomology colimits over neighbourhoods of $K$.

structure PoincareDuality.CombinedOpenNhds {α : Type u} [TopologicalSpace α] (A : ℕ → Set α) : Type u

An "indexed" open neighbourhood: a pair $(k, U)$ where $U$ is an open neighbourhood of $A_k$. Used to interpolate between the colimits along the family $\{A_k\}$ and the colimit along their intersection, in the proof of Lemma 37.2.

• idx : ℕ
• nhd : OpenNhdsOfSet (A self.idx)

@[implicit_reducible]

instance PoincareDuality.CombinedOpenNhds.instPreorder {α : Type u} [TopologicalSpace α] {A : ℕ → Set α} : Preorder (CombinedOpenNhds A)

Reverse-inclusion preorder on CombinedOpenNhds: $(k, U) \le (k', V)$ iff $V \subseteq U$, ignoring the indices.

instance PoincareDuality.CombinedOpenNhds.instNonempty {α : Type u} [TopologicalSpace α] {A : ℕ → Set α} : Nonempty (CombinedOpenNhds A)

The pair $(0, \top)$ is always a combined open neighbourhood, hence the type is nonempty.

@[reducible]

def PoincareDuality.CombinedOpenNhds.isDirectedOfAntitone {α : Type u} [TopologicalSpace α] {A : ℕ → Set α} (hA : Antitone A) : IsDirected (CombinedOpenNhds A) fun (x1 x2 : CombinedOpenNhds A) => x1 ≤ x2

For an antitone (decreasing) family of subsets $A_k$, the preorder on combined neighbourhoods is directed: take a common refinement index and intersect the neighbourhoods.

def PoincareDuality.CombinedOpenNhds.toNhdsInter {α : Type u} [TopologicalSpace α] {A : ℕ → Set α} (_hA : Antitone A) : CombinedOpenNhds A → OpenNhdsOfSet (⋂ (k : ℕ), A k)

Forgetful map from a combined open neighbourhood $(k, U)$ to an open neighbourhood of the intersection $\bigcap_k A_k$: since $\bigcap_k A_k \subseteq A_k \subseteq U$.

theorem PoincareDuality.CombinedOpenNhds.toNhdsInter_monotone {α : Type u} [TopologicalSpace α] {A : ℕ → Set α} (hA : Antitone A) : Monotone (toNhdsInter hA)

The forgetful map toNhdsInter is monotone with respect to the reverse-inclusion preorders.

theorem PoincareDuality.CombinedOpenNhds.toNhdsInter_cofinal {α : Type u} [TopologicalSpace α] {A : ℕ → Set α} [T2Space α] (hA : Antitone A) (hcpt : ∀ (k : ℕ), IsCompact (A k)) (V : OpenNhdsOfSet (⋂ (k : ℕ), A k)) : ∃ (p : CombinedOpenNhds A), V ≤ toNhdsInter hA p

Cofinality of toNhdsInter: in a Hausdorff space, every open neighbourhood of the intersection $\bigcap_k A_k$ of an antitone family of compacts $A_k$ contains some $A_k$, giving a refinement coming from a combined open neighbourhood.

theorem PoincareDuality.CombinedOpenNhds.toNhdsInter_functor_final {α : Type u} [TopologicalSpace α] {A : ℕ → Set α} [T2Space α] (hA : Antitone A) (hcpt : ∀ (k : ℕ), IsCompact (A k)) : ⋯.functor.Final

Finality of toNhdsInter as a functor: cofinality plus monotonicity in a Hausdorff space ensure that colimits along the combined index agree with colimits along open neighbourhoods of the intersection.

noncomputable def PoincareDuality.CombinedOpenNhds.cechCohomology_colimit_iso {α : Type u} [TopologicalSpace α] [T2Space α] {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (A : ℕ → Set α) (hA : Antitone A) (hcpt : ∀ (k : ℕ), IsCompact (A k)) (F : CategoryTheory.Functor (TopologicalSpace.Opens α)ᵒᵖ C) [CategoryTheory.Limits.HasColimit (OpenNhdsOfSet.inclusionFunctorOp.comp F)] : let G := OpenNhdsOfSet.inclusionFunctorOp.comp F; CategoryTheory.Limits.colimit (⋯.functor.comp G) ≅ CategoryTheory.Limits.colimit G

Lemma 37.2 (categorical core). In a Hausdorff space, for any presheaf $F$ on the opens of $\alpha$ and an antitone family of compacts $A_k$ with intersection $A$, the colimit of $F$ over open neighbourhoods of $A$ is canonically isomorphic to the colimit of $F$ along the combined index built from the $A_k$.

noncomputable def PoincareDuality.CombinedOpenNhds.cechCohomology_colimit_iso_cech {α : Type} [TopologicalSpace α] [T2Space α] (R : Type) [CommRing R] (A : ℕ → Set α) (hA : Antitone A) (hcpt : ∀ (k : ℕ), IsCompact (A k)) (F : CategoryTheory.Functor (TopologicalSpace.Opens α)ᵒᵖ (ModuleCat R)) [CategoryTheory.Limits.HasColimit (OpenNhdsOfSet.inclusionFunctorOp.comp F)] : let G := OpenNhdsOfSet.inclusionFunctorOp.comp F; CategoryTheory.Limits.colimit (⋯.functor.comp G) ≅ CategoryTheory.Limits.colimit G

cechCohomology_colimit_iso specialised to C = ModuleCat.{0} R, the variant used to prove Lemma 37.2 in the Čech-cohomology setting.

theorem CapProduct.poincare_duality (R : Type) [CommRing R] [IsPrincipalIdealRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [PoincareDuality.IsROriented R n M] (p q : ℕ) (hpq : p + q = n) : CategoryTheory.IsIso (PoincareDuality.capFundamentalAbsolute R n M p q hpq)

Corollary 37.5 (cap-product / PID form). Over a PID $R$, for a compact $R$-oriented $n$-manifold $M$, the absolute cap-product map $\cap[M] : H^p(M; R) \to H_q(M; R)$ is an iso for $p + q = n$.

noncomputable def PoincareDualityCompact.cohomologyBridge (R : Type) [CommRing R] [IsPrincipalIdealRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (p : ℕ) : ↑(SingularCohomology.singularCohomology R (TopCat.of M) (ModuleCat.of R R) p) ≃ₗ[R] ↑(PoincareDuality.relativeSingularCohomology R M ∅ p)

Bridge identifying the SingularCohomology.singularCohomology module (used elsewhere in the project) with the relativeSingularCohomology … ∅ module used in this file, as $R$-linear equivalence.

noncomputable def PoincareDualityCompact.homologyBridge (R : Type) [CommRing R] [IsPrincipalIdealRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] (q : ℕ) : ↑(SingularCohomology.singularHomologyModule R (TopCat.of M) q) ≃ₗ[R] ↑(PoincareDuality.relativeSingularHomology R M ∅ q)

Bridge identifying the SingularCohomology.singularHomologyModule module (used elsewhere) with the relativeSingularHomology … ∅ module used in this file, as $R$-linear equivalence.

instance PoincareDualityCompact.isROriented_toPoincareDuality (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [h : IsROriented R n M] : PoincareDuality.IsROriented R n M

An IsROriented instance in the outer namespace promotes to one in PoincareDuality.IsROriented, which is the form used by poincareDualityMap.

theorem PoincareDualityCompact.poincareDualityMap_bridge_comm (R : Type) [CommRing R] [IsPrincipalIdealRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] [PoincareDuality.IsROriented R n M] (p q : ℕ) (hpq : p + q = n) : poincareDualityMap R n M p q hpq = ↑(homologyBridge R n M q).symm ∘ₗ (PoincareDuality.capFundamentalAbsolute R n M p q hpq).hom' ∘ₗ ↑(cohomologyBridge R n M p)

Compatibility: the externally defined poincareDualityMap equals the composite of cohomologyBridge, capFundamentalAbsolute, and the inverse of homologyBridge.

theorem PoincareDualityCompact.poincareDualityMap_bijective_of_isIso (R : Type) [CommRing R] [IsPrincipalIdealRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] [PoincareDuality.IsROriented R n M] (p q : ℕ) (hpq : p + q = n) (hiso : CategoryTheory.IsIso (PoincareDuality.capFundamentalAbsolute R n M p q hpq)) : Function.Bijective ⇑(poincareDualityMap R n M p q hpq)

If capFundamentalAbsolute is an iso, then poincareDualityMap is bijective, by composing with the two bridge equivalences.

theorem PoincareDualityCompact.poincareDualityMap_bijective (R : Type) [CommRing R] [IsPrincipalIdealRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (p q : ℕ) (hpq : p + q = n) : Function.Bijective ⇑(poincareDualityMap R n M p q hpq)

poincareDualityMap is bijective for any compact $R$-oriented $n$-manifold over a PID $R$, obtained by combining poincareDualityMap_bijective_of_isIso with CapProduct.poincare_duality.

noncomputable def PoincareDualityCompact.poincareDualityEquiv (R : Type) [CommRing R] [IsPrincipalIdealRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (p q : ℕ) (hpq : p + q = n) : ↑(SingularCohomology.singularCohomology R (TopCat.of M) (ModuleCat.of R R) p) ≃ₗ[R] ↑(SingularCohomology.singularHomologyModule R (TopCat.of M) q)

Poincaré duality as an explicit $R$-linear equivalence $H^p(M; R) \cong H_q(M; R)$, packaged from poincareDualityMap_bijective.

theorem PoincareDualityZMod2.isROriented_zmod2_of_compact (n : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [CompactSpace M] [T2Space M] : PoincareDuality.IsROriented (ZMod 2) n M

Every compact Hausdorff $n$-manifold is canonically $\mathbb{Z}/2$-oriented, since the mod-$2$ orientation sheaf is always trivial. The basis for unconditional mod-$2$ Poincaré duality on closed manifolds.

theorem PoincareDualityZMod2.capIso_to_cupPerfPair (n : ℕ) (M : Type) [TopologicalSpace M] [AlgebraicTopologyI.TopologicalManifold n M] [CompactSpace M] [PoincareDuality.IsROriented (ZMod 2) n M] (hcap : ∀ (p q : ℕ) (hpq : p + q = n), CategoryTheory.IsIso (PoincareDuality.capFundamentalAbsolute (ZMod 2) n M p q hpq)) : ∃! μ : HomolZMod2 (TopCat.of M) n, ∀ (p q : ℕ) (hpq : p + q = n), (cupProductPairing (TopCat.of M) n μ p q hpq).IsPerfPair

From the absolute cap-product iso (mod $2$), produce a fundamental class $\mu \in H_n(M; \mathbb{Z}/2)$ for which the cup-product pairing $H^p(M; \mathbb{Z}/2) \otimes H^q(M; \mathbb{Z}/2) \to \mathbb{Z}/2$ is a perfect pairing for every $p + q = n$, and show uniqueness of such a class.