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.

Contraction of a smooth tensor field is 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 1$ , and let $T$ be a smooth tensor field of type $(r, s)$ on $M$ (Tensor fields of type (r,s) on a Lorentzian four-manifold and their components). For each $p \in M$ let $(ctr T)_{p}$ be the contraction of $T_{p}$ over its first contravariant slot and its first covariant slot (The contraction of a mixed tensor). Then:

$ctr T$ is a smooth tensor field of type $(r - 1, s - 1)$ on $M$ , and its definition is independent of every basis.
In every smooth chart $(U, x)$ the components of $ctr T$ are

$(ctr T)^{a_{2} \dots a_{r}}_{b_{2} \dots b_{s}} = \sum_{i = 0}^{3} T^{i a_{2} \dots a_{r}}_{i b_{2} \dots b_{s}},$

and the field obtained by contracting any other pair consisting of one contravariant and one covariant slot has the analogous component formula after permuting the slots.
If $r = s = 1$ , then $tr T : = ctr T$ is a smooth function on $M$ and $tr T = \sum_{i = 0}^{3} T^{i}_{i}$ in every smooth chart.

Facts & Assumptions

Given: A time-oriented smooth Lorentzian four-manifold $(M, g, N)$ , integers $r, s \geq 1$ , and a smooth type $(r, s)$ tensor field $T$ on $M$ .

[L1]

Contraction of a type $(r, s)$ tensor $T_{p}$ over its first contravariant and first covariant slot is the type $(r - 1, s - 1)$ tensor given in a basis $(e_{i})$ with dual basis $(e^{i})$ by $(ctr T_{p}) (α_{2}, \dots, α_{r}, v_{2}, \dots, v_{s}) = \sum_{i} T_{p} (e^{i}, α_{2}, \dots, α_{r}, e_{i}, v_{2}, \dots, v_{s})$ (The contraction of a mixed tensor).

[L2]

The contraction formula has the same value for every basis and its dual basis (Contraction is independent of the basis formula).

[L3]

For a tensor field $T$ of type $(r, s)$ , the component functions in a chart are $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 smooth exactly when these are $C^{\infty}$ in every smooth chart (Tensor fields of type (r,s) on a Lorentzian four-manifold and their components).

[L4]

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

Proof

technique · direct

1.1L1L2given

For each $p \in M$ the assignment $(ctr T)_{p} : = ctr (T_{p})$ is a type $(r - 1, s - 1)$ tensor at $p$ by [L1], and it does not depend on any basis by [L2]; hence $ctr T$ is a well-defined family of type $(r - 1, s - 1)$ tensors on $M$ .

2.1step 1.1L1L3algebra

Let $(U, x)$ be a smooth chart and $q \in U$ . Applying [L1] with the coordinate basis $e_{i} = \partial_{i} ∣_{q}$ and its dual basis $e^{i} = d x^{i} ∣_{q}$ (which is the dual coordinate basis) and evaluating on the arguments $d x^{a_{2}} ∣_{q}, \dots, d x^{a_{r}} ∣_{q}, \partial_{b_{2}} ∣_{q}, \dots, \partial_{b_{s}} ∣_{q}$ gives $(ctr T)^{a_{2} \dots a_{r}}_{b_{2} \dots b_{s}} (q) = \sum_{i = 0}^{3} T_{q} (d x^{i} ∣_{q}, d x^{a_{2}} ∣_{q}, \dots, \partial_{i} ∣_{q}, \partial_{b_{2}} ∣_{q}, \dots) = \sum_{i = 0}^{3} T^{i a_{2} \dots a_{r}}_{i b_{2} \dots b_{s}} (q)$ , which is the displayed formula.

3.1step 2.1L3L4given

The right-hand side of step 2.1 is a finite sum of the component functions $T^{i a_{2} \dots a_{r}}_{i b_{2} \dots b_{s}}$ of the smooth field $T$ , which are $C^{\infty}$ on $U$ by [L3]; hence by [L4] the components of $ctr T$ are $C^{\infty}$ on $U$ . Since the chart was arbitrary, [L3] now shows that $ctr T$ is a smooth type $(r - 1, s - 1)$ field, proving claims 1 and 2 for the first slot pair.

3.2step 2.1L1L3algebra

For another pair of slots, permute the arguments of $T_{p}$ by the corresponding finite permutation of the $r + s$ slots; the permutation is a linear isomorphism of the space of multilinear maps, so the permuted family is again a smooth tensor field (its components are components of $T$ with permuted indices), and contraction of the chosen pair is the first-pair contraction of the permuted field; the component formula is the one of step 2.1 with the contraction index read in the chosen slots.

4.1step 1.1step 2.1step 3.1algebra∎

If $r = s = 1$ , then $ctr T$ is a type $(0, 0)$ tensor at each $p$ , that is, a real number depending on $p$ ; by steps 1.1-2.1 it is a smooth function and its value in any chart is $\sum_{i} T^{i}_{i}$ by step 2.1. This proves claim 3.

Contraction of a smooth tensor field is a smooth tensor field

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources