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.Mathematics.KroneckerDelta.Basic
public import Mathlib.LinearAlgebra.Matrix.PermutationThe Levi-Civita symbol in general dimension
i. Overview
This module defines the Levi-Civita symbol leviCivitaSymbol on a general finite index
type ι: for g : ι → ι it is the sign of g when g is a permutation and 0
otherwise. Taking ι = Fin d gives the Levi-Civita symbol ε_{i₁ ⋯ i_d} in dimension
d, normalized by ε_{0 1 ⋯ (d-1)} = 1.
The definition is the generalizedKroneckerDelta of g against the identity, i.e. the
determinant of the matrix of Kronecker deltas δ[g i, j], so the basic properties are
inherited from the determinant: the value 1 on the identity, antisymmetry under
transposition of two indices, vanishing on repeated indices, and the sign of a
permutation via Matrix.det_permutation.
ii. Key results
leviCivitaSymbol : the Levi-Civita symbol on a finite index type, valued in ℤ.
leviCivitaSymbol_id : the normalization ε_{0 1 ⋯ (d-1)} = 1.
leviCivitaSymbol_perm : on a permutation σ the symbol is the sign of σ.
leviCivitaSymbol_comp_swap : antisymmetry under transposition of two indices.
leviCivitaSymbol_swap_comp : antisymmetry under transposition of two index values.
leviCivitaSymbol_eq_zero_iff : the symbol vanishes exactly on repeated indices.
iii. Table of contents
A. Definition
B. Value on permutations
C. Antisymmetry
D. Vanishing on repeated indices
iv. References
https://en.wikipedia.org/wiki/Levi-Civita_symbol
@[expose] public sectionA. Definition
The Levi-Civita symbol on a finite index type ι: leviCivitaSymbol g is the sign
of g when g : ι → ι is a permutation, and 0 otherwise. It is the generalized
Kronecker delta of g against the identity, i.e. the determinant of the matrix of
Kronecker deltas δ[g i, j].
For ι = Fin d this is the Levi-Civita symbol ε_{i₁ ⋯ i_d} in dimension d,
normalized by ε_{0 1 ⋯ (d-1)} = 1.
def leviCivitaSymbol (g : ι → ι) : ℤ :=
generalizedKroneckerDelta g (id : ι → ι)
The Levi-Civita symbol as the determinant of the matrix of Kronecker deltas
δ[g i, j].
lemma leviCivitaSymbol_eq_det (g : ι → ι) :
leviCivitaSymbol g = Matrix.det (fun i j => ((kroneckerDelta (g i) j : ℕ) : ℤ)) :=
rfl
The Levi-Civita symbol of the identity, i.e. ε_{0 1 ⋯ (d-1)}, is 1.
ι:Typeinst✝¹:DecidableEq ιinst✝:Fintype ι⊢ Matrix.det 1 = 1
All goals completed! 🐙B. Value on permutations
The Levi-Civita symbol of a permutation σ is the sign of σ.
ι:Typeinst✝¹:DecidableEq ιinst✝:Fintype ισ:Equiv.Perm ι⊢ (Equiv.Perm.permMatrix ℤ σ).det = ↑(Equiv.Perm.sign σ)
All goals completed! 🐙C. Antisymmetry
The Levi-Civita symbol is antisymmetric under transposition of two of its indices: precomposing with the swap of two distinct index positions negates it.
lemma leviCivitaSymbol_comp_swap (g : ι → ι) {i j : ι} (hij : i ≠ j) :
leviCivitaSymbol (g ∘ Equiv.swap i j) = - leviCivitaSymbol g :=
generalizedKroneckerDelta_swap g id hijThe Levi-Civita symbol is antisymmetric under transposition of two index values: postcomposing with the swap of two distinct values exchanges those two values wherever they occur and negates it.
ι:Typeinst✝¹:DecidableEq ιinst✝:Fintype ιg:ι → ιi:ιj:ιhij:i ≠ jh:(fun a b => ↑δ[(⇑(Equiv.swap i j) ∘ g) a,b]) = Matrix.submatrix (fun a b => ↑δ[g a,b]) id ⇑(Equiv.swap i j)⊢ ↑↑(-1) * leviCivitaSymbol g = -leviCivitaSymbol g
All goals completed! 🐙D. Vanishing on repeated indices
The Levi-Civita symbol vanishes on a repeated index: if two distinct index positions
i ≠ j carry the same value, the symbol is zero.
All goals completed! 🐙)The Levi-Civita symbol vanishes on maps which are not injective.
lemma leviCivitaSymbol_eq_zero_of_not_injective {g : ι → ι} (h : ¬ Function.Injective g) :
leviCivitaSymbol g = 0 := ι:Typeinst✝¹:DecidableEq ιinst✝:Fintype ιg:ι → ιh:¬Function.Injective g⊢ leviCivitaSymbol g = 0
ι:Typeinst✝¹:DecidableEq ιinst✝:Fintype ιg:ι → ιh:∃ x x_1, ∃ (_ : g x = g x_1), ¬x = x_1⊢ leviCivitaSymbol g = 0
ι:Typeinst✝¹:DecidableEq ιinst✝:Fintype ιg:ι → ιi:ιj:ιhgij:g i = g jhij:¬i = j⊢ leviCivitaSymbol g = 0
All goals completed! 🐙The Levi-Civita symbol vanishes exactly on maps with a repeated index, i.e. on maps which are not injective.
ι:Typeinst✝¹:DecidableEq ιinst✝:Fintype ισ:Equiv.Perm ιh:↑(Equiv.Perm.sign σ) = 0hinj:Function.Injective ⇑σ⊢ False
All goals completed! 🐙