Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01
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.

Tensor transition laws define a smooth vector bundle

Statement

For every smooth manifold M and integers r,s0, the tensor-coordinate change rules define a smooth vector bundle whose fibre over p is the space of type (r,s) tensors on TpM.

Facts & Assumptions

Given: A smooth manifold M with overlapping charts (U,x) and (V,y).

[F1]

The fibre of TsrM at p is the space of type (r,s) tensors on TpM (The type (r,s) tensor bundle).

[L1]

Tangent bases transform by the Jacobian, and cotangent bases transform by the inverse transpose Jacobian (Change-of-coordinate formula for tangent bases, Cotangent coordinate changes use the inverse transpose Jacobian).

[L2]

A smooth cocycle of fibrewise linear transition maps defines a smooth vector bundle (Construction of a vector bundle from a smooth cocycle).

Proof

technique · direct
1.1

On a chart domain U, the coordinate bases /xi and [F1, given, construct] dxi identify each fibre in [F1] with the fixed finite-dimensional vector space Mult(((Rm))r×(Rm)s,R) of type (r,s) tensors on Rm. This gives local trivializations TsrMUU×Mult(((Rm))r×(Rm)s,R).

F1givenconstruct
2.1

On an overlap, [L1] shows that each contravariant slot picks up one inverse [L1, step 1.1, algebra] Jacobian factor and each covariant slot picks up one Jacobian factor. Hence the tensor-coordinate change map is fibrewise linear, smooth in the base point, and satisfies the cocycle law because Jacobians and inverse Jacobians do.

L1step 1.1algebra
3.1

Therefore [L2] applies to these local transition maps and produces a smooth [F1, L2, step 2.1] vector bundle. By construction its fibre over p is the tensor space from [F1].

F1L2step 2.1
4.1

Thus the tensor transition laws define the smooth tensor bundle TsrM. [step 3.1]

step 3.1

Depends on

Used by

Cited to discharge well-definedness by The type (r,s) tensor bundle.

Dependency tree · two levels

16 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