theorem BorsukUlam.sphere_isConnected (n : ℕ) (hn : 1 ≤ n) : IsConnected (Metric.sphere 0 1)

The unit sphere in EuclideanSpace ℝ (Fin (n+1)) is connected whenever n ≥ 1, i.e. for spheres of dimension at least one.

def BorsukUlam.F2CohomRPn (n k : ℕ) : Type

The k-th singular cohomology of real projective n-space ℝPⁿ with coefficients in 𝔽₂ = ZMod 2, packaged as a plain Type. Used to set up the Borsuk–Ulam proof via the mod-2 cohomology ring of ℝPⁿ.

@[reducible]

noncomputable instance BorsukUlam.F2CohomRPn.instAddCommGroup (n k : ℕ) : AddCommGroup (F2CohomRPn n k)

The additive commutative group structure on F2CohomRPn n k inherited from its ModuleCat representation.

noncomputable def BorsukUlam.F2CohomRPn.cupProduct (n p q : ℕ) : F2CohomRPn n p → F2CohomRPn n q → F2CohomRPn n (p + q)

The cup product H^p(ℝPⁿ; 𝔽₂) ⊗ H^q(ℝPⁿ; 𝔽₂) → H^{p+q}(ℝPⁿ; 𝔽₂) on mod-2 cohomology of ℝPⁿ, exposed as a binary function on the underlying types.

@[implicit_reducible]

noncomputable instance BorsukUlam.F2CohomRPn.instModule (n k : ℕ) : Module (ZMod 2) (F2CohomRPn n k)

The ZMod 2-module structure on F2CohomRPn n k, inherited from the underlying ModuleCat object.

theorem BorsukUlam.F2CohomRPn.instFree (n k : ℕ) (_hn : n ≥ 1) (_hk : k ≤ n) : Module.Free (ZMod 2) (F2CohomRPn n k)

Every module over the field ZMod 2 is free, so in particular H^k(ℝPⁿ; 𝔽₂) is a free 𝔽₂-module for 1 ≤ n and k ≤ n.

theorem BorsukUlam.F2CohomRPn.finrank_eq_one (n k : ℕ) (hn : n ≥ 1) (hk : k ≤ n) : Module.finrank (ZMod 2) (F2CohomRPn n k) = 1

For 1 ≤ n and k ≤ n, the mod-2 cohomology group H^k(ℝPⁿ; 𝔽₂) is one-dimensional over 𝔽₂. This encodes the standard fact that H^*(ℝPⁿ; 𝔽₂) ≅ 𝔽₂[x]/(x^{n+1}).

theorem BorsukUlam.F2CohomRPn.instFinite (n k : ℕ) (hn : n ≥ 1) (hk : k ≤ n) : Module.Finite (ZMod 2) (F2CohomRPn n k)

Since H^k(ℝPⁿ; 𝔽₂) is free of rank one over 𝔽₂ (for 1 ≤ n and k ≤ n), it is a finite 𝔽₂-module.

noncomputable def BorsukUlam.F2CohomRPn.generator (n : ℕ) (hn : n ≥ 1) : F2CohomRPn n 1

A canonical generator x of the one-dimensional 𝔽₂-vector space H^1(ℝPⁿ; 𝔽₂).

noncomputable def BorsukUlam.F2CohomRPn.generatorPow_zero (n : ℕ) (hn : n ≥ 1) : F2CohomRPn n 0

The canonical generator 1 of H^0(ℝPⁿ; 𝔽₂) ≅ 𝔽₂, i.e. the multiplicative unit of the mod-2 cohomology ring.

noncomputable def BorsukUlam.F2CohomRPn.generatorPow (n k : ℕ) (hn : n ≥ 1) : F2CohomRPn n k

The k-th cup power xᵏ ∈ H^k(ℝPⁿ; 𝔽₂) of the canonical generator x in H^1(ℝPⁿ; 𝔽₂).

noncomputable def BorsukUlam.F2CohomRPn.cohomIsoF2 (n k : ℕ) (hn : n ≥ 1) (hk : k ≤ n) : F2CohomRPn n k ≃+ ZMod 2

The additive isomorphism H^k(ℝPⁿ; 𝔽₂) ≃+ 𝔽₂ for 1 ≤ n and k ≤ n, obtained from the fact that this cohomology group is one-dimensional over 𝔽₂.

theorem BorsukUlam.F2CohomRPn.cohomIsoF2_generatorPow (n k : ℕ) (hn : n ≥ 1) (hk : k ≤ n) : (cohomIsoF2 n k hn hk) (generatorPow n k hn) = 1

Under the additive isomorphism H^k(ℝPⁿ; 𝔽₂) ≃+ 𝔽₂, the cup power xᵏ is sent to the unit 1 ∈ 𝔽₂. In particular xᵏ ≠ 0 for k ≤ n.

theorem BorsukUlam.F2CohomRPn.generatorPow_one (n : ℕ) (hn : n ≥ 1) : generatorPow n 1 hn = generator n hn

The first cup power x¹ agrees with the canonical generator x of H^1(ℝPⁿ; 𝔽₂).

theorem BorsukUlam.F2CohomRPn.generatorPow_ne_zero (n : ℕ) (hn : n ≥ 1) : generatorPow n n hn ≠ 0

The top cup power xⁿ ∈ H^n(ℝPⁿ; 𝔽₂) is nonzero. This is the key nonvanishing fact used in the proof of Borsuk–Ulam.

theorem BorsukUlam.singularHomology_isZero_implies_F2_cochain_exact (X : TopCat) (k : ℕ) (h_homol : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor AddCommGrpCat).obj (AddCommGrpCat.of ℤ)).obj X) k)) : HomologicalComplex.ExactAt (SingularCohomology.singularCochainComplex (ZMod 2) X (ModuleCat.of (ZMod 2) (ZMod 2))) k

If the integral singular homology H_k(X; ℤ) vanishes, then the mod-2 singular cochain complex of X is exact at degree k. A universal-coefficient style transfer of vanishing from homology to cohomology.

theorem BorsukUlam.rpn_singularCochainComplex_exactAt (n k : ℕ) (hk : k > n) : HomologicalComplex.ExactAt (SingularCohomology.singularCochainComplex (ZMod 2) (TopCat.of (RealProjectiveSpace.RPn n)) (ModuleCat.of (ZMod 2) (ZMod 2))) k

For k > n, the mod-2 singular cochain complex of ℝPⁿ is exact at degree k. This is the cohomological vanishing above the dimension of the CW complex ℝPⁿ.

theorem BorsukUlam.F2CohomRPn.vanishing (n k : ℕ) (hk : k > n) : Subsingleton (F2CohomRPn n k)

Vanishing of H^k(ℝPⁿ; 𝔽₂) above the dimension: for k > n, the group has at most one element.

noncomputable def BorsukUlam.F2CohomRPn.cohomologyPullback {n₁ n₂ : ℕ} (f : C(RealProjectiveSpace.RPn n₁, RealProjectiveSpace.RPn n₂)) (k : ℕ) : F2CohomRPn n₂ k →+ F2CohomRPn n₁ k

Functoriality of mod-2 cohomology: a continuous map f : ℝPⁿ¹ → ℝPⁿ² induces an additive pullback f* : H^k(ℝPⁿ²; 𝔽₂) → H^k(ℝPⁿ¹; 𝔽₂).

noncomputable def BorsukUlam.F2CohomRPn.descendedMap (m : ℕ) (hm : m ≥ 2) (g : C(↑(Metric.sphere 0 1), ↑(Metric.sphere 0 1))) (hg : ∀ (x : ↑(Metric.sphere 0 1)), g (-x) = -g x) : C(RealProjectiveSpace.RPn m, RealProjectiveSpace.RPn (m - 1))

An antipodal-preserving continuous map g : Sᵐ → Sᵐ⁻¹ descends to the quotient by the antipodal action to yield a continuous map ℝPᵐ → ℝPᵐ⁻¹. Defined for m ≥ 2.

noncomputable def BorsukUlam.F2CohomRPn.pullback (m : ℕ) (hm : m ≥ 2) (g : C(↑(Metric.sphere 0 1), ↑(Metric.sphere 0 1))) (hg : ∀ (x : ↑(Metric.sphere 0 1)), g (-x) = -g x) (k : ℕ) : F2CohomRPn (m - 1) k →+ F2CohomRPn m k

The cohomology pullback H^k(ℝPᵐ⁻¹; 𝔽₂) → H^k(ℝPᵐ; 𝔽₂) induced by an odd map g : Sᵐ → Sᵐ⁻¹ via its descent ℝPᵐ → ℝPᵐ⁻¹.

theorem BorsukUlam.F2CohomRPn.descendedMap_pullback_generator (m : ℕ) (hm : m ≥ 2) (g : C(↑(Metric.sphere 0 1), ↑(Metric.sphere 0 1))) (hg : ∀ (x : ↑(Metric.sphere 0 1)), g (-x) = -g x) (hm1 : m - 1 ≥ 1) : (cohomologyPullback (descendedMap m hm g hg) 1) (generator (m - 1) hm1) = generator m ⋯

The descended map of an odd g : Sᵐ → Sᵐ⁻¹ pulls the canonical degree-1 mod-2 cohomology generator of ℝPᵐ⁻¹ back to the canonical degree-1 generator of ℝPᵐ.

theorem BorsukUlam.F2CohomRPn.descendedMap_pullback_ne_zero (m : ℕ) (hm : m ≥ 2) (g : C(↑(Metric.sphere 0 1), ↑(Metric.sphere 0 1))) (hg : ∀ (x : ↑(Metric.sphere 0 1)), g (-x) = -g x) : cohomologyPullback (descendedMap m hm g hg) 1 ≠ 0

The pullback map on H^1 induced by the descent of an odd g : Sᵐ → Sᵐ⁻¹ is nonzero: it sends the canonical generator to a nonzero class.

theorem BorsukUlam.F2CohomRPn.pullback_generator_ne_zero_ax (m : ℕ) (hm : m ≥ 2) (g : C(↑(Metric.sphere 0 1), ↑(Metric.sphere 0 1))) (hg : ∀ (x : ↑(Metric.sphere 0 1)), g (-x) = -g x) (hm1 : m - 1 ≥ 1) : (pullback m hm g hg 1) (generator (m - 1) hm1) ≠ 0

Auxiliary version of pullback_generator_ne_zero proved directly from the descendedMap_pullback_ne_zero lemma, before being repackaged.

theorem BorsukUlam.F2CohomRPn.pullback_generator_ne_zero (m : ℕ) (hm : m ≥ 2) (g : C(↑(Metric.sphere 0 1), ↑(Metric.sphere 0 1))) (hg : ∀ (x : ↑(Metric.sphere 0 1)), g (-x) = -g x) (hm1 : m - 1 ≥ 1) : (pullback m hm g hg 1) (generator (m - 1) hm1) ≠ 0

The pullback along the descent of an odd g : Sᵐ → Sᵐ⁻¹ sends the canonical generator of H^1(ℝPᵐ⁻¹; 𝔽₂) to a nonzero element of H^1(ℝPᵐ; 𝔽₂).

theorem BorsukUlam.F2CohomRPn.pullback_generator (m : ℕ) (hm : m ≥ 2) (g : C(↑(Metric.sphere 0 1), ↑(Metric.sphere 0 1))) (hg : ∀ (x : ↑(Metric.sphere 0 1)), g (-x) = -g x) (hm1 : m - 1 ≥ 1) : (pullback m hm g hg 1) (generator (m - 1) hm1) = generator m ⋯

The pullback along the descent of an odd g : Sᵐ → Sᵐ⁻¹ sends the canonical generator of H^1(ℝPᵐ⁻¹; 𝔽₂) exactly to the canonical generator of H^1(ℝPᵐ; 𝔽₂).

theorem BorsukUlam.F2CohomRPn.singularCohomologyMap_degree0_isIso (n₁ n₂ : ℕ) (hn₁ : n₁ ≥ 1) (hn₂ : n₂ ≥ 1) (f : C(RealProjectiveSpace.RPn n₂, RealProjectiveSpace.RPn n₁)) : CategoryTheory.IsIso (SingularCohomology.singularCohomologyMap (ZMod 2) (TopCat.ofHom f) 0)

Any continuous map ℝPⁿ² → ℝPⁿ¹ induces an isomorphism on mod-2 cohomology in degree 0. Both groups are isomorphic to 𝔽₂ and the map preserves the unit.

theorem BorsukUlam.F2CohomRPn.cohomologyPullback_unit_ne_zero (n₁ n₂ : ℕ) (hn₁ : n₁ ≥ 1) (hn₂ : n₂ ≥ 1) (f : C(RealProjectiveSpace.RPn n₂, RealProjectiveSpace.RPn n₁)) : (cohomologyPullback f 0) (generatorPow n₁ 0 hn₁) ≠ 0

The cohomology pullback of the multiplicative unit 1 ∈ H^0(ℝPⁿ¹; 𝔽₂) along any continuous map f : ℝPⁿ² → ℝPⁿ¹ is nonzero.

theorem BorsukUlam.F2CohomRPn.cohomologyPullback_preserves_unit (n₁ n₂ : ℕ) (hn₁ : n₁ ≥ 1) (hn₂ : n₂ ≥ 1) (f : C(RealProjectiveSpace.RPn n₂, RealProjectiveSpace.RPn n₁)) : (cohomologyPullback f 0) (generatorPow n₁ 0 hn₁) = generatorPow n₂ 0 hn₂

The cohomology pullback along f : ℝPⁿ² → ℝPⁿ¹ sends the multiplicative unit of H^0(ℝPⁿ¹; 𝔽₂) to the multiplicative unit of H^0(ℝPⁿ²; 𝔽₂).

theorem BorsukUlam.F2CohomRPn.generatorPow_succ (n k : ℕ) (hn : n ≥ 1) : generatorPow n (k + 1) hn = cupProduct n k 1 (generatorPow n k hn) (generator n hn)

Unfolding identity: the (k+1)-th cup power equals the cup product of the k-th cup power with the generator x.

theorem BorsukUlam.SingularCohomology.cupProduct_naturality_hom (R : Type) [CommRing R] {X Y : TopCat} (f : X ⟶ Y) (p q : ℕ) : CategoryTheory.CategoryStruct.comp (SingularCohomology.cupProduct R Y p q) (SingularCohomology.singularCohomologyMap R f (p + q)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (SingularCohomology.singularCohomologyMap R f p) (SingularCohomology.singularCohomologyMap R f q)) (SingularCohomology.cupProduct R X p q)

Naturality of the cup product: for f : X ⟶ Y, the diagram (cup on Y) ∘ f* = f* ⊗ f* ∘ (cup on X) commutes.

theorem BorsukUlam.F2CohomRPn.cohomologyPullback_preserves_cupProduct (n₁ n₂ : ℕ) (f : C(RealProjectiveSpace.RPn n₂, RealProjectiveSpace.RPn n₁)) (p q : ℕ) (α : F2CohomRPn n₁ p) (β : F2CohomRPn n₁ q) : (cohomologyPullback f (p + q)) (cupProduct n₁ p q α β) = cupProduct n₂ p q ((cohomologyPullback f p) α) ((cohomologyPullback f q) β)

Naturality of the cup product on mod-2 cohomology of real projective spaces: f*(α ∪ β) = f* α ∪ f* β.

theorem BorsukUlam.F2CohomRPn.cohomologyPullback_preserves_generatorPow (n₁ n₂ : ℕ) (hn₁ : n₁ ≥ 1) (hn₂ : n₂ ≥ 1) (f : C(RealProjectiveSpace.RPn n₂, RealProjectiveSpace.RPn n₁)) (hf : (cohomologyPullback f 1) (generator n₁ hn₁) = generator n₂ hn₂) (k : ℕ) : (cohomologyPullback f k) (generatorPow n₁ k hn₁) = generatorPow n₂ k hn₂

If a map f : ℝPⁿ² → ℝPⁿ¹ sends the degree-1 generator to the degree-1 generator, then by naturality of cup products it sends every cup power xᵏ to xᵏ.

theorem BorsukUlam.F2CohomRPn.pullback_generatorPow (m : ℕ) (hm : m ≥ 2) (g : C(↑(Metric.sphere 0 1), ↑(Metric.sphere 0 1))) (hg : ∀ (x : ↑(Metric.sphere 0 1)), g (-x) = -g x) (k : ℕ) (hm1 : m - 1 ≥ 1) : (pullback m hm g hg k) (generatorPow (m - 1) k hm1) = generatorPow m k ⋯

For every k, the pullback induced by an odd g : Sᵐ → Sᵐ⁻¹ sends the k-th cup power xᵏ ∈ H^k(ℝPᵐ⁻¹; 𝔽₂) to xᵏ ∈ H^k(ℝPᵐ; 𝔽₂).

theorem BorsukUlam.no_odd_map_sphere (n : ℕ) (g : C(↑(Metric.sphere 0 1), ↑(Metric.sphere 0 1))) (hg : ∀ (x : ↑(Metric.sphere 0 1)), g (-x) = -g x) : False

There is no continuous odd map Sⁿ⁺² → Sⁿ⁺¹. The proof uses the nonvanishing of the top cup power xⁿ⁺² ∈ H^{n+2}(ℝPⁿ⁺²; 𝔽₂) together with the vanishing of H^{n+2}(ℝPⁿ⁺¹; 𝔽₂). This is the key step in Borsuk–Ulam for dimensions ≥ 2.

theorem BorsukUlam.borsuk_ulam_ge2 (n : ℕ) (f : C(↑(Metric.sphere 0 1), EuclideanSpace ℝ (Fin (n + 2)))) : ∃ (x : ↑(Metric.sphere 0 1)), f x = f (-x)

Borsuk–Ulam in dimensions ≥ 2: every continuous map Sⁿ⁺² → ℝⁿ⁺² identifies some pair of antipodal points, i.e. there exists x with f x = f (-x). Deduced from no_odd_map_sphere by normalising f x - f (-x) to a hypothetical odd map to the sphere.

theorem BorsukUlam.borsuk_ulam (n : ℕ) (f : C(↑(Metric.sphere 0 1), EuclideanSpace ℝ (Fin n))) : ∃ (x : ↑(Metric.sphere 0 1)), f x = f (-x)

The Borsuk–Ulam theorem (Theorem 38.11). Thinking of Sⁿ as the unit vectors in ℝⁿ⁺¹, every continuous function f : Sⁿ → ℝⁿ admits a point x ∈ Sⁿ with f x = f (-x). Proved by cases: n = 0 (sphere is two-point), n = 1 (intermediate value theorem on the circle), n ≥ 2 (borsuk_ulam_ge2).

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

Poincaré–Lefschetz duality (Theorem 38.1) for an R-oriented d-manifold along a compact set K: capping with the fundamental class [M]_K gives an isomorphism Ȟ^p(K; R) ≅ H_q(M, M\K; R) whenever p + q = d.

theorem PoincareDuality.cech_cohomology_vanishing (R : Type) [CommRing R] (d : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin d)) M] (K : Set M) (hK : IsCompact K) [IsROrientedAlong R d M K] (p : ℕ) (hp : p > d) : Subsingleton ↑(cechCohomology R M K ∅ p)

Corollary 38.2: for K a compact subset of an R-oriented d-manifold and p > d, the Čech cohomology Ȟ^p(K; R) vanishes.

theorem PoincareDuality.cechCohomology_subsingleton_of_gt_dim (R : Type) [CommRing R] (d : ℕ) (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin d)) M] [IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin d))) 0 M] (K : Set M) (hK : IsCompact K) (p : ℕ) (hp : p > d) : Subsingleton ↑(cechCohomology R M K ∅ p)

Variant of Corollary 38.2 expressed for any C⁰ d-manifold (with no orientation hypothesis): for a compact set K and p > d, Ȟ^p(K; R) is a subsingleton.

def PoincareDuality.ReducedSingularHomology (R : Type) [CommRing R] (X : Type) [TopologicalSpace X] (q : ℕ) : Type

Reduced singular homology \widetilde H_q(X; R): in degree zero it is the kernel of the augmentation H_0(X; R) → R, and in higher degrees it agrees with the usual singular homology.

@[implicit_reducible]

noncomputable instance PoincareDuality.ReducedSingularHomology.instAddCommGroup (R : Type) [CommRing R] (X : Type) [TopologicalSpace X] (q : ℕ) : AddCommGroup (ReducedSingularHomology R X q)

The additive commutative group structure on reduced singular homology, inherited from the augmentation kernel (degree 0) or from singular homology (higher degrees).

@[implicit_reducible]

noncomputable instance PoincareDuality.ReducedSingularHomology.instModule (R : Type) [CommRing R] (X : Type) [TopologicalSpace X] (q : ℕ) : Module R (ReducedSingularHomology R X q)

The R-module structure on reduced singular homology.

@[reducible, inline]

abbrev PoincareDuality.SphereType (n : ℕ) : Type

Convenient abbreviation for the unit sphere Sⁿ ⊂ ℝⁿ⁺¹ viewed as a subtype.

theorem PoincareDuality.cech_cohomology_sphere_complement_iso (R : Type) [CommRing R] {n : ℕ} (K : Set (SphereType n)) (hK : IsCompact K) (q : ℕ) (hq : q ≥ 1) (hqn : q ≤ n - 1) : Nonempty (↑(cechCohomology R (SphereType n) K ∅ q) ≃ₗ[R] ReducedSingularHomology R (↑Kᶜ) (n - q - 1))

Alexander duality on the sphere: for K compact in Sⁿ and 1 ≤ q ≤ n - 1, the Čech cohomology Ȟ^q(K; R) is isomorphic to the reduced singular homology \widetilde H_{n-q-1}(Sⁿ \ K; R).

theorem PoincareDuality.euclideanSpace_isROrientedAlong_univ (R : Type) [CommRing R] {n : ℕ} : IsROrientedAlong R n (EuclideanSpace ℝ (Fin n)) Set.univ

Euclidean space ℝⁿ is R-orientable along the whole space univ; equivalently, it carries a global R-orientation.

theorem PoincareDuality.euclideanSpace_isROrientedAlong (R : Type) [CommRing R] {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n))) : IsROrientedAlong R n (EuclideanSpace ℝ (Fin n)) K

Euclidean space ℝⁿ is R-orientable along any subset K, obtained by restricting the global orientation from univ.

theorem PoincareDuality.euclideanSpace_reduced_homology_vanishes (R : Type) [CommRing R] {n : ℕ} (q : ℕ) : Subsingleton (ReducedSingularHomology R (EuclideanSpace ℝ (Fin n)) q)

Reduced singular homology of contractible Euclidean space vanishes in every degree: \widetilde H_q(ℝⁿ; R) = 0.

noncomputable def PoincareDuality.les_boundary_iso_of_acyclic_ambient (R : Type) [CommRing R] {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n))) (hK : IsCompact K) (q : ℕ) (hAcyclic : ∀ (q : ℕ), Subsingleton (ReducedSingularHomology R (EuclideanSpace ℝ (Fin n)) q)) : ↑(relativeSingularHomology R (↑∅ᶜ) (Subtype.val ⁻¹' Kᶜ) q) ≃ₗ[R] ReducedSingularHomology R (↑Kᶜ) (q - 1)

Boundary isomorphism from the long exact sequence of the pair (ℝⁿ, ℝⁿ \ K) when the ambient space is acyclic: H_q(ℝⁿ, ℝⁿ \ K; R) ≃ \widetilde H_{q-1}(ℝⁿ \ K; R).

noncomputable def PoincareDuality.les_boundary_iso_from_acyclicity (R : Type) [CommRing R] {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n))) (hK : IsCompact K) (q : ℕ) : ↑(relativeSingularHomology R (↑∅ᶜ) (Subtype.val ⁻¹' Kᶜ) q) ≃ₗ[R] ReducedSingularHomology R (↑Kᶜ) (q - 1)

Specialisation of les_boundary_iso_of_acyclic_ambient to Euclidean space, whose reduced homology vanishes in every degree.

noncomputable def PoincareDuality.alexander_duality_edge_case (R : Type) [CommRing R] {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n))) (hK : IsCompact K) (q : ℕ) (hqn : n < q) : ↑(cechCohomology R (EuclideanSpace ℝ (Fin n)) K ∅ (n - q)) ≃ₗ[R] ReducedSingularHomology R (↑Kᶜ) (q - 1)

Edge case of Alexander duality when q > n: both sides vanish, so an isomorphism between them exists trivially.

noncomputable def PoincareDuality.alexander_duality (R : Type) [CommRing R] {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n))) (hK : IsCompact K) (q : ℕ) : ↑(cechCohomology R (EuclideanSpace ℝ (Fin n)) K ∅ (n - q)) ≃ₗ[R] ReducedSingularHomology R (↑Kᶜ) (q - 1)

Alexander duality (Theorem 38.4): for a compact subset K of ℝⁿ, the composite of the Poincaré duality cap product and the long exact sequence boundary gives an isomorphism Ȟ^{n-q}(K; R) ≅ \widetilde H_{q-1}(ℝⁿ \ K; R).

noncomputable def PoincareDuality.alexander_duality_equiv (R : Type) [CommRing R] {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n))) (hK : IsCompact K) (q : ℕ) (hqn : q ≤ n) : ↑(cechCohomology R (EuclideanSpace ℝ (Fin n)) K ∅ (n - q)) ≃ₗ[R] ReducedSingularHomology R (↑Kᶜ) (q - 1)

The main range of Alexander duality (q ≤ n) extracted as a separate construction that avoids case-splitting on q vs n.

@[reducible, inline]

abbrev PoincareDuality.singularCohomologyType (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (p : ℕ) : Type

Convenient Type view of singular cohomology H^p(M; R), defined here as the relative cohomology against the empty pair.

@[reducible, inline]

abbrev PoincareDuality.singularHomologyType (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (q : ℕ) : Type

Convenient Type view of singular homology H_q(M; R), defined here as the relative homology against the empty pair.

noncomputable def PoincareDuality.cohomologyBridgeEquiv (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (n : ℕ) : singularCohomologyType R M n ≃ₗ[R] ↑(SingularCohomology.singularCohomology R (TopCat.of M) (ModuleCat.of R R) n)

Bridge equivalence between the relative cohomology against the empty pair and the absolute singular cohomology object used elsewhere in the library.

noncomputable def PoincareDuality.homologyBridgeEquiv (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (n : ℕ) : singularHomologyType R M n ≃ₗ[R] ↑(SingularCohomology.singularHomologyModule R (TopCat.of M) n)

Bridge equivalence between the relative homology against the empty pair and the absolute singular homology module used elsewhere in the library.

noncomputable def PoincareDuality.cupProductAbsolute (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (p q : ℕ) : singularCohomologyType R M p →ₗ[R] singularCohomologyType R M q →ₗ[R] singularCohomologyType R M (p + q)

The absolute cup product on singular cohomology, transported via the bridge equivalences to singularCohomologyType.

noncomputable def PoincareDuality.kroneckerPairingAbsolute (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (n : ℕ) : singularCohomologyType R M n →ₗ[R] singularHomologyType R M n →ₗ[R] R

The absolute Kronecker pairing H^n(M; R) × H_n(M; R) → R transported via the bridge equivalences.

noncomputable def PoincareDuality.fundamentalClass (R : Type) [CommRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] : singularHomologyType R M n

The fundamental class [M] ∈ H_n(M; R) of a compact R-oriented n-manifold, chosen via the existence statement fundamentalClass_of_isROrientable.

noncomputable def PoincareDuality.cupProductPairingRaw (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) : singularCohomologyType R M p →ₗ[R] singularCohomologyType R M q →ₗ[R] R

The raw cup-product pairing H^p(M; R) × H^q(M; R) → R, defined by a ⊗ b ↦ ⟨a ∪ b, [M]⟩, before quotienting by torsion.

theorem PoincareDuality.cupProductPairingRaw_torsion_left (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) : Submodule.torsion R (singularCohomologyType R M p) ≤ (cupProductPairingRaw R n M p q hpq).ker

The raw cup-product pairing kills torsion on the left: torsion classes in H^p(M; R) lie in the left kernel of the pairing.

theorem PoincareDuality.cupProductPairingRaw_torsion_right (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) : Submodule.torsion R (singularCohomologyType R M q) ≤ (cupProductPairingRaw R n M p q hpq).flip.ker

The raw cup-product pairing kills torsion on the right: torsion classes in H^q(M; R) lie in the right kernel of the pairing.

noncomputable def PoincareDuality.cupProductPairingModTorsion (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) : singularCohomologyType R M p ⧸ Submodule.torsion R (singularCohomologyType R M p) →ₗ[R] singularCohomologyType R M q ⧸ Submodule.torsion R (singularCohomologyType R M q) →ₗ[R] R

The cup-product pairing descended modulo torsion: it induces a pairing on H^p(M; R)/tors × H^q(M; R)/tors → R over any PID R. This is the pairing that appears in Theorem 38.8.

theorem PoincareDuality.isPerfPair_compl₂ {R : Type u_1} {M : Type u_2} {N : Type u_3} {N' : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup N'] [Module R M] [Module R N] [Module R N'] (p : M →ₗ[R] N →ₗ[R] R) (e : N' ≃ₗ[R] N) [hp : p.IsPerfPair] : (p.compl₂ ↑e).IsPerfPair

Perfect pairings are preserved under post-composition on the right by a linear equivalence: if p : M × N → R is a perfect pairing and e : N' ≃ N, then p.compl₂ e is also a perfect pairing.

theorem PoincareDuality.kroneckerPairingAbsolute_torsion_left (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (p : ℕ) : Submodule.torsion R (singularCohomologyType R M p) ≤ (kroneckerPairingAbsolute R M p).ker

The Kronecker pairing kills torsion on the cohomology side: torsion classes in H^p(M; R) lie in the left kernel of the Kronecker pairing.

theorem PoincareDuality.kroneckerPairingAbsolute_torsion_right (R : Type) [CommRing R] (M : Type) [TopologicalSpace M] (p : ℕ) : Submodule.torsion R (singularHomologyType R M p) ≤ (kroneckerPairingAbsolute R M p).flip.ker

The Kronecker pairing kills torsion on the homology side: torsion classes in H_p(M; R) lie in the right kernel of the Kronecker pairing.

noncomputable def PoincareDuality.kroneckerPairingModTorsion (R : Type) [CommRing R] [IsPrincipalIdealRing R] (M : Type) [TopologicalSpace M] (p : ℕ) : singularCohomologyType R M p ⧸ Submodule.torsion R (singularCohomologyType R M p) →ₗ[R] singularHomologyType R M p ⧸ Submodule.torsion R (singularHomologyType R M p) →ₗ[R] R

The Kronecker pairing descended modulo torsion on both sides, yielding a pairing H^p(M; R)/tors × H_p(M; R)/tors → R over a PID.

theorem PoincareDuality.ext1_isTorsion_over_PID (R : Type) [CommRing R] [IsPrincipalIdealRing R] (A : ModuleCat R) (x : ↑(((Ext R (ModuleCat R) 1).obj (Opposite.op A)).obj (ModuleCat.of R R))) : ∃ (r : R), r ≠ 0 ∧ r • x = 0

Over a PID, every element of Ext^1_R(A, R) is torsion: for each x there is a nonzero r ∈ R with r • x = 0. This is used in the universal coefficient argument behind the Poincaré duality / Kronecker pairing modulo torsion.

theorem PoincareDuality.kroneckerPairingAbsolute_surjective (R : Type) [CommRing R] [IsPrincipalIdealRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (p : ℕ) : Function.Surjective ⇑(kroneckerPairingAbsolute R M p)

Over a PID and on a compact R-oriented manifold, the absolute Kronecker map H^p(M; R) → Hom(H_p(M; R), R) is surjective.

theorem PoincareDuality.kroneckerPairingAbsolute_ker_le_torsion (R : Type) [CommRing R] [IsPrincipalIdealRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (p : ℕ) : (kroneckerPairingAbsolute R M p).ker ≤ Submodule.torsion R (singularCohomologyType R M p)

Over a PID and on a compact R-oriented manifold, the kernel of the absolute Kronecker map equals exactly the torsion of H^p(M; R).

theorem PoincareDuality.kroneckerPairingModTorsion_surjective (R : Type) [CommRing R] [IsPrincipalIdealRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (p : ℕ) : Function.Surjective ⇑(kroneckerPairingModTorsion R M p)

The Kronecker pairing modulo torsion is surjective onto Hom(H_p(M; R)/tors, R).

theorem PoincareDuality.kroneckerPairingModTorsion_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 : ℕ) : Function.Bijective ⇑(kroneckerPairingModTorsion R M p)

The Kronecker pairing modulo torsion is bijective: it identifies H^p(M; R)/tors with the dual of H_p(M; R)/tors.

noncomputable def PoincareDuality.kroneckerPairingModTorsion_equiv (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 : ℕ) : (singularCohomologyType R M p ⧸ Submodule.torsion R (singularCohomologyType R M p)) ≃ₗ[R] singularHomologyType R M p ⧸ Submodule.torsion R (singularHomologyType R M p) →ₗ[R] R

The Kronecker pairing modulo torsion packaged as a linear equivalence H^p(M; R)/tors ≃ₗ Hom(H_p(M; R)/tors, R).

theorem PoincareDuality.kroneckerPairingModTorsion_equiv_eq (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 : ℕ) : ⇑(kroneckerPairingModTorsion_equiv R n M p) = ⇑(kroneckerPairingModTorsion R M p)

The underlying function of kroneckerPairingModTorsion_equiv is just the Kronecker pairing modulo torsion.

theorem PoincareDuality.singularHomologyModTorsion_isReflexive (R : Type) [CommRing R] [IsPrincipalIdealRing R] (n : ℕ) (M : Type) [TopologicalSpace M] [CompactSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsROriented R n M] (p : ℕ) : Module.IsReflexive R (singularHomologyType R M p ⧸ Submodule.torsion R (singularHomologyType R M p))

On a compact R-oriented manifold over a PID, the torsion-free quotient of singular homology H_p(M; R)/tors is a reflexive R-module.

noncomputable def PoincareDuality.kroneckerPairingModTorsion_equiv_flip (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 : ℕ) : (singularHomologyType R M p ⧸ Submodule.torsion R (singularHomologyType R M p)) ≃ₗ[R] singularCohomologyType R M p ⧸ Submodule.torsion R (singularCohomologyType R M p) →ₗ[R] R

The "flipped" version of kroneckerPairingModTorsion_equiv, identifying H_p(M; R)/tors with the dual of H^p(M; R)/tors using reflexivity.

theorem PoincareDuality.kroneckerPairingModTorsion_equiv_flip_eq (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 : ℕ) : ⇑(kroneckerPairingModTorsion_equiv_flip R n M p) = ⇑(kroneckerPairingModTorsion R M p).flip

The underlying function of the flipped Kronecker equivalence equals the flipped Kronecker pairing modulo torsion.

theorem PoincareDuality.kroneckerPairingModTorsion_isPerfPair (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 : ℕ) : (kroneckerPairingModTorsion R M p).IsPerfPair

The Kronecker pairing modulo torsion is a perfect pairing on a compact R-oriented manifold over a PID.

noncomputable def PoincareDuality.poincareDuality_modTorsion_equiv (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) : (singularCohomologyType R M q ⧸ Submodule.torsion R (singularCohomologyType R M q)) ≃ₗ[R] singularHomologyType R M p ⧸ Submodule.torsion R (singularHomologyType R M p)

Poincaré duality descended modulo torsion: an R-linear equivalence H^q(M; R)/tors ≃ₗ H_p(M; R)/tors for p + q = n on a compact R-oriented manifold.

theorem PoincareDuality.poincareDualityIso_bridge_compat (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) (hqp : q + p = n := by omega) (b : singularCohomologyType R M q) : (homologyBridgeEquiv R M p) ((poincareDualityIso R n M q p ⋯).toLinearEquiv b) = ((CapProduct.capProduct R (TopCat.of M) q p) ((cohomologyBridgeEquiv R M q) b)) (⋯ ▸ (homologyBridgeEquiv R M (p + q)) (⋯ ▸ fundamentalClass R n M))

Compatibility of the Poincaré duality isomorphism with the cohomology/homology bridge equivalences: applying the bridge map after Poincaré duality equals capping with the (transported) fundamental class.

theorem PoincareDuality.cupCapIdentityRaw (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) (a : singularCohomologyType R M p) (b : singularCohomologyType R M q) : ((cupProductPairingRaw R n M p q hpq) a) b = ((kroneckerPairingAbsolute R M p) a) ((poincareDualityIso R n M q p ⋯).toLinearEquiv b)

The cup–cap identity at the raw (pre-quotient) level: ⟨a ∪ b, [M]⟩ = ⟨a, PD(b)⟩, expressing the cup-product pairing as the Kronecker pairing composed with Poincaré duality.

theorem PoincareDuality.cupProductPairing_eq_kronecker_comp_PD (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) : cupProductPairingModTorsion R n M p q hpq = (kroneckerPairingModTorsion R M p).compl₂ ↑(poincareDuality_modTorsion_equiv R n M p q hpq)

The cup-product pairing modulo torsion equals the Kronecker pairing composed with Poincaré duality (modulo torsion), pair_cup = pair_kron ∘ PD.

theorem PoincareDuality.cupProductPairing_factorsAsPerfPairCompl₂ (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) : ∃ (N : Type) (x : AddCommGroup N) (x_1 : Module R N) (pairing : singularCohomologyType R M p ⧸ Submodule.torsion R (singularCohomologyType R M p) →ₗ[R] N →ₗ[R] R) (_ : pairing.IsPerfPair) (e : (singularCohomologyType R M q ⧸ Submodule.torsion R (singularCohomologyType R M q)) ≃ₗ[R] N), cupProductPairingModTorsion R n M p q hpq = pairing.compl₂ ↑e

The cup-product pairing modulo torsion factors as pair.compl₂ e for some perfect pairing pair and linear equivalence e. This is the structural fact used to deduce that the cup-product pairing itself is perfect.

theorem PoincareDuality.cupProductPairingModTorsion_isPerfPair (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) : (cupProductPairingModTorsion R n M p q hpq).IsPerfPair

Theorem 38.8 (perfect-pairing form of Poincaré duality): for a compact R-oriented n-manifold M over a PID R, the cup-product pairing H^p(M; R)/tors × H^q(M; R)/tors → R (with p + q = n) is a perfect pairing.

theorem AlexanderDuality.reducedSingularHomology_neg_one_subsingleton (R : Type) [CommRing R] {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n))) (hK : IsCompact K) : Subsingleton (PoincareDuality.ReducedSingularHomology R (↑Kᶜ) (0 - 1))

The reduced singular homology \widetilde H_{-1}(Kᶜ; R) — interpreted via natural subtraction 0 - 1 = 0 and the augmentation kernel definition — is trivial.

theorem AlexanderDuality.relativeSingularHomology_degree_zero_subsingleton_of_acyclic (R : Type) [CommRing R] {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n))) (hK : IsCompact K) : Subsingleton ↑(PoincareDuality.relativeSingularHomology R (↑∅ᶜ) (Subtype.val ⁻¹' Kᶜ) 0)

The relative singular homology H_0(ℝⁿ, ℝⁿ \ K; R) vanishes, used as a stepping stone to deduce vanishing of top-degree Čech cohomology of K.

theorem AlexanderDuality.cechCohomology_compact_euclidean_top_degree_eq_zero (R : Type) [CommRing R] {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n))) (hK : IsCompact K) : Subsingleton ↑(PoincareDuality.cechCohomology R (EuclideanSpace ℝ (Fin n)) K ∅ n)

Corollary 38.5: for a compact subset K of ℝⁿ, the Čech cohomology Ȟ^n(K; R) vanishes.

theorem AlexanderDuality.jordan_brouwer_separation_aux {n : ℕ} (hn : n ≥ 1) (K : Set (EuclideanSpace ℝ (Fin n))) (hK : IsCompact K) (hHomeo : Nonempty (↑K ≃ₜ ↑(Metric.sphere 0 1))) : Nat.card (ConnectedComponents ↑Kᶜ) = 2

Auxiliary Jordan–Brouwer separation statement: a compact subset K of ℝⁿ (n ≥ 1) homeomorphic to the unit sphere Sⁿ⁻¹-style sphere has complement with exactly two connected components.

def AlgebraicTopologyI.IsKnot (f : TopCat.sphere 1 ⟶ TopCat.sphere 3) : Prop

A knot is a topological embedding S¹ ↪ S³.

noncomputable def AlgebraicTopologyI.knotComplement (f : TopCat.sphere 1 ⟶ TopCat.sphere 3) : TopCat

The complement S³ \ f(S¹) of a knot f : S¹ ↪ S³, packaged as a topological space.

def AlgebraicTopologyI.IsHomologyCircle (X : TopCat) : Prop

A space X is a homology circle if its singular homology agrees with that of the circle S¹ in every degree and over every commutative ring R.

theorem AlgebraicTopologyI.knotComplement_isHomologyCircle (f : TopCat.sphere 1 ⟶ TopCat.sphere 3) (hf : IsKnot f) : IsHomologyCircle (knotComplement f)

Corollary 38.6: the complement of a knot in S³ is a homology circle.