Polarization of curvature-type tensors

Let T(x, y, z, w) be a quadrilinear form on a module which is antisymmetric in its first pair and in its last pair of arguments and satisfies the first Bianchi identity T(x, y, z, w) + T(y, z, x, w) + T(z, x, y, w) = 0. These are the algebraic symmetries of a Riemann curvature tensor Rm(x, y, z, w) = ⟨R(x, y)z, w⟩. The values T(x, y, y, x), which for a Riemann curvature tensor are the numerators of the sectional curvatures, determine 6 T, and hence T itself whenever multiplication by 6 is injective on the scalars. Explicitly, writing k(x, y) = T(x, y, y, x),

6 T(x, y, z, w) = k(x + w, y + z) - k(x + z, y + w) - k(x, y + z) - k(w, y + z) + k(x, y + w) + k(z, y + w) - k(x + w, y) + k(x + z, y) - k(x + w, z) + k(x + z, w) + k(w, y) - k(z, y) + k(x, z) - k(x, w).

This identity holds over every commutative ring. When multiplication by 6 is injective on the scalars, it can be cancelled, so two such tensors with the same values T(x, y, y, x) are equal. Over a domain in which 6 ≠ 0 it is enough to compare these values on linearly independent pairs, that is, on the pairs spanning a plane, since both sides vanish on dependent pairs. This is how the sectional curvatures of a Riemannian manifold determine its curvature tensor.

Main declarations

• LinearMap.six_mul_apply_eq_of_cyclic_eq_zero: the polarization identity, expressing 6 T through the values T(x, y, y, x).
• LinearMap.eq_of_cyclic_eq_zero: two curvature-type tensors with the same values T(x, y, y, x) are equal when multiplication by 6 is injective.
• LinearMap.apply_apply_apply_apply_eq_zero_of_not_linearIndependent: T(x, y, y, x) = 0 on linearly dependent pairs.
• LinearMap.eq_of_cyclic_eq_zero_of_linearIndependent: two curvature-type tensors agreeing on T(x, y, y, x) for linearly independent pairs are equal.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 8, Proposition 8.31.

theorem LinearMap.six_mul_apply_eq_of_cyclic_eq_zero {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {T : M →ₗ[R] M →ₗ[R] M →ₗ[R] M →ₗ[R] R} (h₁ : ∀ (x y z w : M), (((T x) y) z) w = -(((T y) x) z) w) (h₂ : ∀ (x y z w : M), (((T x) y) z) w = -(((T x) y) w) z) (h₃ : ∀ (x y z w : M), (((T x) y) z) w + (((T y) z) x) w + (((T z) x) y) w = 0) (x y z w : M) : 6 * (((T x) y) z) w = (((T (x + w)) (y + z)) (y + z)) (x + w) - (((T (x + z)) (y + w)) (y + w)) (x + z) - (((T x) (y + z)) (y + z)) x - (((T w) (y + z)) (y + z)) w + (((T x) (y + w)) (y + w)) x + (((T z) (y + w)) (y + w)) z - (((T (x + w)) y) y) (x + w) + (((T (x + z)) y) y) (x + z) - (((T (x + w)) z) z) (x + w) + (((T (x + z)) w) w) (x + z) + (((T w) y) y) w - (((T z) y) y) z + (((T x) z) z) x - (((T x) w) w) x

The polarization identity for curvature-type tensors: for a quadrilinear form T antisymmetric in its first and in its last pair of arguments and satisfying the first Bianchi identity, 6 T(x, y, z, w) is an explicit combination of values T(a, b, b, a). This recovers T itself only when multiplication by 6 is injective, see LinearMap.eq_of_cyclic_eq_zero.

theorem LinearMap.eq_of_cyclic_eq_zero {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (h6 : IsLeftRegular 6) {T₁ T₂ : M →ₗ[R] M →ₗ[R] M →ₗ[R] M →ₗ[R] R} (h₁ : ∀ (x y z w : M), (((T₁ x) y) z) w = -(((T₁ y) x) z) w) (h₂ : ∀ (x y z w : M), (((T₁ x) y) z) w = -(((T₁ x) y) w) z) (h₃ : ∀ (x y z w : M), (((T₁ x) y) z) w + (((T₁ y) z) x) w + (((T₁ z) x) y) w = 0) (h₁' : ∀ (x y z w : M), (((T₂ x) y) z) w = -(((T₂ y) x) z) w) (h₂' : ∀ (x y z w : M), (((T₂ x) y) z) w = -(((T₂ x) y) w) z) (h₃' : ∀ (x y z w : M), (((T₂ x) y) z) w + (((T₂ y) z) x) w + (((T₂ z) x) y) w = 0) (hT : ∀ (x y : M), (((T₁ x) y) y) x = (((T₂ x) y) y) x) : T₁ = T₂

Two quadrilinear forms antisymmetric in their first and in their last pair of arguments and satisfying the first Bianchi identity are equal as soon as T₁(x, y, y, x) = T₂(x, y, y, x) for all x, y, provided multiplication by 6 is injective on the scalars.

theorem LinearMap.apply_apply_apply_apply_eq_zero_of_not_linearIndependent {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {T : M →ₗ[R] M →ₗ[R] M →ₗ[R] M →ₗ[R] R} [NoZeroDivisors R] (h2 : 2 ≠ 0) (h₁ : ∀ (x y z w : M), (((T x) y) z) w = -(((T y) x) z) w) {x y : M} (hxy : ¬LinearIndependent R ![x, y]) : (((T x) y) y) x = 0

A quadrilinear form antisymmetric in its first pair of arguments has T(x, y, y, x) = 0 whenever x and y are linearly dependent, provided the scalars have no zero divisors and 2 ≠ 0.

theorem LinearMap.eq_of_cyclic_eq_zero_of_linearIndependent {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroDivisors R] (h6 : 6 ≠ 0) {T₁ T₂ : M →ₗ[R] M →ₗ[R] M →ₗ[R] M →ₗ[R] R} (h₁ : ∀ (x y z w : M), (((T₁ x) y) z) w = -(((T₁ y) x) z) w) (h₂ : ∀ (x y z w : M), (((T₁ x) y) z) w = -(((T₁ x) y) w) z) (h₃ : ∀ (x y z w : M), (((T₁ x) y) z) w + (((T₁ y) z) x) w + (((T₁ z) x) y) w = 0) (h₁' : ∀ (x y z w : M), (((T₂ x) y) z) w = -(((T₂ y) x) z) w) (h₂' : ∀ (x y z w : M), (((T₂ x) y) z) w = -(((T₂ x) y) w) z) (h₃' : ∀ (x y z w : M), (((T₂ x) y) z) w + (((T₂ y) z) x) w + (((T₂ z) x) y) w = 0) (hT : ∀ (x y : M), LinearIndependent R ![x, y] → (((T₁ x) y) y) x = (((T₂ x) y) y) x) : T₁ = T₂

Two quadrilinear forms antisymmetric in their first and in their last pair of arguments and satisfying the first Bianchi identity are equal as soon as T₁(x, y, y, x) = T₂(x, y, y, x) for every linearly independent pair x, y, provided the scalars have no zero divisors and 6 ≠ 0. Over a field these pairs are the bases of the two-dimensional subspaces.