Physlib.Mathematics.KroneckerDelta.Basic

Imports

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

public import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
public import Mathlib.Algebra.CharZero.Defs
public import Mathlib.Algebra.Field.Defs
public import Mathlib.Algebra.Module.Defs
public import Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Kronecker delta

i. Overview

This module defines the Kronecker delta kroneckerDelta i j (notation δ[i,j]), equal to 1 when i = j and 0 otherwise, together with its behaviour under scalar multiplication, symmetrization, and finite sums. It also defines the generalizedKroneckerDelta, the determinant of a matrix of Kronecker deltas.

ii. Key results

kroneckerDelta : the Kronecker delta on a type with decidable equality.

generalizedKroneckerDelta : the determinant form det (δ[μᵢ, νⱼ]).

iii. Table of contents

A. The Kronecker delta

B. Conditions for smul to vanish

C. Symmetrization

D. Sums

E. The generalized Kronecker delta

iv. References

@[expose] public section

A. The Kronecker delta

The Kronecker delta function, ite (i = j) 1 0.

def kroneckerDelta (i j : α) : ℕ := if i = j then 1 else 0

              @[inherit_doc]
notation "δ[" i "," j "]" => kroneckerDelta i j@[simp]
lemma eq_one_of_same (i : α) : δ[i,i] = 1 := if_pos rfllemma eq_zero_of_ne {i j : α} (h : i ≠ j) : δ[i,j] = 0 := if_neg h

@[simp]
lemma eq_of_coe {p : α → Prop} (i j : Subtype p) : δ[(i : α),j] = δ[i,j] := byα:Type u_1inst✝:DecidableEq αp:α → Propi:Subtype pj:Subtype p⊢ δ[↑i,↑j] = δ[i,j]
  rcases eq_or_ne i j with (rfl | hne)inlα:Type u_1inst✝:DecidableEq αp:α → Propi:Subtype p⊢ δ[↑i,↑i] = δ[i,i]inrα:Type u_1inst✝:DecidableEq αp:α → Propi:Subtype pj:Subtype phne:i ≠ j⊢ δ[↑i,↑j] = δ[i,j]
  ·inlα:Type u_1inst✝:DecidableEq αp:α → Propi:Subtype p⊢ δ[↑i,↑i] = δ[i,i] repeat rw [eq_one_of_sameinlα:Type u_1inst✝:DecidableEq αp:α → Propi:Subtype p⊢ 1 = δ[i,i]All goals completed! 🐙]All goals completed! 🐙
  ·inrα:Type u_1inst✝:DecidableEq αp:α → Propi:Subtype pj:Subtype phne:i ≠ j⊢ δ[↑i,↑j] = δ[i,j] rw [eq_zero_of_ne hne,inrα:Type u_1inst✝:DecidableEq αp:α → Propi:Subtype pj:Subtype phne:i ≠ j⊢ δ[↑i,↑j] = 0All goals completed! 🐙 eq_zero_of_ne <| Subtype.coe_ne_coe.mpr hneinrα:Type u_1inst✝:DecidableEq αp:α → Propi:Subtype pj:Subtype phne:i ≠ j⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙lemma eq_zero_of_not {p : α → Prop} {i j : α} (hi : ¬p i) (hj : p j) : δ[i,j] = 0 :=
  eq_zero_of_ne (fun h ↦ hi (h ▸ hj))

The Kronecker delta is invariant under the component-index equivalence finSumFinEquiv.

lemma kroneckerDelta_finSumFinEquiv (a b : Fin 1 ⊕ Fin 3) :
    kroneckerDelta (finSumFinEquiv a) (finSumFinEquiv b) = kroneckerDelta a b := bya:Fin 1 ⊕ Fin 3b:Fin 1 ⊕ Fin 3⊢ δ[finSumFinEquiv a,finSumFinEquiv b] = δ[a,b]
  simp only [kroneckerDelta, Equiv.apply_eq_iff_eq]All goals completed! 🐙

B. Conditions for smul to vanish

              lemma smul_of_eq_zero [AddMonoid M] (i j : α) {f : α → α → M} (hf : f i i = 0) :
    δ[i,j] • f i j = 0 := byα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αj:αf:α → α → Mhf:f i i = 0⊢ δ[i,j] • f i j = 0
  rcases eq_or_ne i j with (rfl | hne)inlα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αf:α → α → Mhf:f i i = 0⊢ δ[i,i] • f i i = 0inrα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αj:αf:α → α → Mhf:f i i = 0hne:i ≠ j⊢ δ[i,j] • f i j = 0
  ·inlα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αf:α → α → Mhf:f i i = 0⊢ δ[i,i] • f i i = 0 exact smul_eq_zero_of_right _ hfAll goals completed! 🐙
  ·inrα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αj:αf:α → α → Mhf:f i i = 0hne:i ≠ j⊢ δ[i,j] • f i j = 0 exact smul_eq_zero_of_left (eq_zero_of_ne hne) _All goals completed! 🐙lemma smul_eq_zero_iff [AddMonoid M] (i j : α) (f : α → α → M) :
    δ[i,j] • f i j = 0 ↔ i ≠ j ∨ f i i = 0 := byα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αj:αf:α → α → M⊢ δ[i,j] • f i j = 0 ↔ i ≠ j ∨ f i i = 0
  rcases eq_or_ne i j with (rfl | hne)inlα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αf:α → α → M⊢ δ[i,i] • f i i = 0 ↔ i ≠ i ∨ f i i = 0inrα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αj:αf:α → α → Mhne:i ≠ j⊢ δ[i,j] • f i j = 0 ↔ i ≠ j ∨ f i i = 0
  ·inlα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αf:α → α → M⊢ δ[i,i] • f i i = 0 ↔ i ≠ i ∨ f i i = 0 simpAll goals completed! 🐙
  ·inrα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αj:αf:α → α → Mhne:i ≠ j⊢ δ[i,j] • f i j = 0 ↔ i ≠ j ∨ f i i = 0 simp [eq_zero_of_ne, hne]All goals completed! 🐙lemma smul_eq_zero_iff' [AddMonoid M] (i : α) (f : α → α → M) :
    (∀ j : α, δ[i,j] • f i j = 0) ↔ f i i = 0 := byα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αf:α → α → M⊢ (∀ (j : α), δ[i,j] • f i j = 0) ↔ f i i = 0
  refine ⟨fun h ↦ ?_, fun hf j ↦ smul_of_eq_zero i j hf⟩α:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αf:α → α → Mh:∀ (j : α), δ[i,j] • f i j = 0⊢ f i i = 0
  simpa [one_nsmul] using h iAll goals completed! 🐙lemma smul_eq_zero_iff'' [AddMonoid M] (f : α → α → M) :
    (∀ i j : α, δ[i,j] • f i j = 0) ↔ ∀ i : α, f i i = 0 :=
  forall_congr' fun j ↦ smul_eq_zero_iff' j f

C. Symmetrization

              lemma symm (i j : α) : δ[i,j] = δ[j,i] := ite_cond_congr <| Eq.propIntro Eq.symm Eq.symmlemma smul_symm [AddMonoid M] (i j : α) (f : α → α → M) : δ[i,j] • f j i = δ[i,j] • f i j := byα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αj:αf:α → α → M⊢ δ[i,j] • f j i = δ[i,j] • f i j
  rcases eq_or_ne i j with (rfl | hne)inlα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αf:α → α → M⊢ δ[i,i] • f i i = δ[i,i] • f i iinrα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αj:αf:α → α → Mhne:i ≠ j⊢ δ[i,j] • f j i = δ[i,j] • f i j
  ·inlα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αf:α → α → M⊢ δ[i,i] • f i i = δ[i,i] • f i i rflAll goals completed! 🐙
  ·inrα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αj:αf:α → α → Mhne:i ≠ j⊢ δ[i,j] • f j i = δ[i,j] • f i j simp only [eq_zero_of_ne hne, zero_smul]All goals completed! 🐙lemma symmetrize [AddMonoid M] (i j : α) (f : α → α → M) :
    δ[i,j] • (f i j + f j i) = (2 * δ[i,j]) • f i j := byα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αj:αf:α → α → M⊢ δ[i,j] • (f i j + f j i) = (2 * δ[i,j]) • f i j
  rcases eq_or_ne i j with (rfl | hne)inlα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αf:α → α → M⊢ δ[i,i] • (f i i + f i i) = (2 * δ[i,i]) • f i iinrα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αj:αf:α → α → Mhne:i ≠ j⊢ δ[i,j] • (f i j + f j i) = (2 * δ[i,j]) • f i j
  ·inlα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αf:α → α → M⊢ δ[i,i] • (f i i + f i i) = (2 * δ[i,i]) • f i i simp [two_nsmul]All goals completed! 🐙
  ·inrα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddMonoid Mi:αj:αf:α → α → Mhne:i ≠ j⊢ δ[i,j] • (f i j + f j i) = (2 * δ[i,j]) • f i j simp [eq_zero_of_ne hne]All goals completed! 🐙

lemma symmetrize' [AddCommMonoid M] {K : Type*} [Semifield K] [CharZero K] [Module K M]
    (i j : α) (f : α → α → M) : δ[i,j] • (2 : K)⁻¹ • (f i j + f j i) = δ[i,j] • f i j := byα:Type u_1M:Type u_2inst✝⁴:DecidableEq αinst✝³:AddCommMonoid MK:Type u_3inst✝²:Semifield Kinst✝¹:CharZero Kinst✝:Module K Mi:αj:αf:α → α → M⊢ δ[i,j] • 2⁻¹ • (f i j + f j i) = δ[i,j] • f i j
  rcases eq_or_ne i j with (rfl | hne)inlα:Type u_1M:Type u_2inst✝⁴:DecidableEq αinst✝³:AddCommMonoid MK:Type u_3inst✝²:Semifield Kinst✝¹:CharZero Kinst✝:Module K Mi:αf:α → α → M⊢ δ[i,i] • 2⁻¹ • (f i i + f i i) = δ[i,i] • f i iinrα:Type u_1M:Type u_2inst✝⁴:DecidableEq αinst✝³:AddCommMonoid MK:Type u_3inst✝²:Semifield Kinst✝¹:CharZero Kinst✝:Module K Mi:αj:αf:α → α → Mhne:i ≠ j⊢ δ[i,j] • 2⁻¹ • (f i j + f j i) = δ[i,j] • f i j
  ·inlα:Type u_1M:Type u_2inst✝⁴:DecidableEq αinst✝³:AddCommMonoid MK:Type u_3inst✝²:Semifield Kinst✝¹:CharZero Kinst✝:Module K Mi:αf:α → α → M⊢ δ[i,i] • 2⁻¹ • (f i i + f i i) = δ[i,i] • f i i simp only [eq_one_of_same, one_nsmul, ← two_smul K, smul_smul]inlα:Type u_1M:Type u_2inst✝⁴:DecidableEq αinst✝³:AddCommMonoid MK:Type u_3inst✝²:Semifield Kinst✝¹:CharZero Kinst✝:Module K Mi:αf:α → α → M⊢ (2⁻¹ * 2) • f i i = f i i
    rw [inv_mul_cancel₀ (OfNat.zero_ne_ofNat 2).symm,inlα:Type u_1M:Type u_2inst✝⁴:DecidableEq αinst✝³:AddCommMonoid MK:Type u_3inst✝²:Semifield Kinst✝¹:CharZero Kinst✝:Module K Mi:αf:α → α → M⊢ 1 • f i i = f i iAll goals completed! 🐙 one_smulinlα:Type u_1M:Type u_2inst✝⁴:DecidableEq αinst✝³:AddCommMonoid MK:Type u_3inst✝²:Semifield Kinst✝¹:CharZero Kinst✝:Module K Mi:αf:α → α → M⊢ f i i = f i iAll goals completed! 🐙]All goals completed! 🐙
  ·inrα:Type u_1M:Type u_2inst✝⁴:DecidableEq αinst✝³:AddCommMonoid MK:Type u_3inst✝²:Semifield Kinst✝¹:CharZero Kinst✝:Module K Mi:αj:αf:α → α → Mhne:i ≠ j⊢ δ[i,j] • 2⁻¹ • (f i j + f j i) = δ[i,j] • f i j simp [eq_zero_of_ne hne]All goals completed! 🐙@[simp]
lemma smul_sub_eq_zero [AddGroup M] (i j : α) (f : α → α → M) : δ[i,j] • (f i j - f j i) = 0 := byα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddGroup Mi:αj:αf:α → α → M⊢ δ[i,j] • (f i j - f j i) = 0
  rcases eq_or_ne i j with (rfl | hne)inlα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddGroup Mi:αf:α → α → M⊢ δ[i,i] • (f i i - f i i) = 0inrα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddGroup Mi:αj:αf:α → α → Mhne:i ≠ j⊢ δ[i,j] • (f i j - f j i) = 0
  ·inlα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddGroup Mi:αf:α → α → M⊢ δ[i,i] • (f i i - f i i) = 0 exact smul_eq_zero_of_right _ (sub_self <| f i i)All goals completed! 🐙
  ·inrα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddGroup Mi:αj:αf:α → α → Mhne:i ≠ j⊢ δ[i,j] • (f i j - f j i) = 0 exact smul_eq_zero_of_left (eq_zero_of_ne hne) _All goals completed! 🐙

D. Sums

              @[simp]
lemma sum_mul [Fintype α] (i j : α) : ∑ k : α, δ[i,k] * δ[k,j] = δ[i,j] := byα:Type u_1inst✝¹:DecidableEq αinst✝:Fintype αi:αj:α⊢ ∑ k, δ[i,k] * δ[k,j] = δ[i,j]
  simp [kroneckerDelta]All goals completed! 🐙@[simp]
lemma sum_smul [Fintype α] (i : α) (f : α → M) : ∑ j : α, δ[i,j] • f j = f i := byα:Type u_1M:Type u_2inst✝²:DecidableEq αinst✝¹:AddCommMonoid Minst✝:Fintype αi:αf:α → M⊢ ∑ j, δ[i,j] • f j = f i
  simp [kroneckerDelta]All goals completed! 🐙lemma sum_sum_smul_eq_zero [Fintype α] {f : α → α → M} (hf : ∀ i : α, f i i = 0) :
    ∑ i : α, ∑ j : α, δ[i,j] • f i j = 0 := byα:Type u_1M:Type u_2inst✝²:DecidableEq αinst✝¹:AddCommMonoid Minst✝:Fintype αf:α → α → Mhf:∀ (i : α), f i i = 0⊢ ∑ i, ∑ j, δ[i,j] • f i j = 0
  simp [sum_smul, hf, sum_const_zero]All goals completed! 🐙lemma finset_sum_smul (s : Finset α) (i : α) (f : α → M) :
    ∑ j ∈ s, δ[i,j] • f j = if i ∈ s then f i else 0 := byα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddCommMonoid Ms:Finset αi:αf:α → M⊢ ∑ j ∈ s, δ[i,j] • f j = if i ∈ s then f i else 0
  simp [kroneckerDelta]All goals completed! 🐙

lemma finset_sum_sum_smul_eq_zero {s s' : Finset α} {f : α → α → M}
    (hf : ∀ i ∈ s ∩ s', f i i = 0) : ∑ i ∈ s, ∑ j ∈ s', δ[i,j] • f i j = 0 := byα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddCommMonoid Ms:Finset αs':Finset αf:α → α → Mhf:∀ i ∈ s ∩ s', f i i = 0⊢ ∑ i ∈ s, ∑ j ∈ s', δ[i,j] • f i j = 0
  simp only [finset_sum_smul, Finset.sum_ite_mem]α:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddCommMonoid Ms:Finset αs':Finset αf:α → α → Mhf:∀ i ∈ s ∩ s', f i i = 0⊢ ∑ i ∈ s ∩ s', f i i = 0
  rw [← sum_coe_sortα:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddCommMonoid Ms:Finset αs':Finset αf:α → α → Mhf:∀ i ∈ s ∩ s', f i i = 0⊢ ∑ i, f ↑i ↑i = 0α:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddCommMonoid Ms:Finset αs':Finset αf:α → α → Mhf:∀ i ∈ s ∩ s', f i i = 0⊢ ∑ i, f ↑i ↑i = 0]α:Type u_1M:Type u_2inst✝¹:DecidableEq αinst✝:AddCommMonoid Ms:Finset αs':Finset αf:α → α → Mhf:∀ i ∈ s ∩ s', f i i = 0⊢ ∑ i, f ↑i ↑i = 0
  simp [hf]All goals completed! 🐙

E. The generalized Kronecker delta

Integer-valued Kronecker entry via the existing kroneckerDelta.

local notation "δℤ" => (fun ρ σ => ((kroneckerDelta ρ σ : ℕ) : ℤ))

Generalized Kronecker delta: δ^{μ₁...μₙ}_{ν₁...νₙ} = det (δ[μᵢ, νⱼ]).

This is defined for any finite type α with decidable equality.

def generalizedKroneckerDelta {α ι : Type} [DecidableEq α]
    [DecidableEq ι] [Fintype ι]
    (μ : ι → α) (ν : ι → α) : ℤ :=
  Matrix.det (fun i j => δℤ (μ i) (ν j))

Swapping two of the upper indices of the generalized Kronecker delta negates it. This is one row transposition of the underlying determinant.


lemma generalizedKroneckerDelta_swap {α ι : Type} [DecidableEq α] [DecidableEq ι] [Fintype ι]
    (μ ν : ι → α) {i j : ι} (hij : i ≠ j) :
    generalizedKroneckerDelta (μ ∘ Equiv.swap i j) ν = - generalizedKroneckerDelta μ ν := byα:Typeι:Typeinst✝²:DecidableEq αinst✝¹:DecidableEq ιinst✝:Fintype ιμ:ι → αν:ι → αi:ιj:ιhij:i ≠ j⊢ generalizedKroneckerDelta (μ ∘ ⇑(Equiv.swap i j)) ν = -generalizedKroneckerDelta μ ν
  rw [show generalizedKroneckerDelta (μ ∘ Equiv.swap i j) ν
        = (Matrix.submatrix (fun a b => ((kroneckerDelta (μ a) (ν b) : ℕ) : ℤ))
            (Equiv.swap i j) id).det from rfl,α:Typeι:Typeinst✝²:DecidableEq αinst✝¹:DecidableEq ιinst✝:Fintype ιμ:ι → αν:ι → αi:ιj:ιhij:i ≠ j⊢ (submatrix (fun a b => ↑δ[μ a,ν b]) (⇑(Equiv.swap i j)) id).det = -generalizedKroneckerDelta μ να:Typeι:Typeinst✝²:DecidableEq αinst✝¹:DecidableEq ιinst✝:Fintype ιμ:ι → αν:ι → αi:ιj:ιhij:i ≠ j⊢ (↑↑(-1) * det fun a b => ↑δ[μ a,ν b]) = -generalizedKroneckerDelta μ ν
    Matrix.det_permute,α:Typeι:Typeinst✝²:DecidableEq αinst✝¹:DecidableEq ιinst✝:Fintype ιμ:ι → αν:ι → αi:ιj:ιhij:i ≠ j⊢ (↑↑(Equiv.Perm.sign (Equiv.swap i j)) * det fun a b => ↑δ[μ a,ν b]) = -generalizedKroneckerDelta μ να:Typeι:Typeinst✝²:DecidableEq αinst✝¹:DecidableEq ιinst✝:Fintype ιμ:ι → αν:ι → αi:ιj:ιhij:i ≠ j⊢ (↑↑(-1) * det fun a b => ↑δ[μ a,ν b]) = -generalizedKroneckerDelta μ ν Equiv.Perm.sign_swap hijα:Typeι:Typeinst✝²:DecidableEq αinst✝¹:DecidableEq ιinst✝:Fintype ιμ:ι → αν:ι → αi:ιj:ιhij:i ≠ j⊢ (↑↑(-1) * det fun a b => ↑δ[μ a,ν b]) = -generalizedKroneckerDelta μ να:Typeι:Typeinst✝²:DecidableEq αinst✝¹:DecidableEq ιinst✝:Fintype ιμ:ι → αν:ι → αi:ιj:ιhij:i ≠ j⊢ (↑↑(-1) * det fun a b => ↑δ[μ a,ν b]) = -generalizedKroneckerDelta μ ν]α:Typeι:Typeinst✝²:DecidableEq αinst✝¹:DecidableEq ιinst✝:Fintype ιμ:ι → αν:ι → αi:ιj:ιhij:i ≠ j⊢ (↑↑(-1) * det fun a b => ↑δ[μ a,ν b]) = -generalizedKroneckerDelta μ ν
  simp [generalizedKroneckerDelta]All goals completed! 🐙