How 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.
Thom Spectra and Unoriented Bordism Detection — Examples
1 · Prerequisites
- Abelian Categories
- Binary Operations, Monoids, Groups and Subgroups
- Bocksteins Steenrod Squares and Cohomology Operations
- Cardinal Arithmetic, Cofinality and the Alephs
- Categories, Functors and Natural Transformations
- Chain Complexes and Homology
- Chain Homotopy and the Homotopy Category
- Classification of Covering Spaces
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Composition Series, the Jordan–Hölder Theorem and Solvable Groups
- Congruences, the Integers Modulo n and the Chinese Remainder Theorem
- Connectedness
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Covering Spaces and Lifting
- Cup Cap Cross Products and Cohomology Rings
- Cw Complexes and Cellular Homology
- Derived Functors
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Double Complexes Exact Couples and Convergence
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Exactness and the Member Calculus
- Ext and Balanced Resolutions
- Fibrations Fiber Bundles and Homotopy Exact Sequences
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Free Groups and Presentations
- Free Modules, Exact Sequences, Projective and Injective Modules
- Free Products and Amalgamation
- Function Space Topologies and the Exponential Law
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Hausdorff via the Diagonal
- Hereditary and Productive Behaviour of the Separation Axioms
- Higher Homotopy Groups and Cofiber Sequences
- Homology Axioms Degree and Classical Applications
- Homotopy and Homotopy Equivalence
- Hurewicz Whitehead Freudenthal and Cw Approximation
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Kunneth Exactness and Splittings over Principal Ideal Domains
- Leray–Hirsch, the Thom Isomorphism, and Gysin Sequences
- Limits and Colimits
- Limits of Real Functions
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Local Coefficients, Twisted Homology, and Duality
- Localisation of Modules and Support
- Long Exact Sequences in Homology
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Metric Spaces
- Modules, Submodules, Quotient Modules and the Isomorphism Theorems
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Obstruction Theory, Postnikov Towers, and Classifying Spaces
- Order, Zorn's Lemma, and the Axiom of Choice
- Ordinal Arithmetic and the First Uncountable Ordinal
- Ordinals, Cardinals, and Transfinite Recursion
- Partitions of Unity and Paracompactness
- Polynomial Rings, the Division Algorithm and Roots
- Preadditive and Additive Categories and Biproducts
- Projective and Injective Resolutions
- Reflective Subcategories and the Adjoint Functor Theorems
- Relations, Functions, and Quotients
- Relative Homology Excision and Mayer Vietoris
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Simple Field Extensions and the Construction of the Complex Numbers
- Simplicial Complexes and Simplicial Homology
- Simplicial Subdivision and Simplicial Approximation
- Singular Chains and Singular Homology
- Singular Cohomology and Coefficient Theorems
- Spectra and Stable Homotopy Groups
- Spectral Sequences
- Stiefel Whitney and Euler Classes by Universal Constructions
- Subobject Lattices Generators and the Grothendieck Axioms
- Subspaces, Products, and Quotients
- Suprema and Infima
- Tensor Products of Modules
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Diagram Lemmas in an Abelian Category
- The Field of Fractions and Localisation
- The Fundamental Group
- The Fundamental Group of the Circle
- The Group Algebra and Representations of Finite Groups
- The Seifert–van Kampen Theorem
- The Serre Spectral Sequence and Applications
- The Topology of Euclidean Space
- The ZFC Axioms and the Basic Set Constructions
- Thom Spaces Normal Data and Collapse Maps
- Thom Spectra and Unoriented Bordism Detection
- Topological Spaces and Continuity
- Topological Vector Bundles and Grassmannian Classification
- Topology of ℝ
- Tor Flatness and Global Dimension
- Uniform Spaces: the Three Definitions
- Universal Coefficients and Kunneth Theorems
- Universal Properties, Representables and the Yoneda Lemma
- Urysohn's Lemma and the Tietze Extension Theorem
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
The companion collects four short computations illustrating the page's algebraic and homotopical inputs.
The first tabulates the admissible mod-two square monomials in degrees through together with three sample Adem reductions. The second exhibits the strict metastable Eilenberg–Mac Lane range for , where the endpoint is deliberately excluded. The third computes in stable Thom cohomology and its rank-three and rank-two components, showing how instability kills the rank-two component. The fourth records the rational Hurewicz range for , an isomorphism in degrees , and .
Every example depends only on items of the A page or on its published prerequisite closure, and none depends on another example.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
Low-degree admissible Steenrod monomials
Example
Assume AC. The admissible bases in degrees 0–4 are respectively {1}, {Sq¹}, {Sq²}, {Sq³,Sq²Sq¹}, and {Sq⁴,Sq³Sq¹}. The Adem relations give Sq¹Sq¹=0, Sq¹Sq²=Sq³, and Sq²Sq²=Sq³Sq¹.
Facts & Assumptions
Given: AC; the admissible words of the mod-two square algebra in total degrees through ; and the three displayed composite pairs , , .
The Adem-reduction lemma spans each homogeneous degree by admissible words, and the admissible composites form a basis of the square algebra in each degree (Adem reduction spans by admissible square composites, Admissible composites present the mod-two square algebra).
The Adem relations hold in the square algebra for , and the square algebra and its excess calculus are the local definition.
Verification
List the positive sequences of each total degree and retain those satisfying i_j≥2i_{j+1}; this gives exactly the displayed rows. The Adem-reduction item shows every other word reduces to an admissible combination.
The basis theorem proves the listed words are independent, so the table is a basis calculation rather than a dimension guess. Substitution in the displayed Adem relation gives the three sample reductions.
A strict metastable Eilenberg–Mac Lane range
Example
Assume AC. For K=K(F₂,3), H³(K;F₂)=F₂{ι₃}, H⁴(K;F₂)=F₂{Sq¹ι₃}, and H⁵(K;F₂)=F₂{Sq²ι₃}. The strict operation range has i<3; at degree 6 the polynomial presentation also has ι₃², so the endpoint is excluded.
Facts & Assumptions
Given: AC; the model ; the strict metastable range ; and the low-degree admissible basis , , .
The strict metastable theorem identifies with for by evaluation on (Metastable cohomology of mod-two Eilenberg–Mac Lane spaces).
The admissible composites form a basis of in each degree (Admissible composites present the mod-two square algebra), and the full polynomial presentation of gives the degree-six generators (Polynomial mod-two cohomology of Eilenberg–Mac Lane spaces).
Verification
The metastable theorem identifies each listed group with A^i by evaluation on ι₃. The low-degree admissible basis gives A⁰={1}, A¹={Sq¹}, A²={Sq²}; the normalized universal class and naturality identify the three images.
The strict inequality excludes i=3, so the example does not extend the commissioned comparison range.
A Steenrod operation on the universal Thom class
Example
Assume AC, inherited from the cited bundle, cohomology, or operation suppliers. In stable mod-two Thom cohomology, Sq³(U)=w₃U. At rank 3, Sq³(u₃)=w₃(γ₃)u₃; at rank 2 the component is zero because w₃(γ₂)=0 and Sq³(u₂)=0 by instability.
Facts & Assumptions
Given: AC; the stable mod-two Thom cohomology module with its stable class and component classes ; the stable squares ; and the ranks and .
The stable-square lemma identifies every component of with and proves compatibility under the inverse-system maps (Stable Steenrod squares on universal Thom cohomology); the top-square formula and instability govern the degree-two class , and for rank reasons.
Verification
The stable-square supplier identifies every component of Sq^i(U) with w_i(γ_r)u_r and proves compatibility under the inverse-system maps. The rank bound makes w₃(γ₂)=0; instability kills Sq³ on the degree-2 class u₂.
At rank 3 the top-square formula agrees with the Thom identity.
The rational Hurewicz range for the four-sphere
Example
Assume AC. For S⁴, the rational Hurewicz map is an isomorphism in degrees 4, 5, and 6: π₄(S⁴)⊗Q≅H₄(S⁴;Q)≅Q, and both π_i(S⁴)⊗Q and H_i(S⁴;Q) vanish for i=5,6.
Facts & Assumptions
Given: AC; the standard based CW structure on with one -cell and one -cell; the cell-pushing lemma for low-dimensional disks; and the sphere homology computation with coefficients in .
The low-dimensional disk-pushing lemma deforms a based cube map of dimension into the 0-cell while fixing its boundary, so is 3-connected (A low-dimensional disk can be pushed off a higher cell).
The sphere homology computation with coefficient group gives the displayed rational homology groups (Homology of spheres), and the rational Hurewicz theorem applies with in the range , namely (Rational Hurewicz for highly connected CW complexes).
The rational sphere homotopy computation identifies in that range (Rational sphere homotopy below the first unstable degree), and AC is inherited from the rational Hurewicz theorem (The Axiom of Choice).
Verification
Give S⁴ its standard based CW structure with one 0-cell and one 4-cell. For each j=1,2,3, a based cubical representative f:Iʲ→S⁴ has boundary mapped to the 0-cell. Apply lem-a-low-dimensional-disk-can-be-pushed-off-a-higher-cell to the finite one-cell attachment (S⁴,*), with n=j<4. It deforms f into the 0-cell while fixing its boundary, so π₁(S⁴)=π₂(S⁴)=π₃(S⁴)=0. This writes out the one-cell connectivity argument using the published cell-pushing supplier; the stronger lem-high-relative-cells-do-not-change-lower-homotopy is also available in page 547's published prerequisite closure but is not needed as a direct dependency. cor-homology-of-spheres with coefficient group Q gives the displayed rational homology groups directly.
Now apply the rational Hurewicz theorem with c=4; its range is c≤i≤2c−2, namely 4≤i≤6. The rational sphere lemma computes the three homotopy groups. The degree-4 map is the first-nonzero-degree Hurewicz isomorphism; in degrees 5 and 6 both sides vanish.