1. Physlib
  2. Relativity
  3. Tensors
  4. LeviCivita
  5. Basic
Imports
/- Copyright (c) 2026 Robert Sneiderman. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Robert Sneiderman -/ module public import Physlib.Relativity.Tensors.RealTensor.Basic public import Physlib.Relativity.Tensors.UnitTensor public import Physlib.Meta.Sorry public import Physlib.Relativity.Tensors.OfInt public import Physlib.Mathematics.KroneckerDelta.Basic

The Levi-Civita tensor as a real Lorentz tensor

i. Overview

This file defines the rank-four Levi-Civita tensor εᵘᵛᵖᵟ as a real Lorentz tensor in d = 3 spatial dimensions, with ε⁰¹²³ = 1, and proves its antisymmetry under each adjacent transposition of indices.

The component on a multi-index f is the generalized Kronecker delta of f against the identity, i.e. the sign of f when f is a permutation and 0 otherwise. The integer components are carried by TensorSpecies.Tensor.TensorInt.toTensor.

ii. Key results

    leviCivita : the rank-four Levi-Civita tensor ε4, with ε⁰¹²³ = 1.

    leviCivita_basis_repr_apply : its standard-basis components as a generalized Kronecker delta.

    leviCivita_antisymm, leviCivita_antisymm_mid, leviCivita_antisymm_last : antisymmetry under each adjacent transposition of the indices.

iii. Table of contents

    A. Definition

    B. Components in the standard basis

    C. Antisymmetry

iv. References

@[expose] public section

A. Definition

The Levi-Civita tensor εᵘᵛᵖᵟ as a real Lorentz tensor.

scoped[realLorentzTensor] notation "ε4" => leviCivita

The TensorInt.toTensor form of the Levi-Civita tensor.

lemma leviCivita_eq_ofInt : ε4 = TensorInt.toTensor (S := realLorentzTensor 3) (c := ![Color.up, Color.up, Color.up, Color.up]) fun f => generalizedKroneckerDelta (fun i => finSumFinEquiv (f i)) (id : Fin 4 → Fin 4) := rfl

The Euclidean Levi-Civita symbol ε_{ijkl} in dimension 4.

def _root_.euclidLeviCivita (g : Fin 4 → Fin 4) : ℝ := generalizedKroneckerDelta g (id : Fin 4 → Fin 4)

B. Components in the standard basis

The components of the Levi-Civita tensor in the standard basis are the generalized Kronecker delta of the multi-index against the identity.

All goals completed! 🐙

The Levi-Civita tensor vanishes on any multi-index with a repeated value: if two distinct index positions i ≠ j carry the same basis index, the component is zero.

All goals completed! 🐙

C. Antisymmetry

The Levi-Civita tensor is antisymmetric in its first two indices {ε4 | μ ν ρ σ = - ε4 | ν μ ρ σ}ᵀ.

b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ generalizedKroneckerDelta (fun i => finSumFinEquiv (b i)) id = generalizedKroneckerDelta ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0, 2, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 0 1)) id b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ (fun i => finSumFinEquiv (b i)) = (fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0, 2, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 0 1) b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]i:Fin (Nat.succ 0).succ.succ.succ⊢ finSumFinEquiv (b i) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0, 2, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 0 1)) i b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨0, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0, 2, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 0 1)) ((fun i => i) ⟨0, ⋯⟩)b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨1, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0, 2, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 0 1)) ((fun i => i) ⟨1, ⋯⟩)b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨2, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0, 2, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 0 1)) ((fun i => i) ⟨2, ⋯⟩)b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨3, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0, 2, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 0 1)) ((fun i => i) ⟨3, ⋯⟩) b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨0, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0, 2, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 0 1)) ((fun i => i) ⟨0, ⋯⟩)b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨1, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0, 2, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 0 1)) ((fun i => i) ⟨1, ⋯⟩)b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨2, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0, 2, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 0 1)) ((fun i => i) ⟨2, ⋯⟩)b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨3, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![1, 0, 2, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 0 1)) ((fun i => i) ⟨3, ⋯⟩) All goals completed! 🐙

The Levi-Civita tensor is antisymmetric in its middle two indices {ε4 | μ ν ρ σ = - ε4 | μ ρ ν σ}ᵀ.

b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ generalizedKroneckerDelta (fun i => finSumFinEquiv (b i)) id = generalizedKroneckerDelta ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 2, 1, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 1 2)) id b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ (fun i => finSumFinEquiv (b i)) = (fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 2, 1, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 1 2) b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]i:Fin (Nat.succ 0).succ.succ.succ⊢ finSumFinEquiv (b i) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 2, 1, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 1 2)) i b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨0, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 2, 1, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 1 2)) ((fun i => i) ⟨0, ⋯⟩)b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨1, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 2, 1, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 1 2)) ((fun i => i) ⟨1, ⋯⟩)b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨2, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 2, 1, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 1 2)) ((fun i => i) ⟨2, ⋯⟩)b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨3, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 2, 1, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 1 2)) ((fun i => i) ⟨3, ⋯⟩) b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨0, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 2, 1, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 1 2)) ((fun i => i) ⟨0, ⋯⟩)b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨1, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 2, 1, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 1 2)) ((fun i => i) ⟨1, ⋯⟩)b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨2, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 2, 1, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 1 2)) ((fun i => i) ⟨2, ⋯⟩)b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨3, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 2, 1, 3] ⋯ i))) i)) ∘ ⇑(Equiv.swap 1 2)) ((fun i => i) ⟨3, ⋯⟩) All goals completed! 🐙

The Levi-Civita tensor is antisymmetric in its last two indices {ε4 | μ ν ρ σ = - ε4 | μ ν σ ρ}ᵀ.

b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ generalizedKroneckerDelta (fun i => finSumFinEquiv (b i)) id = generalizedKroneckerDelta ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 1, 3, 2] ⋯ i))) i)) ∘ ⇑(Equiv.swap 2 3)) id b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ (fun i => finSumFinEquiv (b i)) = (fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 1, 3, 2] ⋯ i))) i)) ∘ ⇑(Equiv.swap 2 3) b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]i:Fin (Nat.succ 0).succ.succ.succ⊢ finSumFinEquiv (b i) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 1, 3, 2] ⋯ i))) i)) ∘ ⇑(Equiv.swap 2 3)) i b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨0, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 1, 3, 2] ⋯ i))) i)) ∘ ⇑(Equiv.swap 2 3)) ((fun i => i) ⟨0, ⋯⟩)b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨1, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 1, 3, 2] ⋯ i))) i)) ∘ ⇑(Equiv.swap 2 3)) ((fun i => i) ⟨1, ⋯⟩)b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨2, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 1, 3, 2] ⋯ i))) i)) ∘ ⇑(Equiv.swap 2 3)) ((fun i => i) ⟨2, ⋯⟩)b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨3, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 1, 3, 2] ⋯ i))) i)) ∘ ⇑(Equiv.swap 2 3)) ((fun i => i) ⟨3, ⋯⟩) b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨0, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 1, 3, 2] ⋯ i))) i)) ∘ ⇑(Equiv.swap 2 3)) ((fun i => i) ⟨0, ⋯⟩)b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨1, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 1, 3, 2] ⋯ i))) i)) ∘ ⇑(Equiv.swap 2 3)) ((fun i => i) ⟨1, ⋯⟩)b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨2, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 1, 3, 2] ⋯ i))) i)) ∘ ⇑(Equiv.swap 2 3)) ((fun i => i) ⟨2, ⋯⟩)b:ComponentIdx ![Color.up, Color.up, Color.up, Color.up]⊢ finSumFinEquiv (b ((fun i => i) ⟨3, ⋯⟩)) = ((fun i => finSumFinEquiv ((fun i => (basisIdxCongr ⋯) (b (IsReindexing.inv ![0, 1, 3, 2] ⋯ i))) i)) ∘ ⇑(Equiv.swap 2 3)) ((fun i => i) ⟨3, ⋯⟩) All goals completed! 🐙
@[sorryful] lemma declaration uses `sorry`leviCivita_contract_three : {ε4 | μ ν ρ σ ⊗ ε4 | τ(μ) τ(ν) τ(ρ) τ(τ) = (-6) • unitTensor (S := realLorentzTensor) Color.down | σ τ }ᵀ := ⊢ (contrT 2 0 2 ⋯) ((contrT 4 1 4 ⋯) ((contrT 6 2 6 ⋯) ((prodT ε4) ((toDualMapAtIndex 3) ((toDualMapAtIndex 2) ((toDualMapAtIndex 1) ((toDualMapAtIndex 0) ε4))))))) = (permT ![0, 1] ⋯) (-6 • unitTensor Color.down) All goals completed! 🐙-- `checkType` linter: under the v4.32.0 toolchain, whnf on this tensor-notation -- statement exceeds the linter's 200k-heartbeat budget (it did not on v4.31.0). -- Statement unchanged; see the v4.32.0 bump commit message. @[sorryful, nolint checkType] lemma declaration uses `sorry`leviCivita_contract_self : {ε4 | μ ν ρ σ ⊗ ε4 | τ(μ) τ(ν) τ(ρ) τ(σ)}ᵀ.toField = - 24 := ⊢ toField ((contrT 0 0 1 ⋯) ((contrT 2 1 3 ⋯) ((contrT 4 2 5 ⋯) ((contrT 6 3 7 ⋯) ((prodT ε4) ((toDualMapAtIndex 3) ((toDualMapAtIndex 2) ((toDualMapAtIndex 1) ((toDualMapAtIndex 0) ε4))))))))) = -24 All goals completed! 🐙