Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Finite products and comparison cones have homological finite type
Statement
Assume AC. Let Y be a finite product of CW K(Z/2,q) models with q≥1, including the empty product . Then every H_n(Y;Z) is finitely generated and H^(Y;F)=F in degree zero only for every field F of characteristic different from two. For any continuous f:X→Z between arbitrary spaces, the integral chain cone has an exact sequence 0→coker(H_nX→H_nZ)→H_n(Cone(C_*(f;Z)))→ker(H_{n−1}X→H_{n−1}Z)→0. If H_nZ and H_{n−1}X are finitely generated, its middle group is finitely generated. In particular this holds in every degree for X=MO(r) or MSO(r) and Z=Y a finite product as above. The raw cone is nonnegative and degreewise free, without any finite-rank assertion or topological-cone identification.
Facts & Assumptions
Given: AC; the based CW models of the finite-type lemma; a finite product of these models; a continuous map whose source is a based CW model of the unoriented Thom spaces; and the free integral algebraic mapping cone of the singular chain map.
Each has finitely generated integral homology, finite-dimensional mod-two homology, vanishing rational and odd-primary reduced homology, and is finite 2-primary in positive degrees (Finite type and odd-primary acyclicity of K(F₂,q)); the unoriented and oriented Thom spaces have finitely generated integral homology (Integral finite generation of universal real and oriented Thom homology).
The integral Künneth sequence expresses the homology of a finite product as an extension of sums of tensor and Tor terms of the factors, and over a field the Künneth map is an isomorphism (Topological Kunneth short exact sequence for homology, Field Kunneth isomorphism for homology of products); a finitely generated abelian group decomposes into cyclic summands, and submodules of finitely generated modules over the Noetherian ring are finitely generated (The fundamental theorem of finitely generated abelian groups from PID modules, Every principal ideal domain is Noetherian, Finitely generated modules over a left Noetherian ring are Noetherian).
The mapping cone of a chain map has the degreewise split canonical short exact sequence and the long exact cone sequence computing its homology from the source and target (The mapping cone of a chain map, The canonical mapping-cone sequence is degreewise split short exact, The cone long exact sequence); the integral chain groups are free in each degree (Singular simplices and singular chain groups with coefficients).
AC chooses the factor models and generators of the finitely generated groups (The Axiom of Choice).
Proof
Let Y be a finite product of the K_q models of the finite-type lemma. Integral Künneth expresses H_n of a product as an extension of finite sums of tensor and Tor products of its factors' integral homology groups. PID decomposition and finite induction on the number of factors therefore prove that every H_n(Y;Z) is finitely generated. With R=Q or an odd F_p, field Künneth shows H*(Y;R)=R concentrated in degree zero. An empty product is the point. Infinite products are not covered by this argument and must not replace this finite comparison space without a new justification.
For any continuous map f:X→Y, use the free integral chain complex C_f=Cone(C_*(f;Z)). The published cone long exact sequence gives 0→coker(H_nX→H_nY)→H_n(C_f)→ker(H_{n-1}X→H_{n-1}Y)→0. If H_n(Y;Z) and H_{n-1}(X;Z) are finitely generated, the two outer groups are finitely generated, and lifting generators proves the middle group is finitely generated. In particular X=MO(r), the integral finite-generation theorem, and finite Y, the finite-type lemma, give integral finite generation of cone homology in every degree. This does not require the raw singular chain groups to have finite rank. The algebraic cone is free in each degree because it is the finite direct sum C_n(Y;Z)⊕C_{n-1}(X;Z), so the inspected algebraic cohomology UCT applies directly; no unproved topological mapping-cone identification is needed. This is the relative homology obstruction for the comparison map.
Depends on
- The Axiom of Choice
- Finite type and odd-primary acyclicity of K(F₂,q)
- Integral finite generation of universal real and oriented Thom homology
- Topological Kunneth short exact sequence for homology
- Field Kunneth isomorphism for homology of products
- Cohomology over a field is dual to homology over that field
- The fundamental theorem of finitely generated abelian groups from PID modules
- Every principal ideal domain is Noetherian
- Finitely generated modules over a left Noetherian ring are Noetherian
- The mapping cone of a chain map
- The canonical mapping-cone sequence is degreewise split short exact
- The cone long exact sequence
- Singular simplices and singular chain groups with coefficients
Used by
Dependency tree · two levels
89 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Charles Weibel, An Introduction to Homological Algebra, Chapter 3 (standard reference, not scraped)
- Charles Weibel, An Introduction to Homological Algebra, Chapter 1 (standard reference, not scraped)