ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Parallelizable tori have trivial stable normal class

Example

Assume AC. For $n \geq 1$ the torus $T^{n} = R^{n} / Z^{n}$ has trivial tangent bundle: left translations trivialize it, and the images of a basis of $T_{e} T^{n}$ under the left-invariant framing form a global frame (Left-invariant vector fields evaluate isomorphically at the identity, Local and global frames of a vector bundle, A vector bundle is trivial if and only if it has a global frame; for $n = 2$ see the two-dimensional torus The two-dimensional torus $T^{2} = (R / Z)^{2}$ ). Hence $\overset{ˉ}{w} (T^{n}) = 1$ and $\overset{ˉ}{p} (T^{n}) = 1$ (Parallelizable manifolds have no stable characteristic-class obstruction to Euclidean immersion): no Stiefel-Whitney or Pontryagin class test of this page obstructs an immersion of a torus into Euclidean space, and indeed $T^{n}$ immerses in $R^{n + 1}$ and hence in every $R^{n + k}$ with $k \geq 1$ . The example says nothing about embeddability: it exhibits a Euclidean formal immersion with trivial normal class, not an embedding theorem.

Facts & Assumptions

Given: An integer $n \geq 1$ , the torus $T^{n} = R^{n} / Z^{n}$ as the product of $n$ copies of the circle group $R / Z$ (a compact connected abelian Lie group), and AC.

[F1]

The product of $n$ copies of the circle group is a compact connected abelian Lie group of dimension $n$ , hence a torus in the sense of the Lie-group definition; for $n = 2$ this is the two-dimensional torus $T^{2} = (R / Z)^{2}$ (Tori and maximal tori, The two-dimensional torus $T^{2} = (R / Z)^{2}$ ).

[F2]

Left-invariant vector fields on a Lie group evaluate isomorphically at the identity; equivalently the map carrying a vector $v \in T_{e} G$ to the left-invariant field with that value is an isomorphism onto the space of left-invariant fields (Left-invariant vector fields evaluate isomorphically at the identity).

[F3]

A global frame of a smooth rank- $r$ bundle trivializes it: a bundle is trivial if and only if it has a global frame, and the frame determines the trivialization (Local and global frames of a vector bundle, A vector bundle is trivial if and only if it has a global frame).

[F4]

For a closed smooth $M$ with trivial tangent bundle, the trivial bundle is a rank- $k$ stable normal inverse for every $k \geq 1$ , $M$ immerses in $R^{m + k}$ , and the normal classes vanish: $\overset{ˉ}{w} (M) = 1$ and $\overset{ˉ}{p} (M) = 1$ (Parallelizable manifolds have no stable characteristic-class obstruction to Euclidean immersion). The relevant countable choice is implied by AC (AC implies DC implies countable choice, The Axiom of Countable Choice ( ${A C}_{ω}$ ), The Axiom of Choice).

[F5]

A trivial positive-rank bundle has a nowhere-zero constant section, so its Euler class vanishes (A nowhere-zero section forces the Euler class to vanish).

Verification

technique · direct

1.1F1F2

By [F1] the torus $T^{n}$ is a compact connected abelian Lie group of dimension $n$ . Choose a basis $v_{1}, \dots, v_{n}$ of the tangent space $T_{e} T^{n}$ at the identity; by [F2] the corresponding left-invariant vector fields $X_{1}, \dots, X_{n}$ are smooth global sections of $T T^{n}$ whose values at $e$ form a basis, and left invariance carries this basis to a basis of every tangent space $T_{g} T^{n}$ (translation by $g$ is a diffeomorphism and identifies $T_{e} T^{n}$ with $T_{g} T^{n}$ ). Hence $(X_{1}, \dots, X_{n})$ is a global frame of $T T^{n}$ , smooth by [F2].

2.1F2F3step 1.1

By [F3] the existence of the global frame of step 1.1 makes $T T^{n}$ trivial: $T T^{n} ≅ ε^{n}$ over $T^{n}$ , with the trivialization determined by the frame.

3.1F4step 2.1

By [F4] applied to the closed manifold $T^{n}$ with trivial tangent bundle, the trivial bundle is a rank- $k$ stable normal inverse of $T^{n}$ for every $k \geq 1$ ; consequently $T^{n}$ immerses in $R^{n + k}$ for every $k \geq 1$ , in particular in $R^{n + 1}$ , and its normal classes are trivial: $\overset{ˉ}{w} (T^{n}) = w (T T^{n})^{- 1} = 1^{- 1} = 1, \overset{ˉ}{p} (T^{n}) = p (T T^{n})^{- 1} = 1^{- 1} = 1.$

4.1F4F5step 2.1step 3.1∎

Therefore no Stiefel-Whitney or Pontryagin class test of this page obstructs a Euclidean immersion of $T^{n}$ : every class ${\overset{ˉ}{w}}_{i} (T^{n})$ , ${\overset{ˉ}{p}}_{i} (T^{n})$ with $i \geq 1$ vanishes, and the Euler class of the trivial normal bundle vanishes as well. The example exhibits a Euclidean formal immersion with trivial normal class and says nothing about embeddability of tori; in particular it does not assert that $T^{n}$ embeds in $R^{n + 1}$ or in any other specific Euclidean space, nor does it identify a minimal immersion dimension below $n + 1$ . The only choice used is the AC assumed by the parallelizable-manifold proposition and its countable-choice input.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

39 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

John W. Milnor and James D. Stasheff, Characteristic Classes (Annals of Mathematics Studies 74, Princeton University Press; complete text) (standard reference, not scraped)
Ralph L. Cohen, Immersions of Manifolds and Homotopy Theory (lecture notes, 30 June 2022; complete 46-page text) (standard reference, not scraped)
Arkadiy Skopenkov, Embedding and Knotting of Manifolds in Euclidean Spaces (arXiv:math/0604045) (standard reference, not scraped)