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.
General linear frame spaces have the Stiefel cohomology gap
Statement
Assume the Axiom of Choice (The Axiom of Choice). Fix integers , and for , let be a field, and put where is the open set of injective, equivalently full-rank, complex matrices. Then:
- each is homotopy equivalent to the Stiefel space of orthonormal frames (Stiefel spaces, Grassmannians, and tautological bundles);
- each is a compact path-connected smooth manifold and is homeomorphic to a finite CW complex, and the map forgetting the last column is a numerable locally trivial fiber bundle with fiber , hence a Hurewicz and a Serre fibration;
- and for .
No claim is made about the cohomology of above degree , and no GL-equivariance of the retractions or trivializations below is asserted.
Facts & Assumptions
Given: Integers with , ; the field ; the spaces , and with the subspace and product topologies; the Axiom of Choice The Axiom of Choice.
Stiefel spaces and Gram-Schmidt (Stiefel spaces, Grassmannians, and tautological bundles, Gram–Schmidt turns every finite independent list into an orthonormal list with the same successive spans): is the space of ordered orthonormal -frames in with the subspace topology of ; Gram-Schmidt sends a linearly independent list to the orthonormal list spanning the same flags, by the displayed recursion.
Submersions and regular level sets (Immersions, submersions, and constant-rank maps, A regular level set is locally a graph of dimension , Smooth manifolds and their smooth charts): a regular level set of a map between open subsets of Euclidean spaces is locally a graph over the kernel of the differential, hence a smooth submanifold of the ambient Euclidean space of the corresponding dimension.
Compactness and triangulation (Assuming and , compactness, sequential compactness, countable compactness, limit point compactness, completeness and total boundedness, pseudocompactness, closedness and boundedness, and the extreme-value property are equivalent for nonempty subsets of with , Finite smooth triangulation of compact corners, relative to admissible boundary data, The geometric realization of an abstract simplicial complex, CW complex with closure finiteness and weak topology): a closed and bounded subset of a Euclidean space is compact; a compact smooth manifold, viewed as a manifold with corners with no corners, has a finite smooth triangulation, i.e. is homeomorphic to the realization of a finite abstract simplicial complex, and a finite simplicial complex is a finite CW complex whose cells are its open simplices.
Bundles, paracompactness and fibrations (Locally trivial fiber bundle, Every compact space is paracompact, Under choice and dependent choice, every open cover of a compact Hausdorff space admits a finite subordinate partition of unity, Numerable fiber bundles are hurewicz fibrations): a compact Hausdorff space is paracompact, every open cover of a compact Hausdorff space admits a finite subordinate partition of unity, so a locally trivial bundle over a compact Hausdorff base is numerable, and every numerable fiber bundle with its ordinary product charts is a Hurewicz fibration, hence a Serre fibration; the pullback of a locally trivial bundle along a continuous map is a locally trivial bundle with the same fiber.
The cohomological Serre spectral sequence (Cohomological Serre spectral sequence): for a Serre fibration over a path-connected CW complex and a commutative unital ring , there is a natural first-quadrant spectral sequence , with differentials , strongly converging to ; is the constant system when the fibers are nonempty and connected.
Cohomology of spheres (Homology of spheres, The universal coefficient theorem for cohomology over a PID): reduced homology of is in degree and zero otherwise; over a field the universal coefficient sequence gives , and for . Spheres of dimension at least one are path-connected (For , the sphere is path-connected and connected, Paths, path-connected spaces and path components).
Constant-sheaf comparison (Locally contractible metric spaces have singular constant sheaf cohomology): on a metric space with a contractible-open neighbourhood basis, the cohomology of the constant -sheaf agrees naturally with singular cohomology. Euclidean open subsets and smooth submanifolds have this property by their ball charts.
A locally trivial bundle with nonempty path-connected fibre over a path-connected base has path-connected total space. Indeed, subdivide a base path into finitely many intervals lying in bundle charts, lift each interval using its product chart, and join the final lifted point to the desired point within the fibre. This follows directly from the product charts and path concatenation (Paths, path-connected spaces and path components, Locally trivial fiber bundle).
AC supplies DC and countable choice by AC implies DC implies countable choice, meeting the explicit choice hypotheses in [F3] and [F4]. AC is used through the partition-of-unity, triangulation and Serre-spectral-sequence and constant-sheaf comparison suppliers of [F3]-[F7]; the Gram-Schmidt, level-set and degree bookkeeping arguments are choice-free (The Axiom of Choice).
Proof
The frame retraction. Fix and let have columns , a linearly independent list. Applying the Gram-Schmidt recursion of [F1] to gives an orthonormal list with for every , so the upper triangular matrix with for , and for satisfies with . The Gram-Schmidt formulas are continuous rational expressions with positive denominators on the full-rank locus, so is continuous. Writing with the diagonal part and unit upper triangular, the family is continuous, has invertible upper triangular second factor with positive diagonal for every , and connects to inside ; at it is , so is a deformation retraction onto . This proves claim 1 and shows that is homotopy equivalent to .
Compact smooth frame manifolds. Let from the open full-rank locus of to the real vector space . Its differential is ; for Hermitian , taking gives , hence differential . Thus is a regular value and is a smooth submanifold by [F2]. It is closed in the ambient Euclidean space and bounded, since each frame column has norm one, so it is compact by [F3]. The subspace is Hausdorff and second countable, as required by the triangulation supplier. For it is a point.
The forgetting bundle. Fix and an orthonormal basis of its orthogonal complement. For a nearby frame , put . The vectors remain linearly independent near , since their Gram determinant is continuous and equals one at . Gram-Schmidt gives a continuously varying orthonormal basis of the complement of . The map for trivializes the forgetting map; its continuous inverse takes the inner products with . This also covers over the point . By step 1.2 the base is compact Hausdorff, so [F4] supplies a finite subordinate partition of unity and makes the bundle numerable, hence Hurewicz and Serre.
Finite CW model and path-connectedness. By the triangulation theorem of [F3] applied to the compact smooth manifold , there is a finite simplicial complex and a homeomorphism . A finite simplicial complex is a finite CW complex: its cells are the open simplices, the characteristic maps are the inclusions of the closed simplices, closure finiteness holds because there are finitely many simplices, and the weak topology agrees with the topology of the realization because the realization is the finite union of its closed simplices. Hence is homeomorphic to a finite CW complex, as claimed in claim 2. For path-connectedness, induct on . The space is a point. For the map is the locally trivial bundle of step 2.1 with fiber the nonempty path-connected sphere by [F6], and the base is path-connected by the induction hypothesis; the local connectedness argument of [F8] then makes path-connected. This completes claim 2.
The gap for one factor. Induct on , starting with a point. For put . The forgetting bundle of step 2.1 has fibre and base homeomorphic to a path-connected finite CW complex by step 3.1. The induction hypothesis gives vanishing of the base cohomology in degrees through . In the Serre spectral sequence [F5], [F6] makes all fibre rows in degrees zero; the degree-zero coefficient system is constant , since the fibre is connected. Consequently all terms of total degree are zero, while . No differential can enter or leave it in this first-quadrant sequence. Strong convergence therefore gives and for , completing the induction. No constancy of the top-degree fibre coefficient system is needed.
The product. By step 1.1 it suffices to compute the cohomology of , and we induct on . For this is step 4.1. For let and consider the projection , a trivial bundle with fiber , hence numerable and a Serre fibration by [F4]. By step 3.1 each factor and, inductively, is homeomorphic to a finite CW complex, and a finite product of finite CW complexes is again a finite CW complex: identify with by radial rescaling between their unit balls; the product characteristic maps into the product space then give cells and a finite cell decomposition, closure finiteness holds because there are finitely many cells, and the weak topology of the product cell structure agrees with the product topology for finite compact Hausdorff complexes, where the compactly generated product topology coincides with the ordinary one. So [F5] applies to the projection with constant coefficient system in fiber degree . If and for by induction, and if , for by step 4.1, then in total degree every nonzero with has , for would need fiber cohomology in degree , which vanishes; the differential bookkeeping of step 4.1 then gives , which is for and for . This proves claim 3, and for , by the homotopy equivalence of step 1.1.
The cohomology convention. The full-rank spaces are Euclidean open subsets and the Stiefel spaces and their products are smooth metric manifolds with contractible-open chart bases. Thus [F7] identifies their constant-sheaf cohomology with the singular cohomology computed in steps 4.1 and 5.1; naturality carries the frame deformation retraction of step 1.1 to these comparisons. In particular the same gap holds for the constant-sheaf fibre cohomology used by the later derived pullback lemmas.
Conclusion. Steps 1.1 and 5.1 give claims 1 and 3; steps 1.2, 2.1 and 3.1 give claim 2. AC is consumed only through the named compactness, triangulation, partition-of-unity, spectral-sequence and constant-sheaf comparison suppliers [F3]-[F7], as recorded in [A1].
Remarks
-
The statement is the cohomological input consumed by the equivariant Stiefel approximation lemma of this page; it asserts the gap for and nothing above , where the characteristic classes of the bundle live.
-
The argument is a local finite-cell computation: the sphere bundle is a numerable bundle over a finite CW model, so the Serre spectral sequence has finite pages and the low-degree bookkeeping uses only the base degree with fiber degree zero.
Depends on
- AC implies DC implies countable choice
- Locally contractible metric spaces have singular constant sheaf cohomology
- Under choice and dependent choice, every open cover of a compact Hausdorff space admits a finite subordinate partition of unity
- Assuming $\mathrm{AC}_\omega$ and $\mathrm{DC}$, compactness, sequential compactness, countable compactness, limit point compactness, completeness and total boundedness, pseudocompactness, closedness and boundedness, and the extreme-value property are equivalent for nonempty subsets of $\mathbb{R}^n$ with $n\ge1$
- For $n\ge2$, the sphere $S^{n-1}$ is path-connected and connected
- Homology of spheres
- A regular level set is locally a $C^k$ graph of dimension $m-n$
- The Axiom of Choice
- Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets
- CW complex with closure finiteness and weak topology
- The geometric realization of an abstract simplicial complex
- Immersions, submersions, and constant-rank maps
- Locally trivial fiber bundle
- Paths, path-connected spaces and path components
- Smooth manifolds and their smooth charts
- Stiefel spaces, Grassmannians, and tautological bundles
- Every compact space is paracompact
- Cohomological Serre spectral sequence
- Finite smooth triangulation of compact corners, relative to admissible boundary data
- Gram–Schmidt turns every finite independent list into an orthonormal list with the same successive spans
- Numerable fiber bundles are hurewicz fibrations
- The universal coefficient theorem for cohomology over a PID
Used by
Dependency tree · two levels
135 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
- A. Hatcher, Algebraic Topology (Cambridge University Press, 2002); author-hosted complete PDF, cited sections read in the extracted text (standard reference, not scraped)
- Joseph Bernstein and Valery Lunts, Equivariant Sheaves and Functors, Part I (Derived category and functors) (standard reference, not scraped)