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.
The frame bundle of a smooth manifold
Definition
Assume (The Axiom of Countable Choice ()), inherited from the smooth tangent-bundle theorem. Let be a smooth -manifold with . Its tangent bundle carries the canonical smooth -manifold structure of Assuming countable choice, the tangent bundle has a canonical smooth 2n-manifold structure (The tangent bundle as a disjoint union, Smooth manifolds and their smooth charts). The frame bundle of is the frame bundle of the tangent bundle in the sense of Frame bundles and associated vector bundles, the total space of the principal -bundle of Invertible matrices and the general linear group associated with . It carries the smooth structure induced by the linear bundle charts of (locally , the second factor an open subset of the matrix space), the smooth projection , , and the free smooth right action of , whose orbits are exactly the fibres ; each fibre is therefore a -torsor. A framing of the point is an element of the fibre , equivalently a linear isomorphism .
The fibre has exactly two path components, the two orientation classes of bases of (Orientation of a finite-dimensional real vector space). Indeed the determinant is a surjective continuous group homomorphism (Determinant is a group homomorphism , and ), so its sign separates into the nonempty open sets of positive and negative determinant, and the torsor action identifies these with ; left multiplication by identifies the negative-determinant matrices with the positive-determinant matrices, which are path-connected by Positively oriented bases of an oriented vector space are path-connected, so these are exactly the two path components. When is oriented, a chart of whose coordinate frame is positive at a point gives the identification of with the positive and negative bases used here (Oriented smooth manifolds and oriented charts).
A framing of a closed -dimensional submanifold is a framing of in in the sense of the normal-quotient convention: since , the normal bundle is over the discrete set (Normal and conormal bundles of an embedded submanifold), so a framing of is exactly a family of linear isomorphisms , that is, a family of framings of the individual points . If is compact it is finite: its singleton subsets form an open cover and admit a finite subcover.
Finally, if is oriented, the sign of a framing is when the isomorphism carries the standard orientation of (the one for which the standard basis is positive) to the given orientation of , and otherwise. Two framings of the same point have the same sign exactly when they lie in the same component of : the sign is constant on a component because it is a continuous function with values in , and the two components are the positive and the negative bases for the given orientation. No orientation of is needed for the definition of or of a framing, and this definition selects nothing beyond the supplied chart data of .
Depends on
The tangent bundle as a disjoint union
Assuming countable choice, the tangent bundle has a canonical smooth 2n-manifold structure
Frame bundles and associated vector bundles
Invertible matrices and the general linear group
Orientation of a finite-dimensional real vector space
Oriented smooth manifolds and oriented charts
Smooth manifolds and their smooth charts
Normal and conormal bundles of an embedded submanifold
Determinant is a group homomorphism , and
Positively oriented bases of an oriented vector space are path-connected
The Axiom of Countable Choice ()