The Kulkarni–Nomizu product of bilinear forms

The Kulkarni–Nomizu product of two bilinear forms h and k on a module M is the quadrilinear form

(h ⊙ k)(x, y, z, w) = h(x, w) k(y, z) + h(y, z) k(x, w) - h(x, z) k(y, w) - h(y, w) k(x, z).

It is the basic way to build curvature-type tensors out of symmetric bilinear forms: with the convention Rm(x, y, z, w) = ⟨R(x, y)z, w⟩, the curvature tensor of a space of constant sectional curvature κ is (κ / 2) (g ⊙ g), and the Weyl tensor of a Riemannian metric is the part of Rm left after removing the Kulkarni–Nomizu product of the Schouten tensor with g.

The product is bilinear and commutative, and is always antisymmetric in its first and in its last pair of arguments. For symmetric h and k it is moreover symmetric under interchanging the two pairs and satisfies the first Bianchi identity, so it has all the algebraic symmetries of a Riemann curvature tensor.

Main declarations

• LinearMap.BilinForm.kulkarniNomizu: the Kulkarni–Nomizu product, as a bilinear map.
• LinearMap.BilinForm.kulkarniNomizu_comm: the product is commutative.
• LinearMap.BilinForm.IsSymm.kulkarniNomizu_swap_pairs and LinearMap.BilinForm.IsSymm.kulkarniNomizu_cyclic_eq_zero: pair interchange and the first Bianchi identity for symmetric factors.

References

• A. L. Besse, Einstein Manifolds, Springer (1987), Section 1.G.
• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 7.

def LinearMap.BilinForm.kulkarniNomizu {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] : LinearMap.BilinForm R M →ₗ[R] LinearMap.BilinForm R M →ₗ[R] M →ₗ[R] M →ₗ[R] M →ₗ[R] M →ₗ[R] R

The Kulkarni–Nomizu product of two bilinear forms, bundled as a bilinear map: (h ⊙ k)(x, y, z, w) = h(x, w) k(y, z) + h(y, z) k(x, w) - h(x, z) k(y, w) - h(y, w) k(x, z).

@[simp]

theorem LinearMap.BilinForm.kulkarniNomizu_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (h k : LinearMap.BilinForm R M) (x y z w : M) : (((((kulkarniNomizu h) k) x) y) z) w = (h x) w * (k y) z + (h y) z * (k x) w - (h x) z * (k y) w - (h y) w * (k x) z

Evaluation of the Kulkarni–Nomizu product.

theorem LinearMap.BilinForm.kulkarniNomizu_comm {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (h k : LinearMap.BilinForm R M) : (kulkarniNomizu h) k = (kulkarniNomizu k) h

The Kulkarni–Nomizu product is commutative.

theorem LinearMap.BilinForm.kulkarniNomizu_antisymm_first {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (h k : LinearMap.BilinForm R M) (x y z w : M) : (((((kulkarniNomizu h) k) x) y) z) w = -(((((kulkarniNomizu h) k) y) x) z) w

The Kulkarni–Nomizu product is antisymmetric in its first pair of arguments.

theorem LinearMap.BilinForm.kulkarniNomizu_antisymm_last {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (h k : LinearMap.BilinForm R M) (x y z w : M) : (((((kulkarniNomizu h) k) x) y) z) w = -(((((kulkarniNomizu h) k) x) y) w) z

The Kulkarni–Nomizu product is antisymmetric in its last pair of arguments.

theorem LinearMap.BilinForm.IsSymm.kulkarniNomizu_swap_pairs {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {h k : LinearMap.BilinForm R M} (hh : h.IsSymm) (hk : k.IsSymm) (x y z w : M) : (((((kulkarniNomizu h) k) x) y) z) w = (((((kulkarniNomizu h) k) z) w) x) y

The Kulkarni–Nomizu product of symmetric bilinear forms is unchanged when its two pairs of arguments are interchanged.

theorem LinearMap.BilinForm.IsSymm.kulkarniNomizu_cyclic_eq_zero {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {h k : LinearMap.BilinForm R M} (hh : h.IsSymm) (hk : k.IsSymm) (x y z w : M) : (((((kulkarniNomizu h) k) x) y) z) w + (((((kulkarniNomizu h) k) y) z) x) w + (((((kulkarniNomizu h) k) z) x) y) w = 0

The first Bianchi identity for the Kulkarni–Nomizu product of symmetric bilinear forms: the cyclic sum over the first three arguments vanishes.