Physlib.Relativity.Tensors.RealTensor.Representation.Contraction

Imports

/-
Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Relativity.Tensors.RealTensor.Vector.Representation
public import Physlib.Relativity.Tensors.RealTensor.CoVector.Representation
public import Mathlib.RepresentationTheory.Intertwining

Contraction of Real Lorentz Vectors and Covectors

We define the intertwining maps which define the contraction of a contravariant Lorentz vector with a covariant Lorentz vector, and vice versa.

Note: This file will eventually replace ./Pre/Contraction.lean when we move realLorentzTensor over to Vector and CoVector.

@[expose] public sectionattribute [-simp] Fintype.sum_sum_type

A. The definitions

TODO "In a similar way to `Vector.contract` and `CoVector.contract`,
  we want to define metrics and units as intertwining maps of representations.
  This should copy (and eventually replace) the definitions e.g. `./Units/Pre.lean`."

The intertwining map defining the contraction of a contravariant Lorentz vector with a covariant Lorentz vector.

def Vector.contract : (Vector.rep.tprod CoVector.rep).IntertwiningMap
    (Representation.trivial ℝ (LorentzGroup d) ℝ) where
  toLinearMap := byd:ℕ⊢ Vector d ⊗[ℝ] CoVector d →ₗ[ℝ] ℝ
    refine TensorProduct.lift (LinearMap.mk₂ ℝ (fun φ ψ => ∑ i, φ i * ψ i) ?_ ?_ ?_ ?_)refine_1d:ℕ⊢ ∀ (m₁ m₂ : Vector d) (n : CoVector d), ∑ i, (m₁ + m₂) i * n i = ∑ i, m₁ i * n i + ∑ i, m₂ i * n irefine_2d:ℕ⊢ ∀ (c : ℝ) (m : Vector d) (n : CoVector d), ∑ i, (c • m) i * n i = c • ∑ i, m i * n irefine_3d:ℕ⊢ ∀ (m : Vector d) (n₁ n₂ : CoVector d), ∑ i, m i * (n₁ + n₂) i = ∑ i, m i * n₁ i + ∑ i, m i * n₂ irefine_4d:ℕ⊢ ∀ (c : ℝ) (m : Vector d) (n : CoVector d), ∑ i, m i * (c • n) i = c • ∑ i, m i * n i
    ·refine_1d:ℕ⊢ ∀ (m₁ m₂ : Vector d) (n : CoVector d), ∑ i, (m₁ + m₂) i * n i = ∑ i, m₁ i * n i + ∑ i, m₂ i * n i simp [add_mul, Finset.sum_add_distrib]All goals completed! 🐙
    ·refine_2d:ℕ⊢ ∀ (c : ℝ) (m : Vector d) (n : CoVector d), ∑ i, (c • m) i * n i = c • ∑ i, m i * n i simp [Finset.mul_sum, mul_assoc]All goals completed! 🐙
    ·refine_3d:ℕ⊢ ∀ (m : Vector d) (n₁ n₂ : CoVector d), ∑ i, m i * (n₁ + n₂) i = ∑ i, m i * n₁ i + ∑ i, m i * n₂ i simp [mul_add, Finset.sum_add_distrib]All goals completed! 🐙
    ·refine_4d:ℕ⊢ ∀ (c : ℝ) (m : Vector d) (n : CoVector d), ∑ i, m i * (c • n) i = c • ∑ i, m i * n i introsrefine_4d:ℕc✝:ℝm✝:Vector dn✝:CoVector d⊢ ∑ i, m✝ i * (c✝ • n✝) i = c✝ • ∑ i, m✝ i * n✝ i
      simp_rw [refine_4d:ℕc✝:ℝm✝:Vector dn✝:CoVector d⊢ ∑ i, m✝ i * (c✝ • n✝) i = c✝ • ∑ i, m✝ i * n✝ iCoVector.apply_smul,refine_4d:ℕc✝:ℝm✝:Vector dn✝:CoVector d⊢ ∑ x, m✝ x * (c✝ * n✝ x) = c✝ • ∑ i, m✝ i * n✝ i smul_eq_mul,refine_4d:ℕc✝:ℝm✝:Vector dn✝:CoVector d⊢ ∑ x, m✝ x * (c✝ * n✝ x) = c✝ * ∑ i, m✝ i * n✝ i Finset.mul_sumrefine_4d:ℕc✝:ℝm✝:Vector dn✝:CoVector d⊢ ∑ x, m✝ x * (c✝ * n✝ x) = ∑ i, c✝ * (m✝ i * n✝ i)]
      exact Finset.sum_congr rfl (fun _ _ ↦ byd:ℕc✝:ℝm✝:Vector dn✝:CoVector dx✝¹:Fin 1 ⊕ Fin dx✝:x✝¹ ∈ Finset.univ⊢ m✝ x✝¹ * (c✝ * n✝ x✝¹) = c✝ * (m✝ x✝¹ * n✝ x✝¹) ringAll goals completed! 🐙)
  isIntertwining' Λ := byd:ℕΛ:↑(LorentzGroup d)⊢ TensorProduct.lift (LinearMap.mk₂ ℝ (fun φ ψ => ∑ i, φ i * ψ i) ⋯ ⋯ ⋯ ⋯) ∘ₗ (rep.tprod CoVector.rep) Λ =
  (Representation.trivial ℝ ↑(LorentzGroup d) ℝ) Λ ∘ₗ
    TensorProduct.lift (LinearMap.mk₂ ℝ (fun φ ψ => ∑ i, φ i * ψ i) ⋯ ⋯ ⋯ ⋯)
    ext φ ψd:ℕΛ:↑(LorentzGroup d)φ:Vector dψ:CoVector d⊢ ((AlgebraTensorModule.curry
        (TensorProduct.lift (LinearMap.mk₂ ℝ (fun φ ψ => ∑ i, φ i * ψ i) ⋯ ⋯ ⋯ ⋯) ∘ₗ (rep.tprod CoVector.rep) Λ))
      φ)
    ψ =
  ((AlgebraTensorModule.curry
        ((Representation.trivial ℝ ↑(LorentzGroup d) ℝ) Λ ∘ₗ
          TensorProduct.lift (LinearMap.mk₂ ℝ (fun φ ψ => ∑ i, φ i * ψ i) ⋯ ⋯ ⋯ ⋯)))
      φ)
    ψ
    trans (Λ.1 *ᵥ φ) ⬝ᵥ ((LorentzGroup.transpose Λ⁻¹).1 *ᵥ ψ)d:ℕΛ:↑(LorentzGroup d)φ:Vector dψ:CoVector d⊢ ((AlgebraTensorModule.curry
        (TensorProduct.lift (LinearMap.mk₂ ℝ (fun φ ψ => ∑ i, φ i * ψ i) ⋯ ⋯ ⋯ ⋯) ∘ₗ (rep.tprod CoVector.rep) Λ))
      φ)
    ψ =
  ↑Λ *ᵥ φ ⬝ᵥ ↑(LorentzGroup.transpose Λ⁻¹) *ᵥ ψd:ℕΛ:↑(LorentzGroup d)φ:Vector dψ:CoVector d⊢ ↑Λ *ᵥ φ ⬝ᵥ ↑(LorentzGroup.transpose Λ⁻¹) *ᵥ ψ =
  ((AlgebraTensorModule.curry
        ((Representation.trivial ℝ ↑(LorentzGroup d) ℝ) Λ ∘ₗ
          TensorProduct.lift (LinearMap.mk₂ ℝ (fun φ ψ => ∑ i, φ i * ψ i) ⋯ ⋯ ⋯ ⋯)))
      φ)
    ψ
    ·d:ℕΛ:↑(LorentzGroup d)φ:Vector dψ:CoVector d⊢ ((AlgebraTensorModule.curry
        (TensorProduct.lift (LinearMap.mk₂ ℝ (fun φ ψ => ∑ i, φ i * ψ i) ⋯ ⋯ ⋯ ⋯) ∘ₗ (rep.tprod CoVector.rep) Λ))
      φ)
    ψ =
  ↑Λ *ᵥ φ ⬝ᵥ ↑(LorentzGroup.transpose Λ⁻¹) *ᵥ ψ simp [dotProduct, Vector.rep_apply_eq_mulVec, CoVector.rep_apply_eq_mulVec]All goals completed! 🐙
    ·d:ℕΛ:↑(LorentzGroup d)φ:Vector dψ:CoVector d⊢ ↑Λ *ᵥ φ ⬝ᵥ ↑(LorentzGroup.transpose Λ⁻¹) *ᵥ ψ =
  ((AlgebraTensorModule.curry
        ((Representation.trivial ℝ ↑(LorentzGroup d) ℝ) Λ ∘ₗ
          TensorProduct.lift (LinearMap.mk₂ ℝ (fun φ ψ => ∑ i, φ i * ψ i) ⋯ ⋯ ⋯ ⋯)))
      φ)
    ψ simp [dotProduct_mulVec, LorentzGroup.transpose_val,
        vecMul_transpose, mulVec_mulVec, LorentzGroup.coe_inv, inv_mul_of_invertible Λ.1]d:ℕΛ:↑(LorentzGroup d)φ:Vector dψ:CoVector d⊢ φ ⬝ᵥ ψ = ∑ i, φ i * ψ i
      rflAll goals completed! 🐙

The intertwining map defining the contraction of a covariant Lorentz vector with a contravariant Lorentz vector.

def CoVector.contract : (CoVector.rep.tprod Vector.rep).IntertwiningMap
    (Representation.trivial ℝ (LorentzGroup d) ℝ) where
  toLinearMap := byd:ℕ⊢ CoVector d ⊗[ℝ] Vector d →ₗ[ℝ] ℝ
    refine TensorProduct.lift (LinearMap.mk₂ ℝ (fun φ ψ => ∑ i, φ i * ψ i) ?_ ?_ ?_ ?_)refine_1d:ℕ⊢ ∀ (m₁ m₂ : CoVector d) (n : Vector d), ∑ i, (m₁ + m₂) i * n i = ∑ i, m₁ i * n i + ∑ i, m₂ i * n irefine_2d:ℕ⊢ ∀ (c : ℝ) (m : CoVector d) (n : Vector d), ∑ i, (c • m) i * n i = c • ∑ i, m i * n irefine_3d:ℕ⊢ ∀ (m : CoVector d) (n₁ n₂ : Vector d), ∑ i, m i * (n₁ + n₂) i = ∑ i, m i * n₁ i + ∑ i, m i * n₂ irefine_4d:ℕ⊢ ∀ (c : ℝ) (m : CoVector d) (n : Vector d), ∑ i, m i * (c • n) i = c • ∑ i, m i * n i
    ·refine_1d:ℕ⊢ ∀ (m₁ m₂ : CoVector d) (n : Vector d), ∑ i, (m₁ + m₂) i * n i = ∑ i, m₁ i * n i + ∑ i, m₂ i * n i simp [add_mul, Finset.sum_add_distrib]All goals completed! 🐙
    ·refine_2d:ℕ⊢ ∀ (c : ℝ) (m : CoVector d) (n : Vector d), ∑ i, (c • m) i * n i = c • ∑ i, m i * n i simp [Finset.mul_sum, mul_assoc]All goals completed! 🐙
    ·refine_3d:ℕ⊢ ∀ (m : CoVector d) (n₁ n₂ : Vector d), ∑ i, m i * (n₁ + n₂) i = ∑ i, m i * n₁ i + ∑ i, m i * n₂ i simp [mul_add, Finset.sum_add_distrib]All goals completed! 🐙
    ·refine_4d:ℕ⊢ ∀ (c : ℝ) (m : CoVector d) (n : Vector d), ∑ i, m i * (c • n) i = c • ∑ i, m i * n i introsrefine_4d:ℕc✝:ℝm✝:CoVector dn✝:Vector d⊢ ∑ i, m✝ i * (c✝ • n✝) i = c✝ • ∑ i, m✝ i * n✝ i
      simp_rw [refine_4d:ℕc✝:ℝm✝:CoVector dn✝:Vector d⊢ ∑ i, m✝ i * (c✝ • n✝) i = c✝ • ∑ i, m✝ i * n✝ iVector.apply_smul,refine_4d:ℕc✝:ℝm✝:CoVector dn✝:Vector d⊢ ∑ x, m✝ x * (c✝ * n✝ x) = c✝ • ∑ i, m✝ i * n✝ i smul_eq_mul,refine_4d:ℕc✝:ℝm✝:CoVector dn✝:Vector d⊢ ∑ x, m✝ x * (c✝ * n✝ x) = c✝ * ∑ i, m✝ i * n✝ i Finset.mul_sumrefine_4d:ℕc✝:ℝm✝:CoVector dn✝:Vector d⊢ ∑ x, m✝ x * (c✝ * n✝ x) = ∑ i, c✝ * (m✝ i * n✝ i)]
      exact Finset.sum_congr rfl (fun _ _ ↦ byd:ℕc✝:ℝm✝:CoVector dn✝:Vector dx✝¹:Fin 1 ⊕ Fin dx✝:x✝¹ ∈ Finset.univ⊢ m✝ x✝¹ * (c✝ * n✝ x✝¹) = c✝ * (m✝ x✝¹ * n✝ x✝¹) ringAll goals completed! 🐙)
  isIntertwining' Λ := byd:ℕΛ:↑(LorentzGroup d)⊢ TensorProduct.lift (LinearMap.mk₂ ℝ (fun φ ψ => ∑ i, φ i * ψ i) ⋯ ⋯ ⋯ ⋯) ∘ₗ (rep.tprod Vector.rep) Λ =
  (Representation.trivial ℝ ↑(LorentzGroup d) ℝ) Λ ∘ₗ
    TensorProduct.lift (LinearMap.mk₂ ℝ (fun φ ψ => ∑ i, φ i * ψ i) ⋯ ⋯ ⋯ ⋯)
    ext φ ψd:ℕΛ:↑(LorentzGroup d)φ:CoVector dψ:Vector d⊢ ((AlgebraTensorModule.curry
        (TensorProduct.lift (LinearMap.mk₂ ℝ (fun φ ψ => ∑ i, φ i * ψ i) ⋯ ⋯ ⋯ ⋯) ∘ₗ (rep.tprod Vector.rep) Λ))
      φ)
    ψ =
  ((AlgebraTensorModule.curry
        ((Representation.trivial ℝ ↑(LorentzGroup d) ℝ) Λ ∘ₗ
          TensorProduct.lift (LinearMap.mk₂ ℝ (fun φ ψ => ∑ i, φ i * ψ i) ⋯ ⋯ ⋯ ⋯)))
      φ)
    ψ
    trans ((LorentzGroup.transpose Λ⁻¹).1 *ᵥ φ) ⬝ᵥ (Λ.1 *ᵥ ψ)d:ℕΛ:↑(LorentzGroup d)φ:CoVector dψ:Vector d⊢ ((AlgebraTensorModule.curry
        (TensorProduct.lift (LinearMap.mk₂ ℝ (fun φ ψ => ∑ i, φ i * ψ i) ⋯ ⋯ ⋯ ⋯) ∘ₗ (rep.tprod Vector.rep) Λ))
      φ)
    ψ =
  ↑(LorentzGroup.transpose Λ⁻¹) *ᵥ φ ⬝ᵥ ↑Λ *ᵥ ψd:ℕΛ:↑(LorentzGroup d)φ:CoVector dψ:Vector d⊢ ↑(LorentzGroup.transpose Λ⁻¹) *ᵥ φ ⬝ᵥ ↑Λ *ᵥ ψ =
  ((AlgebraTensorModule.curry
        ((Representation.trivial ℝ ↑(LorentzGroup d) ℝ) Λ ∘ₗ
          TensorProduct.lift (LinearMap.mk₂ ℝ (fun φ ψ => ∑ i, φ i * ψ i) ⋯ ⋯ ⋯ ⋯)))
      φ)
    ψ
    ·d:ℕΛ:↑(LorentzGroup d)φ:CoVector dψ:Vector d⊢ ((AlgebraTensorModule.curry
        (TensorProduct.lift (LinearMap.mk₂ ℝ (fun φ ψ => ∑ i, φ i * ψ i) ⋯ ⋯ ⋯ ⋯) ∘ₗ (rep.tprod Vector.rep) Λ))
      φ)
    ψ =
  ↑(LorentzGroup.transpose Λ⁻¹) *ᵥ φ ⬝ᵥ ↑Λ *ᵥ ψ simp [dotProduct, Vector.rep_apply_eq_mulVec, CoVector.rep_apply_eq_mulVec]All goals completed! 🐙
    ·d:ℕΛ:↑(LorentzGroup d)φ:CoVector dψ:Vector d⊢ ↑(LorentzGroup.transpose Λ⁻¹) *ᵥ φ ⬝ᵥ ↑Λ *ᵥ ψ =
  ((AlgebraTensorModule.curry
        ((Representation.trivial ℝ ↑(LorentzGroup d) ℝ) Λ ∘ₗ
          TensorProduct.lift (LinearMap.mk₂ ℝ (fun φ ψ => ∑ i, φ i * ψ i) ⋯ ⋯ ⋯ ⋯)))
      φ)
    ψ simp [dotProduct_mulVec, LorentzGroup.transpose_val,
        mulVec_transpose, vecMul_vecMul, LorentzGroup.coe_inv, inv_mul_of_invertible Λ.1]d:ℕΛ:↑(LorentzGroup d)φ:CoVector dψ:Vector d⊢ φ ⬝ᵥ ψ = ∑ i, φ i * ψ i
      rflAll goals completed! 🐙

B. Properties of the contractions

              lemma Vector.contract_tmul (φ : Vector d) (ψ : CoVector d) :
    Vector.contract (φ ⊗ₜ ψ) = ∑ i, φ i * ψ i := rfllemma CoVector.contract_tmul (φ : CoVector d) (ψ : Vector d) :
    CoVector.contract (φ ⊗ₜ ψ) = ∑ i, φ i * ψ i := rfllemma Vector.contract_basis_left (μ : Fin 1 ⊕ Fin d) (ψ : CoVector d) :
    Vector.contract (basis μ ⊗ₜ ψ) = ψ μ := byd:ℕμ:Fin 1 ⊕ Fin dψ:CoVector d⊢ contract (basis μ ⊗ₜ[ℝ] ψ) = ψ μ simp [Vector.contract_tmul, basis_apply]All goals completed! 🐙lemma CoVector.contract_basis_left (μ : Fin 1 ⊕ Fin d) (φ : Vector d) :
    CoVector.contract (basis μ ⊗ₜ φ) = φ μ := byd:ℕμ:Fin 1 ⊕ Fin dφ:Vector d⊢ contract (basis μ ⊗ₜ[ℝ] φ) = φ μ simp [CoVector.contract_tmul, basis_apply]All goals completed! 🐙lemma Vector.contract_basis_right (φ : Vector d) (μ : Fin 1 ⊕ Fin d) :
    Vector.contract (φ ⊗ₜ basis μ) = φ μ := byd:ℕφ:Vector dμ:Fin 1 ⊕ Fin d⊢ contract (φ ⊗ₜ[ℝ] basis μ) = φ μ simp [Vector.contract_tmul, basis_apply]All goals completed! 🐙lemma CoVector.contract_basis_right (ψ : CoVector d) (μ : Fin 1 ⊕ Fin d) :
    CoVector.contract (ψ ⊗ₜ basis μ) = ψ μ := byd:ℕψ:CoVector dμ:Fin 1 ⊕ Fin d⊢ contract (ψ ⊗ₜ[ℝ] basis μ) = ψ μ simp [CoVector.contract_tmul, basis_apply]All goals completed! 🐙lemma Vector.contract_eq_coVector_contract (φ : Vector d) (ψ : CoVector d) :
    Vector.contract (φ ⊗ₜ ψ) = CoVector.contract (ψ ⊗ₜ φ) := byd:ℕφ:Vector dψ:CoVector d⊢ contract (φ ⊗ₜ[ℝ] ψ) = CoVector.contract (ψ ⊗ₜ[ℝ] φ)
  simp_rw [d:ℕφ:Vector dψ:CoVector d⊢ contract (φ ⊗ₜ[ℝ] ψ) = CoVector.contract (ψ ⊗ₜ[ℝ] φ)Vector.contract_tmul,d:ℕφ:Vector dψ:CoVector d⊢ ∑ i, φ i * ψ i = CoVector.contract (ψ ⊗ₜ[ℝ] φ) CoVector.contract_tmul,d:ℕφ:Vector dψ:CoVector d⊢ ∑ i, φ i * ψ i = ∑ i, ψ i * φ i mul_commAll goals completed! 🐙]lemma Vector.contract_rep (Λ : LorentzGroup d) (φ : Vector d) (ψ : CoVector d) :
    Vector.contract ((Vector.rep Λ φ) ⊗ₜ (CoVector.rep Λ ψ)) = Vector.contract (φ ⊗ₜ ψ) := byd:ℕΛ:↑(LorentzGroup d)φ:Vector dψ:CoVector d⊢ contract ((rep Λ) φ ⊗ₜ[ℝ] (CoVector.rep Λ) ψ) = contract (φ ⊗ₜ[ℝ] ψ)
  convert! Vector.contract.isIntertwining _ _ Λ (φ ⊗ₜ ψ)All goals completed! 🐙lemma CoVector.contract_rep (Λ : LorentzGroup d) (φ : CoVector d) (ψ : Vector d) :
    CoVector.contract ((CoVector.rep Λ φ) ⊗ₜ (Vector.rep Λ ψ)) = CoVector.contract (φ ⊗ₜ ψ) := byd:ℕΛ:↑(LorentzGroup d)φ:CoVector dψ:Vector d⊢ contract ((rep Λ) φ ⊗ₜ[ℝ] (Vector.rep Λ) ψ) = contract (φ ⊗ₜ[ℝ] ψ)
  convert! CoVector.contract.isIntertwining _ _ Λ (φ ⊗ₜ ψ)All goals completed! 🐙