LemmaStatement: AI-adaptedProof: AI-generatedprecheck pass

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 component transformation law of a smooth tensor field

Statement

Let $(M, g, N)$ be a time-oriented smooth Lorentzian four-manifold (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model), let $r, s \geq 0$ , and let $T$ be a family assigning to each $p \in M$ a type $(r, s)$ tensor at $p$ (Tensor fields of type (r,s) on a Lorentzian four-manifold and their components). Let $(U, x)$ and $(V, y)$ be overlapping smooth charts, and write $T^{a_{1} \dots a_{r}}_{b_{1} \dots b_{s}}$ and $T^{' a_{1} \dots a_{r}}_{b_{1} \dots b_{s}}$ for the components of $T$ in the charts $x$ and $y$ . Then for every $q \in U \cap V$ ,

$T^{' a_{1} \dots a_{r}}_{b_{1} \dots b_{s}} (y (q)) = \sum_{c_{1}, \dots, c_{r}} \sum_{d_{1}, \dots, d_{s}} (\prod_{i = 1}^{r} \frac{\partial y^{a_{i}}}{\partial x^{c_{i}}} (x (q))) (\prod_{j = 1}^{s} \frac{\partial x^{d_{j}}}{\partial y^{b_{j}}} (y (q))) T^{c_{1} \dots c_{r}}_{d_{1} \dots d_{s}} (x (q)),$

where $\partial y^{a} / \partial x^{c}$ and $\partial x^{d} / \partial y^{b}$ are the entries of the total derivatives of $y \circ x^{- 1}$ and $x \circ y^{- 1}$ . Moreover $T$ is a smooth tensor field of type $(r, s)$ if and only if its components are $C^{\infty}$ in the charts of some one smooth atlas of $M$ ; in that case the components in every smooth chart are $C^{\infty}$ .

Facts & Assumptions

Given: A time-oriented smooth Lorentzian four-manifold $(M, g, N)$ , integers $r, s \geq 0$ , a family $T$ of type $(r, s)$ tensors, and overlapping smooth charts $(U, x)$ , $(V, y)$ .

[L1]

The components of $T$ in a chart are the evaluations $T^{a_{1} \dots a_{r}}_{b_{1} \dots b_{s}} (q) = T_{q} (d x^{a_{1}} ∣_{q}, \dots, \partial_{b_{1}} ∣_{q}, \dots)$ , and $T$ is a smooth tensor field of type $(r, s)$ when these are $C^{\infty}$ in the charts of the maximal smooth atlas (Tensor fields of type (r,s) on a Lorentzian four-manifold and their components).

[L2]

The coordinate derivations of one chart expand in those of another by $\partial_{x^{i}} ∣_{q} = \sum_{j} \frac{\partial (y^{j} \circ x^{- 1})}{\partial x^{i}} (x (q)) \partial_{y^{j}} ∣_{q}$ (Change-of-coordinate formula for tangent bases).

[L3]

The coordinate differentials of a chart form the dual basis of its coordinate derivations, and every covector expands in a dual basis (Coordinate differentials form the dual cotangent basis, Coordinate derivations form a basis of the tangent space).

[L4]

For a chart $(U, x)$ and $q \in U$ , the coordinate derivation acts on a smooth function by $\partial_{x^{i}} ∣_{q} f = D_{i} (f \circ x^{- 1}) (x (q))$ ; in particular $\partial_{x^{i}} ∣_{q} (y^{j}) = \frac{\partial y^{j}}{\partial x^{i}} (x (q))$ (Coordinate derivations are well-defined derivations).

[L5]

Smoothly compatible charts have smooth transition maps in both directions, and the entries of their total derivatives are smooth functions (Smoothly compatible charts and the smoothness of Euclidean transition maps, $C^{r}$ and smooth maps between smooth manifolds).

[L6]

Matrix inversion preserves $C^{k}$ regularity on the invertible matrices, so the entries $\frac{\partial x^{d}}{\partial y^{b}}$ of the inverse Jacobian are $C^{\infty}$ (Matrix inversion preserves $C^{k}$ regularity where the determinant is nonzero).

[L7]

Finite sums and products of $C^{\infty}$ Euclidean maps are $C^{\infty}$ , and composites of $C^{\infty}$ maps are $C^{\infty}$ ( $C^{k}$ Euclidean maps are closed under componentwise algebra and composition).

Proof

technique · direct

1.1L2L3L4given

Fix $q \in U \cap V$ and write $\partial_{x^{i}} : = \partial_{x^{i}} ∣_{q}$ , $\partial_{y^{j}} : = \partial_{y^{j}} ∣_{q}$ , $d x^{i} : = d x^{i} ∣_{q}$ , $d y^{j} : = d y^{j} ∣_{q}$ . By [L2] applied to the two charts, $\partial_{y^{b}} = \sum_{d} \frac{\partial x^{d}}{\partial y^{b}} (y (q)) \partial_{x^{d}}$ . By [L3] and [L4], $d y^{a}$ is the dual basis element of $\partial_{y^{a}}$ and its coefficients in the dual basis $(d x^{c})$ are $d y^{a} (\partial_{x^{c}}) = \partial_{x^{c}} (y^{a}) = \frac{\partial y^{a}}{\partial x^{c}} (x (q))$ ; hence $d y^{a} = \sum_{c} \frac{\partial y^{a}}{\partial x^{c}} (x (q)) d x^{c}$ .

2.1step 1.1L1algebra

Since $T_{q}$ is multilinear in its $r$ covector and $s$ vector arguments, substituting the expansions of step 1.1 into the definition of the $y$ -components gives the displayed transformation law: each contravariant slot contributes one factor $\frac{\partial y^{a_{i}}}{\partial x^{c_{i}}} (x (q))$ and each covariant slot one factor $\frac{\partial x^{d_{j}}}{\partial y^{b_{j}}} (y (q))$ , and the sums over the intermediate indices are finite.

3.1step 2.1L1algebra

In the special case $r = s = 0$ the double sum is empty and the law reduces to $T^{'} (y (q)) = T (x (q))$ ; in the case $r = 1, s = 0$ it reduces to the vector transformation law and in the case $r = 0, s = 1$ to the covector law of step 1.1.

3.2step 2.1L1L5L6L7given

Suppose $T$ has $C^{\infty}$ components in the charts of one smooth atlas $A$ . Let $(V, y)$ be any smooth chart and $q \in V$ ; choose a chart $(U, x)$ of $A$ with $q \in U$ (the charts of $A$ cover $M$ ). By step 2.1 the components of $T$ in $y$ equal the finite sum of step 2.1, whose factors are: the numbers computed from the components of $T$ in $x$ , which are $C^{\infty}$ functions of $x$ by hypothesis, evaluated along the smooth map $x$ ; and the Jacobian entries $\frac{\partial y^{a}}{\partial x^{c}} \circ x$ and $\frac{\partial x^{d}}{\partial y^{b}} \circ y$ , which are $C^{\infty}$ on the overlap by [L5] and [L6]. By [L7] the sum is $C^{\infty}$ on $y (U \cap V)$ . Since $q$ and $(V, y)$ were arbitrary, the components of $T$ are $C^{\infty}$ in every smooth chart, so $T$ is a smooth tensor field by [L1]. The converse direction is immediate from [L1], since the maximal atlas contains every smooth atlas.

4.1step 1.1step 2.1step 3.1step 3.2∎

Steps 1.1, 2.1 and 3.1 prove the transformation law and step 3.2 proves the smoothness criterion.

The component transformation law of a smooth tensor field

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources