Chapter 3. Cohomology
FC07 — Hatcher, Algebraic Topology.
This chapter contains 34 definitions, 19 theorems, 23 propositions, 7 lemmas, 12 corollaries, 46 examples, 16 constructions and 2 conventions.
Of the 159 statements checked against Lean, 12 are formalized somewhere and 147 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 147 | 92% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 12 | 8% | Mathlib states and proves it. |
| checked in total | 159 |
- Canonical source block: FC07 Hatcher, Chapter 3,
FC07-C03-U001–FC07-C03-U159, exactly 159 contiguous rows retrieved from FC07 — Hatcher, Algebraic Topology throughagent-memory. - Search order followed the mapping plan: project source first at
A=3b2239e161592472b34e02ad3b7da308f9ce7280, then pinned MathlibP=db584cd6d46c92f209a44c0f1c829460d327499d(Apache-2.0, Lean 4.33.0), current upstream MathlibH=633b366493a76df88a2bff099ed0cbf711a59ec9(Apache-2.0, Lean 4.34.0-rc2), current/open work and indexed searches, Reservoir/package discovery, broad GitHub/discoverable Lean, and local mirrors. Noproject-existingC03 owner was found. - Every promoted Mathlib declaration/path was compiled through the project toolchain at the exact pin
P; every cited source path was also verified withgit cat-fileat the pinned git object. C03 therefore uses onlymathlibandunmatchedroutes: 12 pinned positive rows and 147 dated unmatched rows. - The exact pinned positives are U002 (abelian dual and precomposition), U003 (dual cochain complex), U004 (projective/free-resolution lift, homotopy uniqueness, and resolution-independent dual cohomology via Ext), U025 (tensor product of abelian groups), U055 (directed systems/direct limits), U073 (right exactness of tensor product), U091 (H-spaces), U100 (Lucas congruence), U108 (SO(n) as determinant-one orthogonal matrices), U126 (inverse limits as compatible sections), U128 (p-adic integers as the inverse limit of
ZMod (p^n)via the universal property), and U133 (the two six-term Hom/Ext exact sequences). ChainComplex.linearYonedaObjis the decisive C03 cochain-level interface: overModuleCat ℤit has degree-n termHom(C_n,G)with differential induced contravariantly from the chain differential.ProjectiveResolution.lift,liftHomotopy,homotopyEquiv, andisoExtthen own all clauses of U004; generic resolution machinery is not credited for stronger UCT rows without their stated exact sequences/splittings.TensorProduct.gradedMulandtmul_of_gradedMul_of_tmulat P implement the exact Koszul multiplication(a⊗b)(c⊗d)=(-1)^(|b||c|)ac⊗bd, but U026 also asserts that the cohomology cross product is a ring homomorphism. Since no checked singular-cohomology cross product exists, strict bundle semantics leave U026 unmatched. LikewiseGradedRingsupplies degree-compatible multiplication but not Hatcher’s graded-commutativity sign clause in U020.Matrix.orthogonalGroup/mem_orthogonalGroup_iffsupply the algebraic O(n) characterization, butTopologicalSpace (Matrix.orthogonalGroup (Fin 2) ℝ)does not synthesize at P. U107 therefore remains unmatched because its subspace-topology clause is part of the row.Matrix.specialOrthogonalGroupandmem_specialOrthogonalGroup_iffdo own U108, which has no topology clause.- Current upstream
H=633b366493a76df88a2bff099ed0cbf711a59ec9was verified as the 2026-09-06 Mathlib dependency-update commit. Current Mathlib code search found nosingularCohomology, cup-product cohomology, orPoincareDualitydeclaration. The main Chapter-3 topological gap therefore persists beyond P: singular/reduced/relative/cellular cohomology, cup/cap products, compact-support cohomology, Poincaré/Alexander duality, Bockstein, covering-space transfer, and local coefficients are not bridged by checked current interfaces. - Mathlib does contain substantial algebraic group-cohomology infrastructure (including finite cyclic groups), but U139–U144 are topological cohomology-ring computations of
K(G,1)spaces and transfer examples. No checkedK(G,1)/singular-cohomology bridge and no required ring computation were found, so these remain unmatched. - Generic Čech nerves and sheaf Čech cohomology are not Hatcher’s topological Čech cohomology of open-cover nerves; generic fiber/vector-bundle pullbacks are not bundles of groups with fiberwise group-isomorphism structure; and the algebraic finite-group transfer is not the covering-space transfer. These name-adjacent APIs are not credited.
- A broad external search found no complete Lean-4 owner for the missing Chapter-3 singular-cohomology/duality/local-coefficient interfaces. A small external cohomology-ring development found in discovery is coefficient- and construction-specific and does not own the general Hatcher rows.
N=2026-09-07denotes a dated unmatched result after the prescribed search layers. Strict whole-row semantics are applied uniformly: specializations, adjacent algebra, isolated clauses/examples, and unbridged alternative representations do not count.
Definition/construction — simplicial cochains and cohomology
For a Δ-complex X and abelian group G, simplicial i-cochains are G-valued functions on oriented i-simplices, with coboundary the alternating face sum; the cohomology of this cochain complex is simplicial cohomology H^i(X;G).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a Δ-complex X and abelian group G, simplicial i-cochains are G-valued functions on oriented i-simplices, with coboundary the alternating face sum; the cohomology of this cochain complex is simplicial cohomology H^i(X;G). Pinned/current Mathlib has singular chains and simplicial-set homology, but no Hatcher Δ-complex cochain/cohomology construction. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition/construction — dual group and dual homomorphism
For an abelian group A, Hom(A,G) is its dual group (with coefficients G). A homomorphism α:A→B has dual α^:Hom(B,G)→Hom(A,G), α^(φ)=φ∘α.
Formalized. Mathlib/Algebra/Group/Hom/Defs.lean::AddMonoidHom; Mathlib/Algebra/Group/Hom/Instances.lean::AddMonoidHom.comp — For additive abelian groups, A →+ G is exactly Hom(A,G), with its pointwise abelian-group structure. AddMonoidHom.comp is precomposition, so φ ↦ φ.comp α is exactly the contravariant dual homomorphism in the source.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Construction — dual cochain complex of a chain complex
For a chain complex C, set C_n^=Hom(C_n,G) and define the coboundary δ=∂:C_{n−1}^→C_n; since ∂²=0, δ²=0 and this is the dual cochain complex.
Formalized. Mathlib/CategoryTheory/Abelian/Ext.lean::ChainComplex.linearYonedaObj — Specialized to abelian groups as ℤ-modules, ChainComplex.linearYonedaObj sends a chain complex C and coefficient object G to the cochain complex whose degree-n object is Hom(C_n,G) and whose differential is induced contravariantly by the chain differential. Thus δ is precomposition with ∂ and δ²=0.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Lemma 3.1
Let F,F′ be free resolutions of abelian groups H,H′. Every homomorphism H→H′ extends to a chain map F→F′, any two extensions are chain homotopic, and consequently the cohomology groups obtained by dualizing a free resolution are canonically independent of the chosen resolution.
Formalized. Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean::CategoryTheory.ProjectiveResolution.lift, CategoryTheory.ProjectiveResolution.liftHomotopy, CategoryTheory.ProjectiveResolution.homotopyEquiv; Mathlib/CategoryTheory/Abelian/Ext.lean::CategoryTheory.ProjectiveResolution.isoExt — Free resolutions of abelian groups are projective resolutions. lift extends a morphism to a chain map, liftHomotopy makes any two compatible extensions homotopic, and homotopyEquiv identifies any two projective resolutions. isoExt identifies the cohomology of the dualized resolution with Ext, giving the canonical resolution-independent cohomology asserted in the final clause.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Theorem 3.2
Universal coefficient theorem for cohomology: if C is a chain complex of free abelian groups, then for every n and G there is a split exact sequence 0→Ext(H_{n−1}(C),G)→H^n(C;G)→Hom(H_n(C),G)→0.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Universal coefficient theorem for cohomology: if C is a chain complex of free abelian groups, then for every n and G there is a split exact sequence 0→Ext(H_{n−1}(C),G)→H^n(C;G)→Hom(H_n(C),G)→0. Pinned Mathlib has projective resolutions, Ext, Hom complexes, and generic quasi-isomorphism/homotopy machinery, but no checked theorem packages the stated universal-coefficient or cohomology-isomorphism conclusion for free abelian chain complexes. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 3.3
If the homology groups H_{n} and H_{n - 1} of a chain complex C of free abelian groups are finitely generated, with torsion subgroups T_{n} ~ ⊂ ~ H_{n} and T_{n - 1} ⊂ H_{n - 1}, then H^{n} (C; ℤ) ≅ (H_{n} / T_{n}) ⊕ T_{n - 1}.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If the homology groups H_{n} and H_{n - 1} of a chain complex C of free abelian groups are finitely generated, with torsion subgroups T_{n} ~ ⊂ ~ H_{n} and T_{n - 1} ⊂ H_{n - 1}, then H^{n} (C; ℤ) ≅ (H_{n} / T_{n}) ⊕ T_{n - 1}. Pinned Mathlib has projective resolutions, Ext, Hom complexes, and generic quasi-isomorphism/homotopy machinery, but no checked theorem packages the stated universal-coefficient or cohomology-isomorphism conclusion for free abelian chain complexes. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 3.4
If a chain map between chain complexes of free abelian groups induces an isomorphism on homology groups, then it induces an isomorphism on cohomology groups with any coefficient group G.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If a chain map between chain complexes of free abelian groups induces an isomorphism on homology groups, then it induces an isomorphism on cohomology groups with any coefficient group G. Pinned Mathlib has projective resolutions, Ext, Hom complexes, and generic quasi-isomorphism/homotopy machinery, but no checked theorem packages the stated universal-coefficient or cohomology-isomorphism conclusion for free abelian chain complexes. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — singular cochains and cohomology
For abelian G, C^n(X;G)=Hom(C_n(X),G); the coboundary δ is dual to ∂, and H^n(X;G)=ker δ/im δ.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For abelian G, C^n(X;G)=Hom(C_n(X),G); the coboundary δ is dual to ∂, and H^n(X;G)=ker δ/im δ. Pinned/current Mathlib has singular homology but no checked singular-cohomology functor, reduced/relative singular cohomology, cup product, or cellular-cohomology bridge realizing this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — reduced cohomology
Reduced cohomology is obtained by dualizing the augmented singular chain complex; for n>0 it agrees with ordinary cohomology.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Reduced cohomology is obtained by dualizing the augmented singular chain complex; for n>0 it agrees with ordinary cohomology. Pinned/current Mathlib has singular homology but no checked singular-cohomology functor, reduced/relative singular cohomology, cup product, or cellular-cohomology bridge realizing this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — relative cohomology
C^n(X,A;G) consists of cochains on X vanishing on chains in A; the restricted coboundary defines H^n(X,A;G).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: C^n(X,A;G) consists of cochains on X vanishing on chains in A; the restricted coboundary defines H^n(X,A;G). Pinned/current Mathlib has singular homology but no checked singular-cohomology functor, reduced/relative singular cohomology, cup product, or cellular-cohomology bridge realizing this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — cellular cohomology
For a CW complex, dualizing the cellular chain complex with coefficients G gives the cellular cochain complex; its cohomology is cellular cohomology.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a CW complex, dualizing the cellular chain complex with coefficients G gives the cellular cochain complex; its cohomology is cellular cohomology. Pinned/current Mathlib has singular homology but no checked singular-cohomology functor, reduced/relative singular cohomology, cup product, or cellular-cohomology bridge realizing this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 3.5
H^{n} (X; G) ≅ ker d_{n} / im d_{n - 1}. Furthermore, the cellular cochain complex { H^{n} (X^{n}, X^{n - 1}; G), d_{n} } is isomorphic to the dual of the cellular chain complex, obtained by applying Hom (-, G).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: H^{n} (X; G) ≅ ker d_{n} / im d_{n - 1}. Furthermore, the cellular cochain complex { H^{n} (X^{n}, X^{n - 1}; G), d_{n} } is isomorphic to the dual of the cellular chain complex, obtained by applying Hom (-, G). Pinned/current Mathlib has singular homology but no checked singular-cohomology functor, reduced/relative singular cohomology, cup product, or cellular-cohomology bridge realizing this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition/construction — cup product
For cochains φ∈C^k(X;R), ψ∈C^ℓ(X;R), the cup product φ⌣ψ evaluates φ on the front k-face and ψ on the back ℓ-face of a singular (k+ℓ)-simplex; it descends to cohomology.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For cochains φ∈C^k(X;R), ψ∈C^ℓ(X;R), the cup product φ⌣ψ evaluates φ on the front k-face and ψ on the back ℓ-face of a singular (k+ℓ)-simplex; it descends to cohomology. Pinned/current Mathlib has singular homology but no checked singular-cohomology functor, reduced/relative singular cohomology, cup product, or cellular-cohomology bridge realizing this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3.7
Let M be the closed orientable surface of genus g ≥ 1 with the Δ-complex structure shown in the figure for the case g = 2. We have H^{1} (M) ≅ Hom (H_{1} (M), ℤ) by cellular cohomology or the universal coefficient theorem.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let M be the closed orientable surface of genus g ≥ 1 with the Δ-complex structure shown in the figure for the case g = 2. We have H^{1} (M) ≅ Hom (H_{1} (M), ℤ) by cellular cohomology or the universal coefficient theorem. Pinned/current Mathlib has singular homology but no checked singular-cohomology functor, reduced/relative singular cohomology, cup product, or cellular-cohomology bridge realizing this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3.8
The closed nonorientable surface N of genus g can be treated in similar fashion if we use ℤ_{2} coefficients. In particular, when g = 1 we have N = ℝP^{2}, and the cup product of a generator of H^{1} (ℝP^{2}; ℤ_{2}) with itself is a generator of H^{2} (ℝP^{2}; ℤ_{2}).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The closed nonorientable surface N of genus g can be treated in similar fashion if we use ℤ_{2} coefficients. In particular, when g = 1 we have N = ℝP^{2}, and the cup product of a generator of H^{1} (ℝP^{2}; ℤ_{2}) with itself is a generator of H^{2} (ℝP^{2}; ℤ_{2}). Pinned/current Mathlib has singular homology but no checked singular-cohomology functor, reduced/relative singular cohomology, cup product, or cellular-cohomology bridge realizing this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3.9
Let X be the 2 dimensional CW complex obtained by attaching a 2 cell to S^{1} by the degree m map S^{1} → S^{1}, z ↦ z^{m}. Using cellular cohomology, or cellular homology and the universal coefficient theorem, we see that H^{n} (X; ℤ) consists of a ℤ for n = 0 and a ℤ_{m} for n = 2, so the cup product structure with ℤ coefficients is uninteresting. However, with ℤ_{m} coefficients we have H^{i} (X; ℤ_{m}) ≅ ℤ_{m} for i = 0, 1, 2, so there is the possibility that the cup product of two 1 dimensional classes can be nontrivial.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let X be the 2 dimensional CW complex obtained by attaching a 2 cell to S^{1} by the degree m map S^{1} → S^{1}, z ↦ z^{m}. Using cellular cohomology, or cellular homology and the universal coefficient theorem, we see that H^{n} (X; ℤ) consists of a ℤ for n = 0 and a ℤ_{m} for n = 2, so the cup product structure with ℤ coefficients is uninteresting. However, with ℤ_{m} coefficients we have H^{i} (X; ℤ_{m}) ≅ ℤ_{m} for i = 0, 1, 2, so there is the possibility that the cup product of two 1 dimensional classes can be nontrivial. Pinned/current Mathlib has singular homology but no checked singular-cohomology functor, reduced/relative singular cohomology, cup product, or cellular-cohomology bridge realizing this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 3.10
For a map f: X {→ } Y, the induced maps f^{}: H^{n} (Y; R) → H^{n} (X; R) satisfy f^{} (α ∪ β) = f^{} (α) ∪ f^{} (β), and similarly in the relative case.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a map f: X {→ } Y, the induced maps f^{}: H^{n} (Y; R) → H^{n} (X; R) satisfy f^{} (α ∪ β) = f^{} (α) ∪ f^{} (β), and similarly in the relative case. Pinned/current Mathlib has singular homology but no checked singular-cohomology functor, reduced/relative singular cohomology, cup product, or cellular-cohomology bridge realizing this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 3.11
The identity α ∪ β = (- 1)^{k ℓ} β ∪ α holds for all α ∈ H^{k} (X, A; R) and β ∈ H^{ℓ} (X, A; R), when R is commutative.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The identity α ∪ β = (- 1)^{k ℓ} β ∪ α holds for all α ∈ H^{k} (X, A; R) and β ∈ H^{ℓ} (X, A; R), when R is commutative. Pinned/current Mathlib has singular homology but no checked singular-cohomology functor, reduced/relative singular cohomology, cup product, or cellular-cohomology bridge realizing this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — cohomology ring
For coefficient ring R, H^*(X;R)=⊕_{n≥0}H^n(X;R) with cup product is the cohomology ring of X.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For coefficient ring R, H^*(X;R)=⊕_{n≥0}H^n(X;R) with cup product is the cohomology ring of X. Pinned/current Mathlib has singular homology but no checked singular-cohomology functor, reduced/relative singular cohomology, cup product, or cellular-cohomology bridge realizing this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — graded and graded-commutative ring
A graded ring A=⊕{k≥0}A_k satisfies A_kA_ℓ⊂A{k+ℓ}; in this context “commutative” means ab=(−1)^{|a||b|}ba.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A graded ring A=⊕{k≥0}A_k satisfies A_kA_ℓ⊂A{k+ℓ}; in this context “commutative” means ab=(−1)^{}ba. Mathlib/RingTheory/GradedAlgebra/Basic.lean::GradedRing records degree-compatible multiplication, but no checked graded-commutativity structure/sign law supplies the second half of the bundled definition. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3.12
Polynomial Rings. Among the simplest graded rings are polynomial rings R [ α ] and their truncated versions R [ α ] / (α^{n}), consisting of polynomials of degree less than n. We will also show that H^{} (ℂP^{n}; ℤ) ≅ ℤ [ α ] / (α^{n + 1}) and H^{} (ℂP^{∞}; ℤ) ≅ ℤ [ α ] with | α | = 2.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Polynomial Rings. Among the simplest graded rings are polynomial rings R [ α ] and their truncated versions R [ α ] / (α^{n}), consisting of polynomials of degree less than n. We will also show that H^{} (ℂP^{n}; ℤ) ≅ ℤ [ α ] / (α^{n + 1}) and H^{} (ℂP^{∞}; ℤ) ≅ ℤ [ α ] with α = 2. Polynomial/exterior/tensor algebra interfaces exist algebraically, but no checked singular-cohomology ring or cohomology cross-product declaration connects them to the topological statement. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3.13
Exterior Algebras. Another nice example of a commutative graded ring is the exterior algebra Λ_{R} [ α_{1}, …, α_{n} ] over a commutative ring R with identity. The exterior algebra becomes a commutative graded ring by specifying odd dimensions for the generators α_{i}.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Exterior Algebras. Another nice example of a commutative graded ring is the exterior algebra Λ_{R} [ α_{1}, …, α_{n} ] over a commutative ring R with identity. The exterior algebra becomes a commutative graded ring by specifying odd dimensions for the generators α_{i}. Polynomial/exterior/tensor algebra interfaces exist algebraically, but no checked singular-cohomology ring or cohomology cross-product declaration connects them to the topological statement. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3.14
Cohomology converts disjoint unions into products of graded rings: H^*(⊔_α X_α;R)≅∏_α H^*(X_α;R). Under the stated good-basepoint hypotheses, reduced cohomology of a wedge has the analogous product-ring description.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Cohomology converts disjoint unions into products of graded rings: H^*(⊔_α X_α;R)≅∏_α H^*(X_α;R). Under the stated good-basepoint hypotheses, reduced cohomology of a wedge has the analogous product-ring description. Polynomial/exterior/tensor algebra interfaces exist algebraically, but no checked singular-cohomology ring or cohomology cross-product declaration connects them to the topological statement. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — cross product in cohomology
The external product a×b∈H^{i+j}(X×Y) is p_1^a⌣p_2^b.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The external product a×b∈H^{i+j}(X×Y) is p_1^a⌣p_2^b. Polynomial/exterior/tensor algebra interfaces exist algebraically, but no checked singular-cohomology ring or cohomology cross-product declaration connects them to the topological statement. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — tensor product of abelian groups
For abelian groups A and B, A⊗B is generated by symbols a⊗b subject to additivity in each variable.
Formalized. Mathlib/LinearAlgebra/TensorProduct/Defs.lean::TensorProduct, TensorProduct.tmul — For abelian groups viewed as ℤ-modules, TensorProduct ℤ A B is the universal additive-bilinear tensor product generated by pure tensors a ⊗ₜ b; its quotient relations give additivity in each variable. This is the standard tensor product of abelian groups in the source.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Convention — multiplication in a tensor product of graded rings
For graded rings, the tensor-product multiplication is (a⊗b)(c⊗d)=(-1)^{|b||c|}ac⊗bd; with this Koszul sign the cohomology cross product is a ring homomorphism.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For graded rings, the tensor-product multiplication is (a⊗b)(c⊗d)=(-1)^{|b||c|}ac⊗bd; with this Koszul sign the cohomology cross product is a ring homomorphism. TensorProduct.gradedMul and tmul_of_gradedMul_of_tmul implement the exact Koszul multiplication formula, but no checked cohomology cross product exists to prove the bundled ring-homomorphism clause. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 3.15
The cross product H^{*} (X; R) ⊗_{R} H^{} (Y; R) {→ } H^{} (X × Y; R) is an isomorphism of rings if X and Y are CW complexes and H^{k} (Y; R) is a finitely generated free R module for all k.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The cross product H^{*} (X; R) ⊗_{R} H^{} (Y; R) {→ } H^{} (X × Y; R) is an isomorphism of rings if X and Y are CW complexes and H^{k} (Y; R) is a finitely generated free R module for all k. Pinned/current Mathlib has generic tensor and graded-algebra infrastructure, but no checked cohomological Künneth theorem or the stated cohomology-ring computation. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3.16
The exterior algebra Λ_{R} [ α_{1}, …, α_{n} ] is the graded tensor product over R of the one-variable exterior algebras Λ_{R} [ α_{i} ] where the α_{i} ’s have odd dimension. The Künneth formula then gives an isomorphism H^{*} (S ^ { k_{1} } × … × S ^ { k_{n} }; ℤ) ≅ Λ_{ℤ} [ α_{1}, …, α_{n} ] if the dimensions k_{i} are all odd.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The exterior algebra Λ_{R} [ α_{1}, …, α_{n} ] is the graded tensor product over R of the one-variable exterior algebras Λ_{R} [ α_{i} ] where the α_{i} ’s have odd dimension. The Künneth formula then gives an isomorphism H^{*} (S ^ { k_{1} } × … × S ^ { k_{n} }; ℤ) ≅ Λ_{ℤ} [ α_{1}, …, α_{n} ] if the dimensions k_{i} are all odd. Pinned/current Mathlib has generic tensor and graded-algebra infrastructure, but no checked cohomological Künneth theorem or the stated cohomology-ring computation. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 3.17
If a natural transformation between unreduced cohomology theories on the category of CW pairs is an isomorphism when the CW pair is (point, ∅), then it is an isomorphism for all CW pairs.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If a natural transformation between unreduced cohomology theories on the category of CW pairs is an isomorphism when the CW pair is (point, ∅), then it is an isomorphism for all CW pairs. Pinned/current Mathlib has generic tensor and graded-algebra infrastructure, but no checked cohomological Künneth theorem or the stated cohomology-ring computation. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 3.18
For CW pairs (X, A) and (Y, B) the cross product homomorphism H^{*} (X, A; R) ⊗_{R} H^{} (Y, B; R) → H^{} (X × Y, A × Y ∪ X × B; R) is an isomorphism of rings i f H^{k} (Y, B; R) is a finitely generated free R module for each k.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For CW pairs (X, A) and (Y, B) the cross product homomorphism H^{*} (X, A; R) ⊗_{R} H^{} (Y, B; R) → H^{} (X × Y, A × Y ∪ X × B; R) is an isomorphism of rings i f H^{k} (Y, B; R) is a finitely generated free R module for each k. Pinned/current Mathlib has generic tensor and graded-algebra infrastructure, but no checked cohomological Künneth theorem or the stated cohomology-ring computation. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 3.19
H^{} (ℝP^{n}; ℤ_{2}) ≅ ℤ_{2} [ α ] / (α^{n + 1}) and H^{} (ℝP^{∞}; ℤ_{2}) ≅ ℤ_{2} [ α ], where | α | = 1. In the complex case, H^{} (ℂP^{n}; ℤ) ≅ ℤ [ α ] / (α^{n + 1}) and H^{} (ℂP^{∞}; ℤ) ≅ ℤ [ α ] where | α | = 2.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: H^{} (ℝP^{n}; ℤ_{2}) ≅ ℤ_{2} [ α ] / (α^{n + 1}) and H^{} (ℝP^{∞}; ℤ_{2}) ≅ ℤ_{2} [ α ], where α = 1. In the complex case, H^{} (ℂP^{n}; ℤ) ≅ ℤ [ α ] / (α^{n + 1}) and H^{} (ℂP^{∞}; ℤ) ≅ ℤ [ α ] where α = 2. Pinned/current Mathlib has generic tensor and graded-algebra infrastructure, but no checked cohomological Künneth theorem or the stated cohomology-ring computation. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3.20
Combining the calculation H^{} (ℝP^{∞}; ℤ_{2}) ≅ ℤ_{2} [ α ] with the Künneth formula, we see that H^{} (ℝP^{∞} × ℝP^{∞}; ℤ_{2}) is isomorphic to ℤ_{2} [ α_{1} ] ⊗ ℤ_{2} [ α_{2} ], which is just the polynomial ring ℤ_{2} [ α_{1}, α_{2} ]. More generally it follows by induction that for a product of n copies of ℝP^{∞}, the ℤ_{2} cohomology is a polynomial ring in n variables. Similar remarks apply to ℂP^{∞} and { {H } } {P }^{∞} with coefficients in ℤ or any commutative ring.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Combining the calculation H^{} (ℝP^{∞}; ℤ_{2}) ≅ ℤ_{2} [ α ] with the Künneth formula, we see that H^{} (ℝP^{∞} × ℝP^{∞}; ℤ_{2}) is isomorphic to ℤ_{2} [ α_{1} ] ⊗ ℤ_{2} [ α_{2} ], which is just the polynomial ring ℤ_{2} [ α_{1}, α_{2} ]. More generally it follows by induction that for a product of n copies of ℝP^{∞}, the ℤ_{2} cohomology is a polynomial ring in n variables. Similar remarks apply to ℂP^{∞} and { {H } } {P }^{∞} with coefficients in ℤ or any commutative ring. Pinned/current Mathlib has generic tensor and graded-algebra infrastructure, but no checked cohomological Künneth theorem or the stated cohomology-ring computation. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 3.21
If ℝ^{n} has the structure of a division algebra over the scalar field ℝ, then n must be a power of 2.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If ℝ^{n} has the structure of a division algebra over the scalar field ℝ, then n must be a power of 2. Pinned/current Mathlib has generic tensor and graded-algebra infrastructure, but no checked cohomological Künneth theorem or the stated cohomology-ring computation. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 3.22
For n > 0, H^{} (J (S^{n}); ℤ) consists of a ℤ in each dimension a multiple of n. If n is even, the i^{t h} power of a generator of H^{n} (J (S^{n}); ℤ) is i! times a generator of H^{i n} (J (S^{n}); ℤ), for each i ~ ≥ ~ 1. When n is odd, H^{} (J (S^{n}); ℤ) is isomorphic as a graded ring to H^{} (S^{n}; ℤ) ⊗ H^{} (J (S^{2 n}); ℤ).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For n > 0, H^{} (J (S^{n}); ℤ) consists of a ℤ in each dimension a multiple of n. If n is even, the i^{t h} power of a generator of H^{n} (J (S^{n}); ℤ) is i! times a generator of H^{i n} (J (S^{n}); ℤ), for each i ~ ≥ ~ 1. When n is odd, H^{} (J (S^{n}); ℤ) is isomorphic as a graded ring to H^{} (S^{n}; ℤ) ⊗ H^{} (J (S^{2 n}); ℤ). Pinned/current Mathlib has generic tensor and graded-algebra infrastructure, but no checked cohomological Künneth theorem or the stated cohomology-ring computation. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3.23
Subcomplexes of the ±b {n } Torus. To give just a small hint of the endless variety of nonfree cup product algebras that can be realized, consider subcomplexes of the n torus T^{n}, the product of n copies of S^{1}. We know that H^{*} (T^{n}; ℤ) is the exterior algebra Λ_{ℤ} [ α_{1}, …, α_{n} ], with the monomial α _ { i_{1} } … α _ { i_{k} } corresponding via cellular cohomology to the k cell e _ { i_{1} }^{1} × … × e _ { i_{k} }^{1}.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Subcomplexes of the ±b {n } Torus. To give just a small hint of the endless variety of nonfree cup product algebras that can be realized, consider subcomplexes of the n torus T^{n}, the product of n copies of S^{1}. We know that H^{*} (T^{n}; ℤ) is the exterior algebra Λ_{ℤ} [ α_{1}, …, α_{n} ], with the monomial α _ { i_{1} } … α _ { i_{k} } corresponding via cellular cohomology to the k cell e _ { i_{1} }^{1} × … × e _ { i_{k} }^{1}. Pinned/current Mathlib has generic tensor and graded-algebra infrastructure, but no checked cohomological Künneth theorem or the stated cohomology-ring computation. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3.24
Cohen–Macaulay Rings. Let X be the quotient space ℂP^{∞} / ℂP^{n - 1}. Thus H^{*} (X; ℤ) is an example of a Cohen–Macaulay ring: a ring containing a polynomial subring over which it is a finitely generated free module.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Cohen–Macaulay Rings. Let X be the quotient space ℂP^{∞} / ℂP^{n - 1}. Thus H^{*} (X; ℤ) is an example of a Cohen–Macaulay ring: a ring containing a polynomial subring over which it is a finitely generated free module. Pinned/current Mathlib has generic tensor and graded-algebra infrastructure, but no checked cohomological Künneth theorem or the stated cohomology-ring computation. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — n-manifold
An n-manifold is a Hausdorff space in which every point has an open neighborhood homeomorphic to ℝ^n.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: An n-manifold is a Hausdorff space in which every point has an open neighborhood homeomorphic to ℝ^n. Smooth/manifold and homological-algebra APIs exist, but no checked local singular-homology orientation theory for topological manifolds realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — closed manifold
A compact manifold without boundary is called closed.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A compact manifold without boundary is called closed. Smooth/manifold and homological-algebra APIs exist, but no checked local singular-homology orientation theory for topological manifolds realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — local orientation of a manifold
A local orientation of an n-manifold M at x is a choice of generator μ_x of H_n(M,M−{x};ℤ).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A local orientation of an n-manifold M at x is a choice of generator μ_x of H_n(M,M−{x};ℤ). Smooth/manifold and homological-algebra APIs exist, but no checked local singular-homology orientation theory for topological manifolds realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Convention — local homology notation
Write H_n(X∣A)=H_n(X,X−A), and more generally H_n(X|A;G)=H_n(X,X−A;G); by excision this depends only on a neighborhood of the closure of A.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Write H_n(X∣A)=H_n(X,X−A), and more generally H_n(X;G)=H_n(X,X−A;G); by excision this depends only on a neighborhood of the closure of A. Smooth/manifold and homological-algebra APIs exist, but no checked local singular-homology orientation theory for topological manifolds realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — orientation and orientable manifold
An orientation of an n-manifold M is a locally consistent choice x↦μ_x of generators μ_x∈H_n(M,M−{x};ℤ); M is orientable if such a choice exists.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: An orientation of an n-manifold M is a locally consistent choice x↦μ_x of generators μ_x∈H_n(M,M−{x};ℤ); M is orientable if such a choice exists. Smooth/manifold and homological-algebra APIs exist, but no checked local singular-homology orientation theory for topological manifolds realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 3.25
If M is connected, then M is orientable iff tilde(M) has two components. In particular, M is orientable if it is simply-connected, or more generally if π_{1} (M) has no subgroup of index two.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If M is connected, then M is orientable iff tilde(M) has two components. In particular, M is orientable if it is simply-connected, or more generally if π_{1} (M) has no subgroup of index two. Smooth/manifold and homological-algebra APIs exist, but no checked local singular-homology orientation theory for topological manifolds realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — section of the orientation covering
A continuous map M→M_ℤ of the form x↦α_x∈H_n(M|x) is a section of the covering M_ℤ→M.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A continuous map M→M_ℤ of the form x↦α_x∈H_n(M) is a section of the covering M_ℤ→M. Smooth/manifold and homological-algebra APIs exist, but no checked local singular-homology orientation theory for topological manifolds realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — R-orientation
For a commutative ring R with identity, an R-orientation of an n-manifold M is a locally consistent choice of a generator of H_n(M|x;R)≅R at every x; equivalently it is a section of M_R→M whose values are generators.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a commutative ring R with identity, an R-orientation of an n-manifold M is a locally consistent choice of a generator of H_n(M;R)≅R at every x; equivalently it is a section of M_R→M whose values are generators. Smooth/manifold and homological-algebra APIs exist, but no checked local singular-homology orientation theory for topological manifolds realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 3.26
Let M be a closed connected n-manifold. If M is R-orientable, H_n(M;R)→H_n(M,M−{x};R)≅R is an isomorphism for every x. If not R-orientable, it is injective with image {r∈R:2r=0}. Also H_i(M;R)=0 for i>n. In particular H_n(M;ℤ) is ℤ or 0 according to orientability, while H_n(M;ℤ_2)=ℤ_2.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let M be a closed connected n-manifold. If M is R-orientable, H_n(M;R)→H_n(M,M−{x};R)≅R is an isomorphism for every x. If not R-orientable, it is injective with image {r∈R:2r=0}. Also H_i(M;R)=0 for i>n. In particular H_n(M;ℤ) is ℤ or 0 according to orientability, while H_n(M;ℤ_2)=ℤ_2. Smooth/manifold and homological-algebra APIs exist, but no checked local singular-homology orientation theory for topological manifolds realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — fundamental class
A class [M]∈H_n(M;R) is fundamental when its image generates H_n(M,M−{x};R) for every x∈M.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A class [M]∈H_n(M;R) is fundamental when its image generates H_n(M,M−{x};R) for every x∈M. Smooth/manifold and homological-algebra APIs exist, but no checked local singular-homology orientation theory for topological manifolds realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 3.27
Let M be an n-manifold and A⊂M compact. A section x↦α_x of the R-orientation covering determines a unique class α_A∈H_n(M,M−A;R) mapping to α_x in H_n(M,M−{x};R) for every x∈A, and H_i(M,M−A;R)=0 for i>n.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let M be an n-manifold and A⊂M compact. A section x↦α_x of the R-orientation covering determines a unique class α_A∈H_n(M,M−A;R) mapping to α_x in H_n(M,M−{x};R) for every x∈A, and H_i(M,M−A;R)=0 for i>n. Smooth/manifold and homological-algebra APIs exist, but no checked local singular-homology orientation theory for topological manifolds realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 3.28
If M is a closed connected n manifold, the torsion subgroup of H_{n - 1} (M; ℤ) is trivial if M is orientable and ℤ_{2} if M is nonorientable.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If M is a closed connected n manifold, the torsion subgroup of H_{n - 1} (M; ℤ) is trivial if M is orientable and ℤ_{2} if M is nonorientable. Smooth/manifold and homological-algebra APIs exist, but no checked local singular-homology orientation theory for topological manifolds realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 3.29
If M is a connected noncompact n manifold, then H_{i} (M; R) = 0 for i ≥ n.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If M is a connected noncompact n manifold, then H_{i} (M; R) = 0 for i ≥ n. Smooth/manifold and homological-algebra APIs exist, but no checked local singular-homology orientation theory for topological manifolds realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — cap product
For k≥ℓ, the cap product C_k(X;R)×C^ℓ(X;R)→C_{k−ℓ}(X;R) evaluates the cochain on the back ℓ-face and retains the front (k−ℓ)-face; it induces the homology/cohomology cap product.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For k≥ℓ, the cap product C_k(X;R)×C^ℓ(X;R)→C_{k−ℓ}(X;R) evaluates the cochain on the back ℓ-face and retains the front (k−ℓ)-face; it induces the homology/cohomology cap product. No checked cap-product or singular-cohomology Poincaré-duality interface was found; generic tensor/Hom infrastructure is insufficient without the topological bridge. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 3
30 (Poincar´e Duality). If M is a closed R orientable n manifold with fundamental class [ M ] ∈ H_{n} (M; R), then the map D {: } H^{k} (M; R) → H_{n - k} (M; R) defined by D (α) = [ M ] frown α is an isomorphism for all k.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: 30 (Poincar´e Duality). If M is a closed R orientable n manifold with fundamental class [ M ] ∈ H_{n} (M; R), then the map D {: } H^{k} (M; R) → H_{n - k} (M; R) defined by D (α) = [ M ] frown α is an isomorphism for all k. No checked cap-product or singular-cohomology Poincaré-duality interface was found; generic tensor/Hom infrastructure is insufficient without the topological bridge. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3.31
Surfaces. Let M be the closed orientable surface of genus g, obtained as usual from a_{4 g} gon by identifying pairs of edges according to the word a_{1} b_{1} a_{1}^{- 1} b_{1}^{- 1} … a_{g} b_{g} a_{g}^{- 1} b_{g}^{- 1}. Under the isomorphism H^{1} (M) ≅ Hom (H_{1} (M), ℤ), the cohomology class α_{i} corresponding to a_{i} assigns the value 1 to α_{i} and 0 to the other basis elements.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Surfaces. Let M be the closed orientable surface of genus g, obtained as usual from a_{4 g} gon by identifying pairs of edges according to the word a_{1} b_{1} a_{1}^{- 1} b_{1}^{- 1} … a_{g} b_{g} a_{g}^{- 1} b_{g}^{- 1}. Under the isomorphism H^{1} (M) ≅ Hom (H_{1} (M), ℤ), the cohomology class α_{i} corresponding to a_{i} assigns the value 1 to α_{i} and 0 to the other basis elements. No checked cap-product or singular-cohomology Poincaré-duality interface was found; generic tensor/Hom infrastructure is insufficient without the topological bridge. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3.32
For ℝ with vertices at the integers, compactly supported simplicial cohomology satisfies H_c^0(ℝ;G)=0 and H_c^1(ℝ;G)≅G; the latter isomorphism sends a compactly supported 1-cochain to the sum of its values on all 1-simplices.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For ℝ with vertices at the integers, compactly supported simplicial cohomology satisfies H_c^0(ℝ;G)=0 and H_c^1(ℝ;G)≅G; the latter isomorphism sends a compactly supported 1-cochain to the sum of its values on all 1-simplices. No checked cap-product or singular-cohomology Poincaré-duality interface was found; generic tensor/Hom infrastructure is insufficient without the topological bridge. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — cohomology with compact supports
For locally compact X, compactly supported cochains are those supported on a compact set in the indicated simplicial/singular sense; their cohomology is H_c^*(X;G).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For locally compact X, compactly supported cochains are those supported on a compact set in the indicated simplicial/singular sense; their cohomology is H_c^*(X;G). No checked cap-product or singular-cohomology Poincaré-duality interface was found; generic tensor/Hom infrastructure is insufficient without the topological bridge. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition/construction — directed set, direct system, direct limit
A directed set admits a common upper bound for every pair. A directed system G_α has compatible maps G_α→G_β for α≤β; its direct limit is the disjoint union modulo eventual equality.
Formalized. Mathlib/Order/Directed.lean::IsDirectedOrder; Mathlib/Order/DirectedInverseSystem.lean::DirectedSystem; Mathlib/Algebra/Colimit/Module.lean::AddCommGroup.DirectLimit, AddCommGroup.DirectLimit.of, AddCommGroup.DirectLimit.of_f, AddCommGroup.DirectLimit.induction_on, AddCommGroup.DirectLimit.of.zero_exact, AddCommGroup.DirectLimit.lift — IsDirectedOrder is the common-upper-bound condition, and DirectedSystem is the compatibility law for transition maps. AddCommGroup.DirectLimit is an equivalent quotient presentation of the direct limit: every element is represented by a stage (induction_on), transition images are identified (of_f), equality is detected after passing far enough (of.zero_exact), and lift gives the universal property.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 3.33
If a space X is the union of a directed set of subspaces X_{α} with the property that each compact set in X is contained in some X_{α}, then the natural map lim–→ H_{i} (X_{α}; G) {→ } H_{i} (X; G) is an isomorphism for all i and G.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If a space X is the union of a directed set of subspaces X_{α} with the property that each compact set in X is contained in some X_{α}, then the natural map lim–→ H_{i} (X_{α}; G) {→ } H_{i} (X; G) is an isomorphism for all i and G. No checked compact-support singular-cohomology, fundamental-class, cap-product, or Poincaré–Lefschetz interface was found; generic manifold/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3.34
H_{c}^{*} (ℝ^{n}; G). To compute lim→{→} H^{i} (ℝ^{n}, ℝ^{n} - K; G) it suffices to let K range over balls B{k} of integer radius k centered at the origin since every compact set is contained in such a ball. Since H^{i} (ℝ^{n}, ℝ^{n} - B_{k}; G) is nonzero only for i = n, when it is G, and the maps H^{n} (ℝ^{n}, ℝ^{n} - B_{k}; G) {→ } H^{n} (ℝ^{n}, ℝ^{n} - B_{k + 1}; G) | are isomorphisms, we deduce that H_{c}^{i} (ℝ^{n}; G) = 0 for i ≠ n and H_{c}^{n} (ℝ^{n}; G) ≅ G.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: H_{c}^{} (ℝ^{n}; G). To compute lim→{→} H^{i} (ℝ^{n}, ℝ^{n} - K; G) it suffices to let K range over balls B*{k} of integer radius k centered at the origin since every compact set is contained in such a ball. Since H^{i} (ℝ^{n}, ℝ^{n} - B_{k}; G) is nonzero only for i = n, when it is G, and the maps H^{n} (ℝ^{n}, ℝ^{n} - B_{k}; G) {→ } H^{n} (ℝ^{n}, ℝ^{n} - B_{k + 1}; G) are isomorphisms, we deduce that H_{c}^{i} (ℝ^{n}; G) = 0 for i ≠ n and H_{c}^{n} (ℝ^{n}; G) ≅ G. No checked compact-support singular-cohomology, fundamental-class, cap-product, or Poincaré–Lefschetz interface was found; generic manifold/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 3.35
The duality map D_{M}: H_{c}^{k} (M; R) {→ } H_{n - k} (M; R) is an isomorphism for all k whenever M is an R oriented n manifold.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The duality map D_{M}: H_{c}^{k} (M; R) {→ } H_{n - k} (M; R) is an isomorphism for all k whenever M is an R oriented n manifold. No checked compact-support singular-cohomology, fundamental-class, cap-product, or Poincaré–Lefschetz interface was found; generic manifold/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 3.36
If M=U∪V with U,V open, the Mayer–Vietoris sequence for compactly supported cohomology maps, via the duality maps D, to the Mayer–Vietoris sequence in homology, with the resulting diagram commuting up to the indicated sign (D_U⊕−D_V in the middle term).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If M=U∪V with U,V open, the Mayer–Vietoris sequence for compactly supported cohomology maps, via the duality maps D, to the Mayer–Vietoris sequence in homology, with the resulting diagram commuting up to the indicated sign (D_U⊕−D_V in the middle term). No checked compact-support singular-cohomology, fundamental-class, cap-product, or Poincaré–Lefschetz interface was found; generic manifold/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 3.37
A closed manifold of odd dimension has Euler characteristic zero.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A closed manifold of odd dimension has Euler characteristic zero. No checked compact-support singular-cohomology, fundamental-class, cap-product, or Poincaré–Lefschetz interface was found; generic manifold/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 3.38
The cup product pairing is nonsingular for closed R orientable manifolds when R is a field, or when R = ℤ and torsion in H^{*} (M; ℤ) is factored out.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The cup product pairing is nonsingular for closed R orientable manifolds when R is a field, or when R = ℤ and torsion in H^{*} (M; ℤ) is factored out. No checked compact-support singular-cohomology, fundamental-class, cap-product, or Poincaré–Lefschetz interface was found; generic manifold/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 3.39
If M is a closed connected orientable n-manifold, then α∈H^k(M;ℤ) generates an infinite cyclic summand iff there is β∈H^{n−k}(M;ℤ) such that α∪β generates H^n(M;ℤ)≅ℤ. Over a field, every nonzero α has such a β.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If M is a closed connected orientable n-manifold, then α∈H^k(M;ℤ) generates an infinite cyclic summand iff there is β∈H^{n−k}(M;ℤ) such that α∪β generates H^n(M;ℤ)≅ℤ. Over a field, every nonzero α has such a β. No checked compact-support singular-cohomology, fundamental-class, cap-product, or Poincaré–Lefschetz interface was found; generic manifold/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3.40
Projective Spaces. The cup product structure of H^{} (ℂP^{n}; ℤ) as a truncated polynomial ring ℤ [ α ] / (α^{n + 1}) with | α | = 2 can easily be deduced from this as follows. For ℝP^{n} one can use the same argument with ℤ_{2} coefficients to deduce that H^{} (ℝP^{n}; ℤ_{2}) ≅ ℤ_{2} [ α ] / (α^{n + 1}) with | α | = 1.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Projective Spaces. The cup product structure of H^{} (ℂP^{n}; ℤ) as a truncated polynomial ring ℤ [ α ] / (α^{n + 1}) with α = 2 can easily be deduced from this as follows. For ℝP^{n} one can use the same argument with ℤ_{2} coefficients to deduce that H^{} (ℝP^{n}; ℤ_{2}) ≅ ℤ_{2} [ α ] / (α^{n + 1}) with α = 1. No checked compact-support singular-cohomology, fundamental-class, cap-product, or Poincaré–Lefschetz interface was found; generic manifold/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3.41
For a lens space L^{2n+1} with π1≅ℤ_m and generators α∈H^1(L;ℤ_m), β∈H^2(L;ℤ_m), H^j is generated by β^i in degree 2i and αβ^i in degree 2i+1. If m is odd then α²=0; if m is even, α² is the unique element of order two in H^2. For L^∞, H^*(L^∞;ℤ)≅ℤ[β]/(mβ), |β|=2.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a lens space L^{2n+1} with π1≅ℤ_m and generators α∈H^1(L;ℤ_m), β∈H^2(L;ℤ_m), H^j is generated by β^i in degree 2i and αβ^i in degree 2i+1. If m is odd then α²=0; if m is even, α² is the unique element of order two in H^2. For L^∞, H^*(L^∞;ℤ)≅ℤ[β]/(mβ), . No checked compact-support singular-cohomology, fundamental-class, cap-product, or Poincaré–Lefschetz interface was found; generic manifold/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — manifold with boundary and its boundary
An n-manifold with boundary is a Hausdorff space locally homeomorphic to ℝ^n or the half-space ℝ_+^n. The points corresponding to the boundary hyperplane are intrinsically the points x with H_n(M,M−{x};ℤ)=0; they form the boundary ∂M.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: An n-manifold with boundary is a Hausdorff space locally homeomorphic to ℝ^n or the half-space ℝ_+^n. The points corresponding to the boundary hyperplane are intrinsically the points x with H_n(M,M−{x};ℤ)=0; they form the boundary ∂M. No checked compact-support singular-cohomology, fundamental-class, cap-product, or Poincaré–Lefschetz interface was found; generic manifold/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 3.42
If M is a compact manifold with boundary, then ∂M has a collar neighborhood.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If M is a compact manifold with boundary, then ∂M has a collar neighborhood. No checked compact-support singular-cohomology, fundamental-class, cap-product, or Poincaré–Lefschetz interface was found; generic manifold/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — R-orientability for a compact manifold with boundary
A compact manifold M with boundary is R-orientable when M−∂M is R-orientable; an R-orientation yields a relative fundamental class [M]∈H_n(M,∂M;R).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A compact manifold M with boundary is R-orientable when M−∂M is R-orientable; an R-orientation yields a relative fundamental class [M]∈H_n(M,∂M;R). No checked compact-support singular-cohomology, fundamental-class, cap-product, or Poincaré–Lefschetz interface was found; generic manifold/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 3.43
Suppose M is a compact R orientable n manifold whose boundary ∂ M is decomposed as the union of two compact (n - 1) dimensional manifolds A and B with a common boundary ∂ A = ∂ B = A ∩ B. Then cap product with a fundamental class [ M ] ∈ H_{n} (M, ∂ M; R) gives isomorphisms D_{M}: H^{k} (M, A; R) {→ } H_{n - k} (M, B; R) for all k.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Suppose M is a compact R orientable n manifold whose boundary ∂ M is decomposed as the union of two compact (n - 1) dimensional manifolds A and B with a common boundary ∂ A = ∂ B = A ∩ B. Then cap product with a fundamental class [ M ] ∈ H_{n} (M, ∂ M; R) gives isomorphisms D_{M}: H^{k} (M, A; R) {→ } H_{n - k} (M, B; R) for all k. No checked compact-support singular-cohomology, fundamental-class, cap-product, or Poincaré–Lefschetz interface was found; generic manifold/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 3.44
If K is a compact, locally contractible subspace of a closed orientable n manifold M, then H_{i} (M, M - K; ℤ) ≅ H^{n - i} (K; ℤ) for all i.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If K is a compact, locally contractible subspace of a closed orientable n manifold M, then H_{i} (M, M - K; ℤ) ≅ H^{n - i} (K; ℤ) for all i. Mathlib has abstract Čech nerves and sheaf Čech cohomology, but no checked topological Čech-cohomology/Alexander-duality construction matching Hatcher’s nerve-refinement and singular-cohomology context. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 3.45
If K is a compact, locally contractible, nonempty, proper subspace of S^{n}, then H̃_{i} (S^{n} - K; ℤ) ≅ H̃^{n - i - 1} (K; ℤ) for all i.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If K is a compact, locally contractible, nonempty, proper subspace of S^{n}, then H̃_{i} (S^{n} - K; ℤ) ≅ H̃^{n - i - 1} (K; ℤ) for all i. Mathlib has abstract Čech nerves and sheaf Čech cohomology, but no checked topological Čech-cohomology/Alexander-duality construction matching Hatcher’s nerve-refinement and singular-cohomology context. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 3.46
If X ⊂ ℝ^{n} is compact and locally contractible then H_{i} (X; ℤ) is 0 for i ≥ n and torsionfree for i = n - 1 and n - 2.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If X ⊂ ℝ^{n} is compact and locally contractible then H_{i} (X; ℤ) is 0 for i ≥ n and torsionfree for i = n - 1 and n - 2. Mathlib has abstract Čech nerves and sheaf Čech cohomology, but no checked topological Čech-cohomology/Alexander-duality construction matching Hatcher’s nerve-refinement and singular-cohomology context. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition/construction — Čech cohomology
For an open cover U, form its nerve N(U); refinement maps induce maps in cohomology, and Čech cohomology is the direct limit lim→ H^i(N(U);G) over refinements.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For an open cover U, form its nerve N(U); refinement maps induce maps in cohomology, and Čech cohomology is the direct limit lim→ H^i(N(U);G) over refinements. Mathlib has abstract Čech nerves and sheaf Čech cohomology, but no checked topological Čech-cohomology/Alexander-duality construction matching Hatcher’s nerve-refinement and singular-cohomology context. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 3A.1
If the sequence of abelian groups A {→ } B {→ } C {→ } 0 is exact, then so is A ⊗ G {→ } B ⊗ G {→ } C ⊗ G {→ } 0.
Formalized. Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean::rTensor_exact, LinearMap.rTensor_surjective — Specializing the scalar ring to ℤ, rTensor_exact sends an exact pair A→B→C with B→C surjective to an exact pair after tensoring with G, while LinearMap.rTensor_surjective preserves the final surjection. Together these give exactly A⊗G→B⊗G→C⊗G→0 exact.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Lemma 3A.2
For any two free resolutions F and F^{′} of H there are canonical isomorphisms H_{n} (F ⊗ G) ≅ H_{n} (F^{’} ⊗ G) for all n.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For any two free resolutions F and F^{′} of H there are canonical isomorphisms H_{n} (F ⊗ G) ≅ H_{n} (F^{’} ⊗ G) for all n. Pinned Mathlib has tensor right-exactness, projective resolutions, Ext/Tor objects, and derived-functor infrastructure, but no checked declaration realizes the complete stated UCT/Tor bundle (including all identifications, splittings, exact sequences, or higher-Tor nonvanishing as applicable). Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 3A.3
Universal coefficient theorem for homology: if C is a chain complex of free abelian groups, then for every n and abelian group G there is a natural short exact sequence 0→H_n(C)⊗G→H_n(C;G)→Tor(H_{n−1}(C),G)→0; it splits, but not naturally.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Universal coefficient theorem for homology: if C is a chain complex of free abelian groups, then for every n and abelian group G there is a natural short exact sequence 0→H_n(C)⊗G→H_n(C;G)→Tor(H_{n−1}(C),G)→0; it splits, but not naturally. Pinned Mathlib has tensor right-exactness, projective resolutions, Ext/Tor objects, and derived-functor infrastructure, but no checked declaration realizes the complete stated UCT/Tor bundle (including all identifications, splittings, exact sequences, or higher-Tor nonvanishing as applicable). Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 3A.4
For every pair (X,A), every n, and every abelian group G there is a split short exact sequence 0→H_n(X,A)⊗G→H_n(X,A;G)→Tor(H_{n−1}(X,A),G)→0, natural with respect to maps of pairs; the splitting is not natural.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For every pair (X,A), every n, and every abelian group G there is a split short exact sequence 0→H_n(X,A)⊗G→H_n(X,A;G)→Tor(H_{n−1}(X,A),G)→0, natural with respect to maps of pairs; the splitting is not natural. Pinned Mathlib has tensor right-exactness, projective resolutions, Ext/Tor objects, and derived-functor infrastructure, but no checked declaration realizes the complete stated UCT/Tor bundle (including all identifications, splittings, exact sequences, or higher-Tor nonvanishing as applicable). Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 3A.5
Tor is symmetric and preserves direct sums in either variable; it vanishes when either input is free (more generally torsion-free), depends only on the torsion subgroup in the first variable, satisfies Tor(ℤ_n,A)≅ker(n:A→A), and fits into the standard six-term exact sequence associated to a short exact sequence 0→B→C→D→0.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Tor is symmetric and preserves direct sums in either variable; it vanishes when either input is free (more generally torsion-free), depends only on the torsion subgroup in the first variable, satisfies Tor(ℤ_n,A)≅ker(n:A→A), and fits into the standard six-term exact sequence associated to a short exact sequence 0→B→C→D→0. Pinned Mathlib has tensor right-exactness, projective resolutions, Ext/Tor objects, and derived-functor infrastructure, but no checked declaration realizes the complete stated UCT/Tor bundle (including all identifications, splittings, exact sequences, or higher-Tor nonvanishing as applicable). Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 3A.6
For field coefficients: (a) H_n(X;ℚ)≅H_n(X;ℤ)⊗ℚ, so for finitely generated integral homology its ℚ-dimension is the integral rank. (b) If H_n(X;ℤ) and H_{n−1}(X;ℤ) are finitely generated and p is prime, H_n(X;ℤ_p) has one ℤ_p summand for each ℤ summand of H_n(X;ℤ), each ℤ_{p^k} summand of H_n(X;ℤ), and each ℤ_{p^k} summand of H_{n−1}(X;ℤ).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For field coefficients: (a) H_n(X;ℚ)≅H_n(X;ℤ)⊗ℚ, so for finitely generated integral homology its ℚ-dimension is the integral rank. (b) If H_n(X;ℤ) and H_{n−1}(X;ℤ) are finitely generated and p is prime, H_n(X;ℤ_p) has one ℤ_p summand for each ℤ summand of H_n(X;ℤ), each ℤ_{p^k} summand of H_n(X;ℤ), and each ℤ_{p^k} summand of H_{n−1}(X;ℤ). Pinned Mathlib has tensor right-exactness, projective resolutions, Ext/Tor objects, and derived-functor infrastructure, but no checked declaration realizes the complete stated UCT/Tor bundle (including all identifications, splittings, exact sequences, or higher-Tor nonvanishing as applicable). Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 3A.7
- H̃{n} (X; ℤ) = 0 for all n iff H̃{n} (X; ℚ) = 0 and H̃{n} (X; ℤ{p}) = 0 for all n and all primes p. (b) A map f: X {→ } Y induces isomorphisms on homology with Z coefficients iff it induces isomorphisms on homology with ℚ and ℤ_{p} coefficients for all primes p.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (a) H̃{n} (X; ℤ) = 0 for all n iff H̃{n} (X; ℚ) = 0 and H̃{n} (X; ℤ{p}) = 0 for all n and all primes p. (b) A map f: X {→ } Y induces isomorphisms on homology with Z coefficients iff it induces isomorphisms on homology with ℚ and ℤ_{p} coefficients for all primes p. Pinned Mathlib has tensor right-exactness, projective resolutions, Ext/Tor objects, and derived-functor infrastructure, but no checked declaration realizes the complete stated UCT/Tor bundle (including all identifications, splittings, exact sequences, or higher-Tor nonvanishing as applicable). Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — higher Tor over a ring
For modules over a ring R, free resolutions define functors Tor_n^R(A,B) by the same procedure as for abelian groups; unlike over ℤ, these groups need not vanish for n>1.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For modules over a ring R, free resolutions define functors Tor_n^R(A,B) by the same procedure as for abelian groups; unlike over ℤ, these groups need not vanish for n>1. Pinned Mathlib has tensor right-exactness, projective resolutions, Ext/Tor objects, and derived-functor infrastructure, but no checked declaration realizes the complete stated UCT/Tor bundle (including all identifications, splittings, exact sequences, or higher-Tor nonvanishing as applicable). Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — cross product in homology
The homology cross product H_i(X;R)×H_j(Y;R)→H_{i+j}(X×Y;R) is induced from the cellular/singular chain product and satisfies the usual signed boundary formula.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The homology cross product H_i(X;R)×H_j(Y;R)→H_{i+j}(X×Y;R) is induced from the cellular/singular chain product and satisfies the usual signed boundary formula. Generic tensor/homological-complex machinery exists, but no checked singular/cellular homology cross product or Künneth theorem realizes the full row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 3B.1
The boundary map in the cellular chain complex C_{} (X × Y) is determined by the boundary maps in the cellular chain complexes C_{} (X) and C_{*} (Y) via the formula d (e^{i} {× } e^{j}) = d e^{i} {× } e^{j} + (- 1)^{i} e^{i} {× } d e^{j}.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The boundary map in the cellular chain complex C_{} (X × Y) is determined by the boundary maps in the cellular chain complexes C_{} (X) and C_{*} (Y) via the formula d (e^{i} {× } e^{j}) = d e^{i} {× } e^{j} + (- 1)^{i} e^{i} {× } d e^{j}. Generic tensor/homological-complex machinery exists, but no checked singular/cellular homology cross product or Künneth theorem realizes the full row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 3B.2
For cellular maps f: X → Z and g: Y → W, the cellular chain maps f_{}: C_{} (X) → C_{} (Z), g_{}: C_{} (Y) → C_{} (W), and (f × g){}: C_{} (X × Y) {→ } C{} (Z × W) are related by the formula (f × g){} = f_{} × g{}.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For cellular maps f: X → Z and g: Y → W, the cellular chain maps f_{}: C_{} (X) → C_{} (Z), g_{}: C_{} (Y) → C_{} (W), and (f × g){}: C{} (X × Y) {→ } C_{} (Z × W) are related by the formula (f × g){} = f{} × g_{}. Generic tensor/homological-complex machinery exists, but no checked singular/cellular homology cross product or Künneth theorem realizes the full row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3B.3
Consider X × S^{k} where we give S^{k} its usual CW structure with two cells. The boundary formula in C_{} (X × S^{k}) takes the form d (a × b) = d a × b since d: =: 0 in C_{} (S^{k}). Hence H_{n} (X × S^{k}; ℤ) ≅ H_{n} (X; ℤ) ⊕ H_{n - k} (X; ℤ) for all n.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Consider X × S^{k} where we give S^{k} its usual CW structure with two cells. The boundary formula in C_{} (X × S^{k}) takes the form d (a × b) = d a × b since d: =: 0 in C_{} (S^{k}). Hence H_{n} (X × S^{k}; ℤ) ≅ H_{n} (X; ℤ) ⊕ H_{n - k} (X; ℤ) for all n. Generic tensor/homological-complex machinery exists, but no checked singular/cellular homology cross product or Künneth theorem realizes the full row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3B.4
Let X=S^1∪_m e^2 and Y=S^1∪_n e^2, with attaching maps of degrees m,n and q=gcd(m,n). Then H_1(X×Y;ℤ)≅ℤ_m⊕ℤ_n and H_2(X×Y;ℤ)≅H_3(X×Y;ℤ)≅ℤ_q. The H_3 class is not a cross product; it is the Tor contribution, while H_2 is H_1(X)⊗H_1(Y).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let X=S^1∪_m e^2 and Y=S^1∪_n e^2, with attaching maps of degrees m,n and q=gcd(m,n). Then H_1(X×Y;ℤ)≅ℤ_m⊕ℤ_n and H_2(X×Y;ℤ)≅H_3(X×Y;ℤ)≅ℤ_q. The H_3 class is not a cross product; it is the Tor contribution, while H_2 is H_1(X)⊗H_1(Y). Generic tensor/homological-complex machinery exists, but no checked singular/cellular homology cross product or Künneth theorem realizes the full row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 3B.5
Let R be a PID and let C,C′ be chain complexes of R-modules with every C_i free. For each n there is a natural short exact sequence 0→⊕_i H_i(C)⊗R H{n-i}(C′)→H_n(C⊗_R C′)→⊕i Tor_R(H_i(C),H{n-i-1}(C′))→0, and it splits (not naturally in general).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let R be a PID and let C,C′ be chain complexes of R-modules with every C_i free. For each n there is a natural short exact sequence 0→⊕_i H_i(C)⊗R H{n-i}(C′)→H_n(C⊗_R C′)→⊕i Tor_R(H_i(C),H{n-i-1}(C′))→0, and it splits (not naturally in general). Generic tensor/homological-complex machinery exists, but no checked singular/cellular homology cross product or Künneth theorem realizes the full row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 3B.6
Künneth theorem: if X,Y are CW complexes and R is a PID, then for every n there is a natural split short exact sequence 0→⊕_i(H_i(X;R)⊗R H{n−i}(Y;R))→H_n(X×Y;R)→⊕i Tor_R(H_i(X;R),H{n−i−1}(Y;R))→0.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Künneth theorem: if X,Y are CW complexes and R is a PID, then for every n there is a natural split short exact sequence 0→⊕_i(H_i(X;R)⊗R H{n−i}(Y;R))→H_n(X×Y;R)→⊕i Tor_R(H_i(X;R),H{n−i−1}(Y;R))→0. Generic tensor/homological-complex machinery exists, but no checked singular/cellular homology cross product or Künneth theorem realizes the full row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 3B.7
If F is a field and X and Y are CW complexes, then the cross product map h: ⊕{i} (H{i} (X; F) ⊗{F} H{n - i} (Y; F)) → H_{n} (X × Y; F) is an isomorphism for all n.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If F is a field and X and Y are CW complexes, then the cross product map h: ⊕{i} (H{i} (X; F) ⊗{F} H{n - i} (Y; F)) → H_{n} (X × Y; F) is an isomorphism for all n. Generic tensor/homological-complex machinery exists, but no checked singular/cellular homology cross product or Künneth theorem realizes the full row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — singular-chain cross product
For singular simplices f:Δ^m→X and g:Δ^n→Y, subdivide Δm×Δn by monotone lattice paths σ and define f×g=Σ_σ(-1)^{|σ|}(f×g)ℓ_σ. This satisfies ∂(f×g)=∂f×g+(-1)^m f×∂g and induces the homology cross product.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For singular simplices f:Δ^m→X and g:Δ^n→Y, subdivide Δm×Δn by monotone lattice paths σ and define f×g=Σ_σ(-1)^{}(f×g)ℓ_σ. This satisfies ∂(f×g)=∂f×g+(-1)^m f×∂g and induces the homology cross product. Generic tensor/homological-complex machinery exists, but no checked singular/cellular homology cross product or Künneth theorem realizes the full row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — cellular cohomology cross product
For CW complexes X,Y, cellular cochains φ∈C^k(X;R), ψ∈C^ℓ(Y;R) have cross product defined by (φ×ψ)(e_αm×e_βn)=φ(e_αm)ψ(e_βn), using the convention that a k-cochain vanishes on cells of other dimensions.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For CW complexes X,Y, cellular cochains φ∈C^k(X;R), ψ∈C^ℓ(Y;R) have cross product defined by (φ×ψ)(e_αm×e_βn)=φ(e_αm)ψ(e_βn), using the convention that a k-cochain vanishes on cells of other dimensions. Generic tensor/homological-complex machinery exists, but no checked singular/cellular homology cross product or Künneth theorem realizes the full row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — H-space
A based space (X,e) is an H-space if it has a multiplication μ:X×X→X for which left and right multiplication by e are homotopic to id_X through basepoint-preserving homotopies.
Formalized. Mathlib/Topology/Homotopy/HSpaces.lean::HSpace — HSpace X consists of a continuous multiplication X×X→X, a distinguished element e, and basepoint-relative homotopies from left and right multiplication by e to the identity. This is exactly Hatcher’s based H-space definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition/construction — infinite symmetric product
For a based space X, SP_n(X)=X^n/Σ_n; adjoining the basepoint gives inclusions SP_n(X)→SP_{n+1}(X), and SP(X)=⋃_n SP_n(X) is the infinite symmetric product.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a based space X, SP_n(X)=X^n/Σ_n; adjoining the basepoint gives inclusions SP_n(X)→SP_{n+1}(X), and SP(X)=⋃_n SP_n(X) is the infinite symmetric product. No checked infinite symmetric-product construction with the stated homotopy/homology property was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — Hopf algebra
A Hopf algebra here is a graded algebra A over a commutative ring equipped with a coproduct Δ:A→A⊗A and augmentation satisfying the stated algebra-homomorphism, coassociativity/counit, and graded sign conditions.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A Hopf algebra here is a graded algebra A over a commutative ring equipped with a coproduct Δ:A→A⊗A and augmentation satisfying the stated algebra-homomorphism, coassociativity/counit, and graded sign conditions. Bialgebra/HopfAlgebra and monoid-algebra instances exist, but Hatcher’s structure is graded with Koszul tensor signs and the stated concrete primitive/polynomial/exterior conclusions are not packaged by a checked declaration. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3C.1
One of the simplest Hopf algebras is a polynomial ring R [ α ]. The coproduct Δ (α) must equal α ⊗ 1 + 1 ⊗ α since the only elements of R [ α ] of lower dimension than α are the elements of R in dimension zero, so the terms α_{i}^{′} and α_{i}^{′ ′} in the coproduct formula { Δ (α) = α ⊗ 1 + 1 ⊗ α + ∑{i} α{i}^{′} ⊗ α_{i}^{′ ′} } must be zero. Thus if we set β: =: α^{2}, then β is even-dimensional and we have { Δ (α^{2 n}) = Δ (β^{n}) = (β ⊗ 1 + 1 ⊗ β)^{n} = ∑{i} { binom {n } {i } } β^{i} ⊗ β^{n - i} } and { Δ (α^{2 n + 1}) = Δ (α β^{n}) = Δ (α) Δ (β^{n}) = ∑{i} binom {n } {i } α β^{i} ⊗ β^{n - i} + ∑_{i} binom {n } {i } β^{i} ⊗ α β^{n - i} }.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: One of the simplest Hopf algebras is a polynomial ring R [ α ]. The coproduct Δ (α) must equal α ⊗ 1 + 1 ⊗ α since the only elements of R [ α ] of lower dimension than α are the elements of R in dimension zero, so the terms α_{i}^{′} and α_{i}^{′ ′} in the coproduct formula { Δ (α) = α ⊗ 1 + 1 ⊗ α + ∑{i} α{i}^{′} ⊗ α_{i}^{′ ′} } must be zero. Thus if we set β: =: α^{2}, then β is even-dimensional and we have { Δ (α^{2 n}) = Δ (β^{n}) = (β ⊗ 1 + 1 ⊗ β)^{n} = ∑{i} { binom {n } {i } } β^{i} ⊗ β^{n - i} } and { Δ (α^{2 n + 1}) = Δ (α β^{n}) = Δ (α) Δ (β^{n}) = ∑{i} binom {n } {i } α β^{i} ⊗ β^{n - i} + ∑_{i} binom {n } {i } β^{i} ⊗ α β^{n - i} }. Bialgebra/HopfAlgebra and monoid-algebra instances exist, but Hatcher’s structure is graded with Koszul tensor signs and the stated concrete primitive/polynomial/exterior conclusions are not packaged by a checked declaration. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3C.2
The exterior algebra Λ_{R} [ α ] on an odd-dimensional generator α is a Hopf algebra, with Δ (α) = α ⊗ 1 + 1 ⊗ α. Note that if α were even-dimensional we would instead have Δ (α)^{2} = α^{2} ∘ 1 + 2 α ⊗ α + 1 ⊗ α^{2}, which would be 0 in Λ_{R} [ α ] ⊗ Λ_{R} [ α ] only if 2 = 0 in R.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The exterior algebra Λ_{R} [ α ] on an odd-dimensional generator α is a Hopf algebra, with Δ (α) = α ⊗ 1 + 1 ⊗ α. Note that if α were even-dimensional we would instead have Δ (α)^{2} = α^{2} ∘ 1 + 2 α ⊗ α + 1 ⊗ α^{2}, which would be 0 in Λ_{R} [ α ] ⊗ Λ_{R} [ α ] only if 2 = 0 in R. Bialgebra/HopfAlgebra and monoid-algebra instances exist, but Hatcher’s structure is graded with Koszul tensor signs and the stated concrete primitive/polynomial/exterior conclusions are not packaged by a checked declaration. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — primitive element
An element α of a Hopf algebra is primitive when Δ(α)=α⊗1+1⊗α.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: An element α of a Hopf algebra is primitive when Δ(α)=α⊗1+1⊗α. Bialgebra/HopfAlgebra and monoid-algebra instances exist, but Hatcher’s structure is graded with Koszul tensor signs and the stated concrete primitive/polynomial/exterior conclusions are not packaged by a checked declaration. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3C.3
If F[α]/(α^n) is a Hopf algebra with α primitive, and either |α| is even or char(F)=2, then all binomial coefficients (n choose i), 0<i<n, vanish in F. Hence this is impossible in characteristic 0, while in characteristic p>0 it forces n to be a power of p; conversely F[α]/(α{pi}) has such a Hopf structure (with α even-dimensional when p is odd).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If F[α]/(α^n) is a Hopf algebra with α primitive, and either is even or char(F)=2, then all binomial coefficients (n choose i), 0<i<n, vanish in F. Hence this is impossible in characteristic 0, while in characteristic p>0 it forces n to be a power of p; conversely F[α]/(α{pi}) has such a Hopf structure (with α even-dimensional when p is odd). Bialgebra/HopfAlgebra and monoid-algebra instances exist, but Hatcher’s structure is graded with Koszul tensor signs and the stated concrete primitive/polynomial/exterior conclusions are not packaged by a checked declaration. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 3C.4
If A is a commutative, associative Hopf algebra over a field F of characteristic 0, and A^{n} is finite-dimensional over F for each n, then A is isomorphic as an algebra to the tensor product of an exterior algebra on odd-dimensional generators and a polynomial algebra on even-dimensional generators.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If A is a commutative, associative Hopf algebra over a field F of characteristic 0, and A^{n} is finite-dimensional over F for each n, then A is isomorphic as an algebra to the tensor product of an exterior algebra on odd-dimensional generators and a polynomial algebra on even-dimensional generators. Bialgebra/HopfAlgebra and monoid-algebra instances exist, but Hatcher’s structure is graded with Koszul tensor signs and the stated concrete primitive/polynomial/exterior conclusions are not packaged by a checked declaration. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3C.5
For n even, H^*(J(S^n);ℤ)=Γ_ℤ[α] with generators α_i in degree ni, multiplication α_iα_j=binom(i+j,i)α_{i+j}, and coproduct Δ(α_k)=∑i α_i⊗α{k−i}. Over ℤ_p the algebra is ⊗{i≥0}ℤ_p[α_{p^i}]/(α{pi}p), though this is not an isomorphism of Hopf algebras for i>0.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For n even, H^(J(S^n);ℤ)=Γ_ℤ[α] with generators α_i in degree ni, multiplication α_iα_j=binom(i+j,i)α_{i+j}, and coproduct Δ(α_k)=∑i α_i⊗α{k−i}. Over ℤ_p the algebra is ⊗{i≥0}ℤ_p[α*{p^i}]/(α_{pi}p), though this is not an isomorphism of Hopf algebras for i>0. Bialgebra/HopfAlgebra and monoid-algebra instances exist, but Hatcher’s structure is graded with Koszul tensor signs and the stated concrete primitive/polynomial/exterior conclusions are not packaged by a checked declaration. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 3C.6
If p is a prime, then { binom {n } {k } ≡ ∏{i} binom { n{i} } { k_{i} } } mod p where { n = ∑{i} n{i} p^{i} } and { k = ∑{i} k{i} p^{i} } with 0 ≤ n_{i} < p and 0 ≤ k_{i} < p are the p adic representations of n and k.
Formalized. Mathlib/Data/Nat/Choose/Lucas.lean::Choose.lucas_theorem — Choose.lucas_theorem is Lucas’s congruence: modulo a prime p, binomial(n,k) is the product of the binomial coefficients of the base-p digits of n and k, exactly the source lemma.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Construction — Pontryagin product
For an H-space X with multiplication μ, the Pontryagin product on homology is H_i(X)×H_j(X)→H_{i+j}(X×X)→^{μ_*}H_{i+j}(X).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For an H-space X with multiplication μ, the Pontryagin product on homology is H_i(X)×H_j(X)→H_{i+j}(X×X)→^{μ_*}H_{i+j}(X). HSpace is formalized, but no checked singular-homology Pontryagin product or corresponding Hopf-algebra calculation is connected to it. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3C.7
Let us compute the Pontryagin product for J (S^{n}). Here there is one cell e^{i n} for each i ≥ 0, and μ takes the product cell e^{i n} × e^{j n} homeomorphically onto the cell e^{(i + j) n}. This means that H_{*} (J (S^{n}); ℤ) is simply the polynomial ring ℤ [ x ] on an n dimensional generator x.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let us compute the Pontryagin product for J (S^{n}). Here there is one cell e^{i n} for each i ≥ 0, and μ takes the product cell e^{i n} × e^{j n} homeomorphically onto the cell e^{(i + j) n}. This means that H_{*} (J (S^{n}); ℤ) is simply the polynomial ring ℤ [ x ] on an n dimensional generator x. HSpace is formalized, but no checked singular-homology Pontryagin product or corresponding Hopf-algebra calculation is connected to it. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 3C.8
If X is a connected CW complex with H_{} (X; R) a free R module, then H_{} (J (X); R) is isomorphic to the tensor algebra T H̃_{*} (X; R).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If X is a connected CW complex with H_{} (X; R) a free R module, then H_{} (J (X); R) is isomorphic to the tensor algebra T H̃_{*} (X; R). HSpace is formalized, but no checked singular-homology Pontryagin product or corresponding Hopf-algebra calculation is connected to it. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3C.9
Consider J (S^{n}) with n even, so H^{*} (J (S^{n}); ℤ) is the divided polynomial algebra Γ_{ℤ} [ α ]. Thus Δ_{i j} takes α_{i + j} to α_{i} ⊗ α_{j}, so if x_{i} is the generator of H_{i n} (J (S^{n}); ℤ) dual to α_{i}, then x_{i} x_{j} = x_{i + j}.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Consider J (S^{n}) with n even, so H^{*} (J (S^{n}); ℤ) is the divided polynomial algebra Γ_{ℤ} [ α ]. Thus Δ_{i j} takes α_{i + j} to α_{i} ⊗ α_{j}, so if x_{i} is the generator of H_{i n} (J (S^{n}); ℤ) dual to α_{i}, then x_{i} x_{j} = x_{i + j}. HSpace is formalized, but no checked singular-homology Pontryagin product or corresponding Hopf-algebra calculation is connected to it. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 3C.10
Let A be a Hopf algebra over R that is a finitely generated free R module in each dimension. Then the product π: A ⊗ A {→ } A and coproduct Δ {: } A → A ⊗ A have duals π^{}: A^{} {→ } A^{} ⊗ A^{} and Δ^{}: A^{} ⊗ A^{} → A^{} that give A^{*} the structure of a Hopf algebra.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let A be a Hopf algebra over R that is a finitely generated free R module in each dimension. Then the product π: A ⊗ A {→ } A and coproduct Δ {: } A → A ⊗ A have duals π^{}: A^{} {→ } A^{} ⊗ A^{} and Δ^{}: A^{} ⊗ A^{} → A^{} that give A^{*} the structure of a Hopf algebra. HSpace is formalized, but no checked singular-homology Pontryagin product or corresponding Hopf-algebra calculation is connected to it. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3C.11
For a primitive polynomial generator x, if |x| is even (or 2=0 in R), the Hopf-algebra dual of R[x] is the divided polynomial algebra Γ_R[α]. If |x| is odd, writing y=x^2, the dual is Λ_R[α]⊗Γ_R[β], with α dual to x and β dual to y.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a primitive polynomial generator x, if is even (or 2=0 in R), the Hopf-algebra dual of R[x] is the divided polynomial algebra Γ_R[α]. If is odd, writing y=x^2, the dual is Λ_R[α]⊗Γ_R[β], with α dual to x and β dual to y. HSpace is formalized, but no checked singular-homology Pontryagin product or corresponding Hopf-algebra calculation is connected to it. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — orthogonal group O(n)
O(n) is the group of isometries of ℝ^n fixing the origin, equivalently the n×n real matrices A satisfying AA^t=I, with the subspace topology from ℝ^{n²}.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: O(n) is the group of isometries of ℝ^n fixing the origin, equivalently the n×n real matrices A satisfying AA^t=I, with the subspace topology from ℝ^{n²}. Matrix.orthogonalGroup and mem_orthogonalGroup_iff give the algebraic group and AAᵗ=I characterization, but the type has no inferred TopologicalSpace instance at P, so the required subspace topology clause is missing. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — special orthogonal group SO(n)
SO(n) is the kernel of det:O(n)→{±1}, the subgroup of orthogonal matrices of determinant 1.
Formalized. Mathlib/LinearAlgebra/UnitaryGroup.lean::Matrix.specialOrthogonalGroup, Matrix.mem_specialOrthogonalGroup_iff — Matrix.specialOrthogonalGroup n R is the determinant-one submonoid of the orthogonal group (defined through the kernel condition), and mem_specialOrthogonalGroup_iff states membership iff the matrix is orthogonal and has determinant 1. Over ℝ this is exactly SO(n), the kernel of determinant on O(n).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 3D.1
The maps ρ {φ }^{I} {: } D^{I} → SO (n), for I ranging over all admissible sequences, are the characteristic maps of a CW structure on SO (n) for which the map ρ: P^{n - 1} × P^{n - 2} × … × P^{1} → SO (n) is cellular.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The maps ρ {φ }^{I} {: } D^{I} → SO (n), for I ranging over all admissible sequences, are the characteristic maps of a CW structure on SO (n) for which the map ρ: P^{n - 1} × P^{n - 2} × … × P^{1} → SO (n) is cellular. The algebraic groups O(n)/SO(n) are present, but no checked CW/cohomology computation or real Stiefel-manifold interface realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 3D.2
- H^{} (SO (n); ℤ_{2}) ≅ ⊗{i odd} ℤ{2} [ β_{i} ] / (β_{i} ^ { p_{i} }) where | β_{i} | = i and p_{i} is the smallest power of 2 such that | β_{i} ^ { p_{i} } | ≥ n. (b) The Pontryagin ring H_{} (SO (n); ℤ_{2}) is the exterior algebra Λ _ { ℤ_{2} } [ e^{1}, …, e^{n - 1} ].
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: (a) H^{} (SO (n); ℤ_{2}) ≅ ⊗{i odd} ℤ{2} [ β_{i} ] / (β_{i} ^ { p_{i} }) where β_{i} = i and p_{i} is the smallest power of 2 such that β_{i} ^ { p_{i} } ≥ n. (b) The Pontryagin ring H_{} (SO (n); ℤ_{2}) is the exterior algebra Λ _ { ℤ_{2} } [ e^{1}, …, e^{n - 1} ]. The algebraic groups O(n)/SO(n) are present, but no checked CW/cohomology computation or real Stiefel-manifold interface realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 3D.3
The integral homology H_*(SO(n);ℤ) is a direct sum of copies of ℤ and ℤ_2; in particular it has no odd-primary torsion.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The integral homology H_*(SO(n);ℤ) is a direct sum of copies of ℤ and ℤ_2; in particular it has no odd-primary torsion. The algebraic groups O(n)/SO(n) are present, but no checked CW/cohomology computation or real Stiefel-manifold interface realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 3D.4
Modulo torsion, the Pontryagin ring is exterior: H_^{free}(SO(2k+1);ℤ)≅Λ_ℤ[a_3,a_7,…,a_{4k−1}] and H_^{free}(SO(2k+2);ℤ)≅Λ_ℤ[a_3,a_7,…,a_{4k−1},a′_{2k+1}], with |a_i|=i. These generators are primitive, so the dual free cohomology Hopf algebra is exterior on the dual generators.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Modulo torsion, the Pontryagin ring is exterior: H_^{free}(SO(2k+1);ℤ)≅Λ_ℤ[a_3,a_7,…,a_{4k−1}] and H_^{free}(SO(2k+2);ℤ)≅Λ_ℤ[a_3,a_7,…,a_{4k−1},a′_{2k+1}], with _i=i. These generators are primitive, so the dual free cohomology Hopf algebra is exterior on the dual generators. The algebraic groups O(n)/SO(n) are present, but no checked CW/cohomology computation or real Stiefel-manifold interface realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — real Stiefel manifold
The Stiefel manifold V_{n,k} is the space of orthonormal k-frames in ℝ^n, topologized as a subspace of (S{n−1})k.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The Stiefel manifold V_{n,k} is the space of orthonormal k-frames in ℝ^n, topologized as a subspace of (S{n−1})k. The algebraic groups O(n)/SO(n) are present, but no checked CW/cohomology computation or real Stiefel-manifold interface realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — Bockstein homomorphism
The connecting homomorphism Hn(X;K)→H{n+1}(X;G) associated to a short exact coefficient sequence 0→G→H→K→0 is called a Bockstein homomorphism.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The connecting homomorphism Hn(X;K)→H{n+1}(X;G) associated to a short exact coefficient sequence 0→G→H→K→0 is called a Bockstein homomorphism. No checked Bockstein operation or the stated singular-cohomology ring/computation was found in pinned/current Mathlib. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3E.1
Let X be a K (ℤ_{m}, 1), for example ℝP^{∞} when m = 2 or an infinite-dimensional lens space with fundamental group ℤ_{m} for arbitrary m. From the homology calculations in Examples 2.42 and 2.43 together with the universal coefficient theorem or cellular cohomology we have H^{n} (X; ℤ_{m}) ≅ ℤ_{m} for all n.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let X be a K (ℤ_{m}, 1), for example ℝP^{∞} when m = 2 or an infinite-dimensional lens space with fundamental group ℤ_{m} for arbitrary m. From the homology calculations in Examples 2.42 and 2.43 together with the universal coefficient theorem or cellular cohomology we have H^{n} (X; ℤ_{m}) ≅ ℤ_{m} for all n. No checked Bockstein operation or the stated singular-cohomology ring/computation was found in pinned/current Mathlib. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3E.2
Cup Products in Lens Spaces. The cup product structure for lens spaces was computed in Example 3.41 via Poincar´e duality, but using Bocksteins we can deduce it from the cup product structure in ℂP^{∞}, which was computed in Theorem 3.19 without Poincar´e duality. Since H^{*} (ℂP^{∞}; ℤ_{m}) is a polynomial ring, we deduce that if γ ∈ H^{2} (L; ℤ_{m}) is a generator, then y^{k} generates H^{2 k} (L; ℤ_{m}) for all k.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Cup Products in Lens Spaces. The cup product structure for lens spaces was computed in Example 3.41 via Poincar´e duality, but using Bocksteins we can deduce it from the cup product structure in ℂP^{∞}, which was computed in Theorem 3.19 without Poincar´e duality. Since H^{*} (ℂP^{∞}; ℤ_{m}) is a polynomial ring, we deduce that if γ ∈ H^{2} (L; ℤ_{m}) is a generator, then y^{k} generates H^{2 k} (L; ℤ_{m}) for all k. No checked Bockstein operation or the stated singular-cohomology ring/computation was found in pinned/current Mathlib. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 3E.3
Assume the integral homology of X is finitely generated and p is prime. In Bockstein cohomology BH^(X;ℤ_p), each ℤ summand of H^n(X;ℤ) contributes ℤ_p in degree n; each ℤ_{p^k} summand with k>1 contributes ℤ_p in degrees n−1 and n; a ℤ_p summand gives two ordinary mod-p summands joined isomorphically by the Bockstein and hence contributes nothing to BH^.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Assume the integral homology of X is finitely generated and p is prime. In Bockstein cohomology BH^(X;ℤ_p), each ℤ summand of H^n(X;ℤ) contributes ℤ_p in degree n; each ℤ_{p^k} summand with k>1 contributes ℤ_p in degrees n−1 and n; a ℤ_p summand gives two ordinary mod-p summands joined isomorphically by the Bockstein and hence contributes nothing to BH^. No checked Bockstein operation or the stated singular-cohomology ring/computation was found in pinned/current Mathlib. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 3E.4
In the situation of the preceding proposition, H^{} (X; ℤ) contains no elements of order p^{2} iff the dimension of B H^{n} (X; ℤ_{p}) as a vector space over ℤ_{p} equals the rank of H^{n} (X; ℤ) for all n. In this case ρ: H^{} (X; ℤ) {→ } H^{*} (X; ℤ_{p}) is injective on the p torsion, and the image of this p torsion under ρ is equal to im β.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: In the situation of the preceding proposition, H^{} (X; ℤ) contains no elements of order p^{2} iff the dimension of B H^{n} (X; ℤ_{p}) as a vector space over ℤ_{p} equals the rank of H^{n} (X; ℤ) for all n. In this case ρ: H^{} (X; ℤ) {→ } H^{*} (X; ℤ_{p}) is injective on the p torsion, and the image of this p torsion under ρ is equal to im β. No checked Bockstein operation or the stated singular-cohomology ring/computation was found in pinned/current Mathlib. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3E.5
Bocksteins give H^*(ℝP∞×ℝP∞;ℤ)≅ℤ[λ,μ,ν]/(2λ,2μ,2ν,ν2+λ2μ+λμ^2), where reduction mod 2 sends λ↦x^2, μ↦y^2, and ν↦x2y+xy2.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Bocksteins give H^*(ℝP∞×ℝP∞;ℤ)≅ℤ[λ,μ,ν]/(2λ,2μ,2ν,ν2+λ2μ+λμ^2), where reduction mod 2 sends λ↦x^2, μ↦y^2, and ν↦x2y+xy2. No checked Bockstein operation or the stated singular-cohomology ring/computation was found in pinned/current Mathlib. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3E.6
There are finite CW complexes X₁,X₂,Y with H^(X₁;ℤ)≅H^(X₂;ℤ) as rings, while H^(X₁×Y;ℤ) and H^(X₂×Y;ℤ) are isomorphic only as groups: the product H2×H5→H^7 is nonzero for X₁×Y and zero for X₂×Y. Thus cohomology rings of factors do not determine the product-space cohomology ring.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: There are finite CW complexes X₁,X₂,Y with H^(X₁;ℤ)≅H^(X₂;ℤ) as rings, while H^(X₁×Y;ℤ) and H^(X₂×Y;ℤ) are isomorphic only as groups: the product H2×H5→H^7 is nonzero for X₁×Y and zero for X₂×Y. Thus cohomology rings of factors do not determine the product-space cohomology ring. No checked Bockstein operation or the stated singular-cohomology ring/computation was found in pinned/current Mathlib. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3E.7
Bockstein homomorphisms can be used to get a more complete picture of the structure of H^{} (SO (n); ℤ) than we obtained in the preceding section. It is interesting that the generator y ∈ H^{3} (SO (5); ℤ) ≅ ℤ has y^{2} nontrivial, since this implies that the ring structures of H^{} (SO (5); ℤ) and H^{*} (ℝP^{7} × S^{3}; ℤ) are not isomorphic, even though the cohomology groups and the ℤ_{2} cohomology rings of these two spaces are the same.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Bockstein homomorphisms can be used to get a more complete picture of the structure of H^{} (SO (n); ℤ) than we obtained in the preceding section. It is interesting that the generator y ∈ H^{3} (SO (5); ℤ) ≅ ℤ has y^{2} nontrivial, since this implies that the ring structures of H^{} (SO (5); ℤ) and H^{*} (ℝP^{7} × S^{3}; ℤ) are not isomorphic, even though the cohomology groups and the ℤ_{2} cohomology rings of these two spaces are the same. No checked Bockstein operation or the stated singular-cohomology ring/computation was found in pinned/current Mathlib. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3F.1
For a prime p, consider the sequence ℤ → ℤ → ℤ → … with all maps multiplication by p. Then lim→ G_{i} can be identified with the subgroup ℤ [ 1 / p ] of ℚ consisting of rational numbers with denominator a power of p. More generally, we can realize any subgroup of ℚ as the direct limit of a sequence ℤ → ℤ → ℤ → … with an appropriate choice of maps. For example, if the n^{t h} map is multiplication by n, then the direct limit is ℚ itself.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a prime p, consider the sequence ℤ → ℤ → ℤ → … with all maps multiplication by p. Then lim→ G_{i} can be identified with the subgroup ℤ [ 1 / p ] of ℚ consisting of rational numbers with denominator a power of p. More generally, we can realize any subgroup of ℚ as the direct limit of a sequence ℤ → ℤ → ℤ → … with an appropriate choice of maps. For example, if the n^{t h} map is multiplication by n, then the direct limit is ℚ itself. AddCommGroup.DirectLimit and localization/Prüfer-adjacent algebra exist, but no checked declaration identifies these specific systems with ℤ[1/p], ℚ, ℤ_{p∞}, or the stated Moore-space examples and decompositions. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3F.2
The sequence of injections ℤ_{p} → ℤ _ { p^{2} } → ℤ _ { p^{3} } → …, with p prime, has direct limit a group we denote ℤ _ { p^{∞} }. In fact ℚ / ℤ is isomorphic to the direct sum of the subgroups ℤ [ 1 / p ] / ℤ ≅ ℤ _ { p^{∞} } for all primes p.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The sequence of injections ℤ_{p} → ℤ _ { p^{2} } → ℤ _ { p^{3} } → …, with p prime, has direct limit a group we denote ℤ _ { p^{∞} }. In fact ℚ / ℤ is isomorphic to the direct sum of the subgroups ℤ [ 1 / p ] / ℤ ≅ ℤ _ { p^{∞} } for all primes p. AddCommGroup.DirectLimit and localization/Prüfer-adjacent algebra exist, but no checked declaration identifies these specific systems with ℤ[1/p], ℚ, ℤ_{p∞}, or the stated Moore-space examples and decompositions. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3F.3
Suppose each f_{i} is a map S^{n} → S^{n} of degree p for a fixed prime p. Then H_{n} (T) is the direct limit of the sequence ℤ → ℤ → ℤ → … considered in Example 3F.1 above, and H̃_{k} (T) = 0 for k ≠ n, so T is a Moore space M (ℤ [ 1 / p ], n).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Suppose each f_{i} is a map S^{n} → S^{n} of degree p for a fixed prime p. Then H_{n} (T) is the direct limit of the sequence ℤ → ℤ → ℤ → … considered in Example 3F.1 above, and H̃{k} (T) = 0 for k ≠ n, so T is a Moore space M (ℤ [ 1 / p ], n). AddCommGroup.DirectLimit and localization/Prüfer-adjacent algebra exist, but no checked declaration identifies these specific systems with ℤ[1/p], ℚ, ℤ{p∞}, or the stated Moore-space examples and decompositions. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3F.4
In the preceding example, if we attach a cell e^{n + 1} to the first S^{n} in T via the identity map of S^{n}, we obtain a space X which is a Moore space M (ℤ _ { p^{∞} }, n) since X is the union of its subspaces X_{i} = T_{i} ∪ e^{n + 1}, which are M (ℤ _ { p^{i} }, n) ’s, and the inclusion X_{i} ⊂ X_{i + 1} induces the inclusion ℤ _ { p^{i} } ⊂ ℤ _ { p^{i + 1} } on H_{n}.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: In the preceding example, if we attach a cell e^{n + 1} to the first S^{n} in T via the identity map of S^{n}, we obtain a space X which is a Moore space M (ℤ _ { p^{∞} }, n) since X is the union of its subspaces X_{i} = T_{i} ∪ e^{n + 1}, which are M (ℤ _ { p^{i} }, n) ’s, and the inclusion X_{i} ⊂ X_{i + 1} induces the inclusion ℤ _ { p^{i} } ⊂ ℤ _ { p^{i + 1} } on H_{n}. AddCommGroup.DirectLimit and localization/Prüfer-adjacent algebra exist, but no checked declaration identifies these specific systems with ℤ[1/p], ℚ, ℤ_{p∞}, or the stated Moore-space examples and decompositions. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — inverse limit
For an inverse sequence …→G_2→G_1→G_0, lim←G_i is the subgroup of ∏iG_i consisting of compatible sequences (g_i) with α_i(g_i)=g{i−1}.
Formalized. Mathlib/Algebra/Category/Grp/Limits.lean::AddCommGrpCat.limitCone, AddCommGrpCat.limitConeIsLimit — Limits of diagrams of additive commutative groups are constructed on Functor.sections, i.e. compatible families in the product, and limitConeIsLimit proves the universal property. For an inverse sequence this is exactly the subgroup of ∏ᵢGᵢ satisfying the transition compatibility equations.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 3F.5
If the CW complex X is the union of an increasing sequence of subcomplexes X_{i} and if G is one of the fields ℚ or ℤ_{p}, then λ: H^{n} (X; G) → lim← H^{n} (X_{i}; G) is an isomorphism for all n.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If the CW complex X is the union of an increasing sequence of subcomplexes X_{i} and if G is one of the fields ℚ or ℤ_{p}, then λ: H^{n} (X; G) → lim← H^{n} (X_{i}; G) is an isomorphism for all n. Generic inverse limits of additive commutative groups are formalized, but no checked theorem identifies cohomology of the increasing CW union with the stated inverse limit. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3F.6
Consider the sequence of natural surjections … → ℤ _ { p^{3} } → ℤ _ { p^{2} } → ℤ_{p} with p a prime. Elements of {hat(ℤ) }{p} are infinite sequences (…, a{2}, a_{1}) with a_{i} ∈ ℤ _ { p^{i} } such that α_{i} is the mod p^{i} reduction of a_{i + 1}.
Formalized. Mathlib/NumberTheory/Padics/RingHoms.lean::PadicInt.toZModPow, PadicInt.zmod_cast_comp_toZModPow, PadicInt.lift, PadicInt.lift_spec, PadicInt.lift_unique — The maps toZModPow n : ℤ_[p] → ZMod (p^n) are compatible under reduction. lift, lift_spec, and lift_unique give the universal property for every compatible family of maps to these quotients, so ℤ_[p] realizes the inverse limit of the system …→ℤ/p³→ℤ/p²→ℤ/p as an equivalent ring-level formalization.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Example 3F.7
For the inverse system ⋯→pℤ→pℤ→^pℤ, lim←ℤ=0 and lim←¹ℤ≅ℤ̂_p/ℤ. The latter identifies the cokernel of δ(y₁,y₂,…)= (y₁−py₂,y₂−py₃,…) with p-adic integers modulo the embedded copy of ℤ.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For the inverse system ⋯→pℤ→pℤ→^pℤ, lim←ℤ=0 and lim←¹ℤ≅ℤ̂_p/ℤ. The latter identifies the cokernel of δ(y₁,y₂,…)= (y₁−py₂,y₂−py₃,…) with p-adic integers modulo the embedded copy of ℤ. Generic inverse limits are present, but no checked lim¹ construction or Milnor exact sequence/cohomology calculation matching the row was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 3F.8
If a CW complex X is the union of an increasing sequence of subcomplexes X_i, then every cohomology theory has a natural exact sequence 0→lim^1 h{n-1}(X_i)→hn(X)→lim← h^n(X_i)→0. For every homology theory, the natural map lim→ h_n(X_i)→h_n(X) is an isomorphism.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If a CW complex X is the union of an increasing sequence of subcomplexes X_i, then every cohomology theory has a natural exact sequence 0→lim^1 h{n-1}(X_i)→hn(X)→lim← h^n(X_i)→0. For every homology theory, the natural map lim→ h_n(X_i)→h_n(X) is an isomorphism. Generic inverse limits are present, but no checked lim¹ construction or Milnor exact sequence/cohomology calculation matching the row was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3F.9
As in Example 3F.3, consider the mapping telescope T for the sequence of degree p maps S^{n} → S^{n} → ….. Thus we have the rather strange situation that the CW complex T is the union of subcomplexes T_{i} each having cohomology consisting only of a ℤ in dimension n, but T itself has no cohomology in dimension n and instead has a huge uncountable group hat(ℤ)_{p} / ℤ in dimension n + 1.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: As in Example 3F.3, consider the mapping telescope T for the sequence of degree p maps S^{n} → S^{n} → ….. Thus we have the rather strange situation that the CW complex T is the union of subcomplexes T_{i} each having cohomology consisting only of a ℤ in dimension n, but T itself has no cohomology in dimension n and instead has a huge uncountable group hat(ℤ)_{p} / ℤ in dimension n + 1. Generic inverse limits are present, but no checked lim¹ construction or Milnor exact sequence/cohomology calculation matching the row was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3F.10
For X=M(ℤ_{p^∞},n) written as the increasing union of its finite Moore subspaces X_i, the groups H̃{n+1}(X_i;ℤ)≅ℤ_{pi} form the standard surjective inverse system. Hence H̃^{n+1}(X;ℤ)≅ℤ̂_p and all other reduced integral cohomology groups vanish.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For X=M(ℤ_{p^∞},n) written as the increasing union of its finite Moore subspaces X_i, the groups H̃{n+1}(X_i;ℤ)≅ℤ_{pi} form the standard surjective inverse system. Hence H̃^{n+1}(X;ℤ)≅ℤ̂_p and all other reduced integral cohomology groups vanish. Generic inverse limits are present, but no checked lim¹ construction or Milnor exact sequence/cohomology calculation matching the row was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 3F.11
For 0→A→B→C→0 and an abelian group G there are exact sequences 0→Hom(G,A)→Hom(G,B)→Hom(G,C)→Ext(G,A)→Ext(G,B)→Ext(G,C)→0 and 0→Hom(C,G)→Hom(B,G)→Hom(A,G)→Ext(C,G)→Ext(B,G)→Ext(A,G)→0.
Formalized. Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean::CategoryTheory.Abelian.Ext.addEquiv₀; Mathlib/Algebra/Homology/DerivedCategory/Ext/ExactSequences.lean::CategoryTheory.Abelian.Ext.covariantSequence, CategoryTheory.Abelian.Ext.covariantSequence_exact, CategoryTheory.Abelian.Ext.contravariantSequence, CategoryTheory.Abelian.Ext.contravariantSequence_exact — With n₀=0 and n₁=1, the covariant and contravariant Ext sequences are exact six-term sequences. Ext.addEquiv₀ identifies Ext⁰ with Hom, yielding exactly the two Hom/Ext six-term sequences associated to a short exact sequence of abelian groups.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 3F.12
If A is not finitely generated then either {Hom } (A, ℤ) or Ext (A, ℤ) is uncountable. Hence if H_{n} (X; ℤ) is not finitely generated then either H^{n} (X; ℤ) or H^{n + 1} (X; ℤ) is uncountable.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If A is not finitely generated then either {Hom } (A, ℤ) or Ext (A, ℤ) is uncountable. Hence if H_{n} (X; ℤ) is not finitely generated then either H^{n} (X; ℤ) or H^{n + 1} (X; ℤ) is uncountable. Ext is formalized, but no checked countability/uncountability theorem for Hom or Ext and the stated cohomological corollary was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — p-rank of an abelian group
For a prime p, let A_p be the cokernel of multiplication by p on A; the p-rank of A is dim_{ℤ_p} A_p.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a prime p, let A_p be the cokernel of multiplication by p on A; the p-rank of A is dim_{ℤ_p} A_p. Cokernels, ZMod p, and module dimensions are available, but no checked p-rank invariant packages the stated definition as a named interface. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — transfer for finite-sheeted coverings
For an n-sheeted covering π:X̃→X, the transfer chain map τ:C_k(X)→C_k(X̃) sends a singular simplex to the sum of its n distinct lifts. It induces transfer homomorphisms τ_* in homology and τ^* in cohomology.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For an n-sheeted covering π:X̃→X, the transfer chain map τ:C_k(X)→C_k(X̃) sends a singular simplex to the sum of its n distinct lifts. It induces transfer homomorphisms τ_* in homology and τ^* in cohomology. Mathlib has algebraic group cohomology (including finite cyclic groups) and an unrelated finite-group transfer, but no checked covering-space transfer or bridge from H*(K(G,1)) to these group-cohomology ring computations owns the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 3G.1
Let π {: } tilde(X) → X be an n sheeted covering space defined by an action of a group Γ on tilde(X). Then with coefficients in a field F whose characteristic is 0 or a prime not dividing n, the map π^{}: H^{k} (X; F) → H^{k} ({tilde(X) }; F) is injective with image the subgroup H^{} (tilde(X); F)^{Γ} consisting of classes α such that γ^{*} (α) = α for all γ ∈ Γ.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let π {: } tilde(X) → X be an n sheeted covering space defined by an action of a group Γ on tilde(X). Then with coefficients in a field F whose characteristic is 0 or a prime not dividing n, the map π^{}: H^{k} (X; F) → H^{k} ({tilde(X) }; F) is injective with image the subgroup H^{} (tilde(X); F)^{Γ} consisting of classes α such that γ^{} (α) = α for all γ ∈ Γ. Mathlib has algebraic group cohomology (including finite cyclic groups) and an unrelated finite-group transfer, but no checked covering-space transfer or bridge from H(K(G,1)) to these group-cohomology ring computations owns the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3G.2
Let X = S^{1} ∨ S^{k}, k > 1, with tilde(X) the n-sheeted cover corresponding to the index n subgroup of π_{1} (X), so tilde(X) is a circle with n S^{k} ’s attached at equally spaced points around the circle. Hence for any coefficient group G, the invariant cohomology H^{*} (tilde(X); G) ^ { ℤ_{n} } is all of H^{0} and H^{1}, plus a copy of G in dimension k, the cellular cohomology classes assigning the same element of G to each S^{k}.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let X = S^{1} ∨ S^{k}, k > 1, with tilde(X) the n-sheeted cover corresponding to the index n subgroup of π_{1} (X), so tilde(X) is a circle with n S^{k} ’s attached at equally spaced points around the circle. Hence for any coefficient group G, the invariant cohomology H^{} (tilde(X); G) ^ { ℤ_{n} } is all of H^{0} and H^{1}, plus a copy of G in dimension k, the cellular cohomology classes assigning the same element of G to each S^{k}. Mathlib has algebraic group cohomology (including finite cyclic groups) and an unrelated finite-group transfer, but no checked covering-space transfer or bridge from H(K(G,1)) to these group-cohomology ring computations owns the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3G.3
For π=ℤ_p and Γ=Aut(ℤ_p)≅ℤ_p^×, Γ acts on H^*(K(ℤ_p,1);ℤ_p)=Λ[α]⊗ℤ_p[β] by γ(α)=mα, γ(β)=mβ for a generator m of ℤ_p^×. The invariant ring is Λ[αβ^{p−2}]⊗ℤ_p[β^{p−1}], giving generators in degrees 2p−3 and 2p−2.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For π=ℤ_p and Γ=Aut(ℤ_p)≅ℤ_p^×, Γ acts on H^(K(ℤ_p,1);ℤ_p)=Λ[α]⊗ℤ_p[β] by γ(α)=mα, γ(β)=mβ for a generator m of ℤ_p^×. The invariant ring is Λ[αβ^{p−2}]⊗ℤ_p[β^{p−1}], giving generators in degrees 2p−3 and 2p−2. Mathlib has algebraic group cohomology (including finite cyclic groups) and an unrelated finite-group transfer, but no checked covering-space transfer or bridge from H(K(G,1)) to these group-cohomology ring computations owns the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3G.4
As an easy generalization of the preceding example, replace the group Γ there by a subgroup of Aut (ℤ_{p}) of order d, where d is any divisor of p - 1. The new Γ is generated by the automorphism x ↦ m^{(p - 1) / d} x, and the same analysis shows that we obtain a space with ℤ_{p} cohomology Λ _ { ℤ_{p} } [ x_{2 d - 1} ] ⊗ ℤ_{p} [ y_{2 d} ], subscripts again denoting dimension. For a given choice of d the condition that d divides p - 1 says p ≡ 1 mod d, which is satisfied by infinitely many p ’s, according to a classical theorem of Dirichlet.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: As an easy generalization of the preceding example, replace the group Γ there by a subgroup of Aut (ℤ_{p}) of order d, where d is any divisor of p - 1. The new Γ is generated by the automorphism x ↦ m^{(p - 1) / d} x, and the same analysis shows that we obtain a space with ℤ_{p} cohomology Λ _ { ℤ_{p} } [ x_{2 d - 1} ] ⊗ ℤ_{p} [ y_{2 d} ], subscripts again denoting dimension. For a given choice of d the condition that d divides p - 1 says p ≡ 1 mod d, which is satisfied by infinitely many p ’s, according to a classical theorem of Dirichlet. Mathlib has algebraic group cohomology (including finite cyclic groups) and an unrelated finite-group transfer, but no checked covering-space transfer or bridge from H*(K(G,1)) to these group-cohomology ring computations owns the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3G.5
The two preceding examples can be modified so as to eliminate the exterior algebra factors, by replacing ℤ_{p} by ℤ _ { p^{∞} }, the union of the increasing sequence ℤ_{p} ⊂ ℤ _ { p^{2} } ⊂ ℤ _ { p^{3} } ⊂ …. The homology transfer formula π_{} τ_{} = p shows that the image of the induced map H_{n} (K (ℤ _ { p^{i} }, 1); ℤ) → H_{n} (K (ℤ _ { p^{i + 1} }, 1); ℤ) for n odd contains the multiples of p, hence this map is the inclusion ℤ _ { p^{i} } ↪ ℤ _ { p^{i + 1} }.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The two preceding examples can be modified so as to eliminate the exterior algebra factors, by replacing ℤ_{p} by ℤ _ { p^{∞} }, the union of the increasing sequence ℤ_{p} ⊂ ℤ _ { p^{2} } ⊂ ℤ _ { p^{3} } ⊂ …. The homology transfer formula π_{} τ_{} = p shows that the image of the induced map H_{n} (K (ℤ _ { p^{i} }, 1); ℤ) → H_{n} (K (ℤ _ { p^{i + 1} }, 1); ℤ) for n odd contains the multiples of p, hence this map is the inclusion ℤ _ { p^{i} } ↪ ℤ _ { p^{i + 1} }. Mathlib has algebraic group cohomology (including finite cyclic groups) and an unrelated finite-group transfer, but no checked covering-space transfer or bridge from H*(K(G,1)) to these group-cohomology ring computations owns the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 3F
5 to conclude that H^{} (K (ℤ _ { p^{∞} }, 1); ℤ_{p}) is zero in odd dimensions, while in even dimensions the map H^{} (K (ℤ _ { p^{∞} }, 1); ℤ_{p}) {→ } H^{} (K (ℤ_{p}, 1); ℤ_{p}) induced by the inclusion ℤ_{p} ↪ ℤ _ { p^{∞} } is an isomorphism. Thus H^{} (K (ℤ _ { p^{∞} }, 1); ℤ_{p}) ≅ ℤ_{p} [ β ] as claimed.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: 5 to conclude that H^{} (K (ℤ _ { p^{∞} }, 1); ℤ_{p}) is zero in odd dimensions, while in even dimensions the map H^{} (K (ℤ _ { p^{∞} }, 1); ℤ_{p}) {→ } H^{} (K (ℤ_{p}, 1); ℤ_{p}) induced by the inclusion ℤ_{p} ↪ ℤ _ { p^{∞} } is an isomorphism. Thus H^{} (K (ℤ _ { p^{∞} }, 1); ℤ_{p}) ≅ ℤ_{p} [ β ] as claimed. Mathlib has algebraic group cohomology (including finite cyclic groups) and an unrelated finite-group transfer, but no checked covering-space transfer or bridge from H*(K(G,1)) to these group-cohomology ring computations owns the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3G.6
Now we enlarge the preceding example by taking products and bringing in the permutation group to produce a space with ℤ_{p} cohomology the polynomial ring ℤ_{p} [ y_{2 d}, y_{4 d}, …, y_{2 n d} ] where d is any divisor of p ~ - ~ 1 and p > n. Thus there is a split short exact sequence 0 {→ } (ℤ_{d})^{n} {→ } Γ {→ } Σ_{n} {→ } 0, and the order of Γ is d^{n} n !.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Now we enlarge the preceding example by taking products and bringing in the permutation group to produce a space with ℤ_{p} cohomology the polynomial ring ℤ_{p} [ y_{2 d}, y_{4 d}, …, y_{2 n d} ] where d is any divisor of p ~ - ~ 1 and p > n. Thus there is a split short exact sequence 0 {→ } (ℤ_{d})^{n} {→ } Γ {→ } Σ_{n} {→ } 0, and the order of Γ is d^{n} n !. Mathlib has algebraic group cohomology (including finite cyclic groups) and an unrelated finite-group transfer, but no checked covering-space transfer or bridge from H*(K(G,1)) to these group-cohomology ring computations owns the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3G.7
As a further variant on the preceding example, choose a divisor q of d and replace Γ by its subgroup consisting of matrices for which the product of the q^{t h} powers of the nonzero entries is 1. The group Γ in this case happens to be isomorphic to the dihedral group of order 2 d.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: As a further variant on the preceding example, choose a divisor q of d and replace Γ by its subgroup consisting of matrices for which the product of the q^{t h} powers of the nonzero entries is 1. The group Γ in this case happens to be isomorphic to the dihedral group of order 2 d. Mathlib has algebraic group cohomology (including finite cyclic groups) and an unrelated finite-group transfer, but no checked covering-space transfer or bridge from H*(K(G,1)) to these group-cohomology ring computations owns the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — tensor product over a possibly noncommutative ring
For a right R-module A and a left R-module B, A⊗_R B is generated by a⊗b subject to additivity in both variables and the relation ar⊗b=a⊗rb.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a right R-module A and a left R-module B, A⊗_R B is generated by a⊗b subject to additivity in both variables and the relation ar⊗b=a⊗rb. The standard Mathlib tensor product at P is over a commutative semiring; the right-module/left-module tensor product over a possibly noncommutative ring requested here is not supplied (the right-exactness file explicitly leaves the noncommutative case as future work). Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — module-model homology with local coefficients
If X has universal cover X̃, π=π₁(X), and M is a left ℤ[π]-module, C_n(X;M)=C_n(X̃)⊗_π M with boundary ∂⊗1; its homology is homology with local coefficients.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If X has universal cover X̃, π=π₁(X), and M is a left ℤ[π]-module, C_n(X;M)=C_n(X̃)⊗_π M with boundary ∂⊗1; its homology is homology with local coefficients. Group-ring modules and group (co)homology exist algebraically, but no checked universal-cover/local-coefficient chain construction connects them to singular homology of X as stated. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — module-model cohomology with local coefficients
For the same data, C^n(X;M)=Hom_{ℤ[π]}(C_n(X̃),M); its cohomology is cohomology with local coefficients.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For the same data, C^n(X;M)=Hom_{ℤ[π]}(C_n(X̃),M); its cohomology is cohomology with local coefficients. Group-ring modules and group (co)homology exist algebraically, but no checked universal-cover/local-coefficient chain construction connects them to singular homology of X as stated. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3H.1
Let us check that when M is a trivial ℤ [ π ] module, with γ m = m for all γ ∈ π and m ∈ M, then H_{n} (X; M) is just ordinary homology with coefficients in the abelian group M. Thus we can identify C_{n} ({tilde(X) }) ⊗{π} M with C{n} (X) ⊗ M, the chain group denoted C_{n} (X; M) in ordinary homology theory, so H_{n} (X; M) reduces to ordinary homology with coefficients in M.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let us check that when M is a trivial ℤ [ π ] module, with γ m = m for all γ ∈ π and m ∈ M, then H_{n} (X; M) is just ordinary homology with coefficients in the abelian group M. Thus we can identify C_{n} ({tilde(X) }) ⊗{π} M with C{n} (X) ⊗ M, the chain group denoted C_{n} (X; M) in ordinary homology theory, so H_{n} (X; M) reduces to ordinary homology with coefficients in M. Group-ring modules and group (co)homology exist algebraically, but no checked universal-cover/local-coefficient chain construction connects them to singular homology of X as stated. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3H.2
With M=ℤ[π], local-coefficient homology identifies with homology of the universal cover: H_n(X;ℤ[π])≅H_n(X̃). More generally, for the cover X′→X corresponding to π′⊂π, H_n(X;A[π/π′])≅H_n(X′;A). The analogous cohomology assertions need not hold.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: With M=ℤ[π], local-coefficient homology identifies with homology of the universal cover: H_n(X;ℤ[π])≅H_n(X̃). More generally, for the cover X′→X corresponding to π′⊂π, H_n(X;A[π/π′])≅H_n(X′;A). The analogous cohomology assertions need not hold. Group-ring modules and group (co)homology exist algebraically, but no checked universal-cover/local-coefficient chain construction connects them to singular homology of X as stated. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 3H.3
For a nontrivial ℤ[π]-module structure on ℤ, let X′→X be the corresponding double cover with deck involution τ and C_n^±(X′)={α:τ_♯α=±α}. There are short exact sequences 0→C_n−(X′)→C_n(X′)→Σ C_n^+(X′)→0 and 0→C_n+(X′)→C_n(X′)→Δ C_n^−(X′)→0, with Σ(α)=α+τ_♯α and Δ(α)=α−τ_♯α. Identifying C_+(X′)≅C_(X) and C_−(X′)≅C_(X;tilde(ℤ)) gives the long exact sequence …→H_n(X;tilde(ℤ))→H_n(X′)→H_n(X)→H_{n−1}(X;tilde(ℤ))→….
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a nontrivial ℤ[π]-module structure on ℤ, let X′→X be the corresponding double cover with deck involution τ and C_n^±(X′)={α:τ_♯α=±α}. There are short exact sequences 0→C_n−(X′)→C_n(X′)→Σ C_n^+(X′)→0 and 0→C_n+(X′)→C_n(X′)→Δ C_n^−(X′)→0, with Σ(α)=α+τ_♯α and Δ(α)=α−τ_♯α. Identifying C_+(X′)≅C_(X) and C_−(X′)≅C_(X;tilde(ℤ)) gives the long exact sequence …→H_n(X;tilde(ℤ))→H_n(X′)→H_n(X)→H_{n−1}(X;tilde(ℤ))→…. Group-ring modules and group (co)homology exist algebraically, but no checked universal-cover/local-coefficient chain construction connects them to singular homology of X as stated. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — bundle of groups
A bundle of groups p:E→X has a group structure on each fiber, locally identified by homeomorphisms p^{-1}(U)≅U×G that are group isomorphisms on fibers.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A bundle of groups p:E→X has a group structure on each fiber, locally identified by homeomorphisms p^{-1}(U)≅U×G that are group isomorphisms on fibers. Generic fiber/vector bundles and pullbacks exist, but no checked bundle-of-groups structure with fiberwise group-isomorphism trivializations/maps realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — bundle-model homology with local coefficients
For a bundle E of abelian groups over X, C_n(X;E) consists of finite sums of singular n-simplices equipped with lifts to E; restricting these lifts to faces defines ∂, and H_n(X;E) is the homology of this chain complex.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a bundle E of abelian groups over X, C_n(X;E) consists of finite sums of singular n-simplices equipped with lifts to E; restricting these lifts to faces defines ∂, and H_n(X;E) is the homology of this chain complex. Generic fiber/vector bundles and pullbacks exist, but no checked bundle-of-groups structure with fiberwise group-isomorphism trivializations/maps realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 3H.4
If X is a path-connected space having a universal covering space, then the groups H_{n} (X; E) are naturally isomorphic to the homology groups H_{n} (X; G) with local coefficients in the ℤ [ π ] module G associated to E, where π = π_{1} (X).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If X is a path-connected space having a universal covering space, then the groups H_{n} (X; E) are naturally isomorphic to the homology groups H_{n} (X; G) with local coefficients in the ℤ [ π ] module G associated to E, where π = π_{1} (X). Generic fiber/vector bundles and pullbacks exist, but no checked bundle-of-groups structure with fiberwise group-isomorphism trivializations/maps realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — bundle map
For bundles of groups E→X and E′→X′, a commutative square over f:X→X′ is a bundle map when the map E→E′ restricts to an isomorphism on every fiber.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For bundles of groups E→X and E′→X′, a commutative square over f:X→X′ is a bundle map when the map E→E′ restricts to an isomorphism on every fiber. Generic fiber/vector bundles and pullbacks exist, but no checked bundle-of-groups structure with fiberwise group-isomorphism trivializations/maps realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — pullback bundle
For f:X→X′ and a bundle of groups E′→X′, the pullback f^*(E′) has fiber over x identified with the fiber of E′ over f(x); it is the induced bundle over X.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For f:X→X′ and a bundle of groups E′→X′, the pullback f^*(E′) has fiber over x identified with the fiber of E′ over f(x); it is the induced bundle over X. Generic fiber/vector bundles and pullbacks exist, but no checked bundle-of-groups structure with fiberwise group-isomorphism trivializations/maps realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — cohomology with local coefficients
Local-coefficient cochains are Hom over the fundamental-group action/equivalently fiber-valued cochains with transport; the corresponding coboundary defines cohomology with local coefficients.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Local-coefficient cochains are Hom over the fundamental-group action/equivalently fiber-valued cochains with transport; the corresponding coboundary defines cohomology with local coefficients. No checked singular cohomology with local coefficients or twisted Poincaré-duality interface was found; module and bundle ingredients remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 3H.5
If X is a finite CW complex with universal cover tilde(X) and fundamental group π, then for all n, H^{n} (X; ℤ [ π ]) is isomorphic to H_{c}^{n} (tilde(X); ℤ), cohomology of tilde(X) with compact supports and ordinary integer coefficients.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If X is a finite CW complex with universal cover tilde(X) and fundamental group π, then for all n, H^{n} (X; ℤ [ π ]) is isomorphic to H_{c}^{n} (tilde(X); ℤ), cohomology of tilde(X) with compact supports and ordinary integer coefficients. No checked singular cohomology with local coefficients or twisted Poincaré-duality interface was found; module and bundle ingredients remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — relative cohomology with compact supports
For a closed subset A⊂X, compactly supported relative cohomology H_c^n(X,A;G) is defined compatibly with the inclusion A↪X, so the basic relative theory extends to compact supports.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a closed subset A⊂X, compactly supported relative cohomology H_c^n(X,A;G) is defined compatibly with the inclusion A↪X, so the basic relative theory extends to compact supports. No checked singular cohomology with local coefficients or twisted Poincaré-duality interface was found; module and bundle ingredients remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 3H.6
If M is a nonorientable closed connected n manifold then cap product with the pure imaginary fundamental class [ M ] gives isomorphisms H^{k} (M; ℤ) ≅ H_{n - k} (M; {tilde(Z) }) and H^{k} (M; {tilde(Z) }) ≅ H_{n - k} (M; ℤ).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If M is a nonorientable closed connected n manifold then cap product with the pure imaginary fundamental class [ M ] gives isomorphisms H^{k} (M; ℤ) ≅ H_{n - k} (M; {tilde(Z) }) and H^{k} (M; {tilde(Z) }) ≅ H_{n - k} (M; ℤ). No checked singular cohomology with local coefficients or twisted Poincaré-duality interface was found; module and bundle ingredients remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.