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.SchurComplement

Contraction identities for the generalized Kronecker delta

i. Overview

This file proves the combinatorial contraction facts for the generalizedKroneckerDelta (defined in Physlib.Mathematics.KroneckerDelta.Basic). Everything here is purely about the abstract generalized Kronecker delta on a finite type; no tensor or physics content appears. These facts are the reusable backbone of the Levi-Civita epsilon-epsilon contraction identities proved in Physlib.Relativity.Tensors.LeviCivita.Contractions.

The central fact is that summing a generalizedKroneckerDelta over one shared index lowers its rank by one and multiplies it by card α - n (generalizedKroneckerDelta_sum_snoc). Iterating that fact, together with the product identity generalizedKroneckerDelta μ ν = generalizedKroneckerDelta μ id * generalizedKroneckerDelta ν id (generalizedKroneckerDelta_mul), gives the fully-, singly-, and doubly-free contractions sum_generalizedKroneckerDelta_self, sum_generalizedKroneckerDelta_cons, and sum_generalizedKroneckerDelta_cons₂ over Fin 4.

The proof of generalizedKroneckerDelta_sum_snoc borders the delta matrix with the appended index (a Schur-complement reduction) and then applies the ring-general rank-one determinant update lemma Matrix.det_add_rankOne, which is proved here because Mathlib only provides the matrix determinant lemma when det A is a unit and Kronecker-delta matrices are singular.

ii. Key results

    generalizedKroneckerDelta_sum_snoc : summing over one shared index lowers the rank by one.

    sum_generalizedKroneckerDelta_mul_self, sum_generalizedKroneckerDelta_mul_cons, sum_generalizedKroneckerDelta_mul_cons₂ : the fully-, singly-, and doubly-free symbol-level contractions over Fin 4.

iii. Table of contents

    A. The rank-one determinant update

    B. Contraction identities

iv. References

@[expose] public section

A. The rank-one determinant update

Expanding the determinant of a rank-one row update over a finite set of rows. For i ∈ s the row A i is replaced by A i + w i • b; the other rows are untouched.

ι:Type u_1inst✝²:DecidableEq ιinst✝¹:Fintype ιR:Type u_2inst✝:CommRing RA:Matrix ι ι Rw:ι Rb:ι Ri₀:ιs:Finset ιhi₀:i₀ sMs:Matrix ι ι R := A + of fun i j => (if i s then w i else 0) * b jih:Ms.det = A.det + i s, w i * (A.updateRow i b).dethMs:Ms = A + of fun i j => (if i s then w i else 0) * b jhrow:Ms i₀ = A i₀key:(A + of fun i j => (if i insert i₀ s then w i else 0) * b j) = Ms.updateRow i₀ (A i₀ + w i₀ b)h1:(Ms.updateRow i₀ (A i₀)).det = Ms.deth2:(Ms.updateRow i₀ b).det = (A.updateRow i₀ b).detA.det + i s, w i * (A.updateRow i b).det + w i₀ * (A.updateRow i₀ b).det = A.det + (w i₀ * (A.updateRow i₀ b).det + x s, w x * (A.updateRow x b).det) All goals completed! 🐙

Rank-one determinant update (the ring-general matrix determinant lemma for an outer product, valid even when A is singular). Adding the rank-one matrix w ⊗ b to A changes the determinant by ∑ i, w i * det (A.updateRow i b).

Mathlib only provides this when det A is a unit (Matrix.det_add_replicateCol_mul_replicateRow); the singular case is needed here because Kronecker-delta matrices are typically singular.

private lemma det_add_rankOne {ι : Type*} [DecidableEq ι] [Fintype ι] {R : Type*} [CommRing R] (A : Matrix ι ι R) (w b : ι R) : (A + Matrix.of fun i j => w i * b j).det = A.det + i, w i * (A.updateRow i b).det := ι:Type u_1inst✝²:DecidableEq ιinst✝¹:Fintype ιR:Type u_2inst✝:CommRing RA:Matrix ι ι Rw:ι Rb:ι R(A + of fun i j => w i * b j).det = A.det + i, w i * (A.updateRow i b).det ι:Type u_1inst✝²:DecidableEq ιinst✝¹:Fintype ιR:Type u_2inst✝:CommRing RA:Matrix ι ι Rw:ι Rb:ι Rh:(A + of fun i j => (if i Finset.univ then w i else 0) * b j).det = A.det + i, w i * (A.updateRow i b).det(A + of fun i j => w i * b j).det = A.det + i, w i * (A.updateRow i b).det All goals completed! 🐙

B. Contraction identities

The product of two Levi-Civita-type symbols is a generalized Kronecker delta: δ^{μ}_{·} · δ^{ν}_{·} = δ^{μ}_{ν}, where each single factor is a Kronecker matrix against the identity. This is the Lean form of ε^{μ₁…μₙ} ε_{ν₁…νₙ} = δ^{μ₁…μₙ}_{ν₁…νₙ}.

α:Typeinst✝¹:DecidableEq αinst✝:Fintype αμ:α αν:α αi:αj:α k, δ[μ i,k] * δ[k,ν j] = δ[μ i,ν j] All goals completed! 🐙

Generalized Kronecker delta contraction. Summing a generalizedKroneckerDelta over one shared index appended at the end lowers the rank by one and pulls out a factor of card α - n. This is the reusable combinatorial fact behind all epsilon-epsilon identities.

α:Typeinst✝¹:DecidableEq αinst✝:Fintype αn:μ:Fin n αν:Fin n αA:Matrix (Fin n) (Fin n) := of fun i j => δ[μ i,ν j]hA:A = of fun i j => δ[μ i,ν j]b:α Fin n := fun a j => δ[a,ν j]hb:b = fun a j => δ[a,ν j]key: (a : α), generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a) = A.det - i, δ[μ i,a] * (A.updateRow i (b a)).dethrow: (i : Fin n), a, δ[μ i,a] * (A.updateRow i (b a)).det = A.detFintype.card α A.det - n A.det = ((Fintype.card α) - n) * A.det All goals completed! 🐙

Split a sum over (k+1)-tuples into the last entry and the initial k-tuple.

X:Type u_1inst✝¹:Fintype XM:Type u_2inst✝:AddCommMonoid Mk:F:(Fin (k + 1) X) M y, x, F ((Fin.snocEquiv fun x => X) (x, y)) = h', c, F (Fin.snoc h' c) All goals completed! 🐙

Full contraction. Iterating the snoc contraction over all four indices: ∑_f δ^{f}_{f} = 4!. Here f ranges over all maps Fin 4 → Fin 4.

k:ih: h, generalizedKroneckerDelta h h = j Finset.range k, (4 - j)hstep: (h' : Fin k Fin 4), c, generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c) = (4 - k) * generalizedKroneckerDelta h' h'(4 - k) * j Finset.range k, (4 - j) = (∏ x Finset.range k, (4 - x)) * (4 - k) All goals completed! 🐙

Single contraction. Contracting the last k of k+1 index pairs leaves one free pair σ, τ, with the factorial factor (4-1)(4-2)….

σ:Fin 4τ:Fin 4k:ih: h, generalizedKroneckerDelta (Fin.cons σ h) (Fin.cons τ h) = (∏ j Finset.range k, (3 - j)) * δ[σ,τ]hstep: (h' : Fin k Fin 4), c, generalizedKroneckerDelta (Fin.cons σ (Fin.snoc h' c)) (Fin.cons τ (Fin.snoc h' c)) = (3 - k) * generalizedKroneckerDelta (Fin.cons σ h') (Fin.cons τ h')(3 - k) * ((∏ j Finset.range k, (3 - j)) * δ[σ,τ]) = (∏ x Finset.range k, (3 - x)) * (3 - k) * δ[σ,τ] All goals completed! 🐙

Double contraction. Contracting the last k of k+2 index pairs leaves two free pairs, with value a 2×2 generalized Kronecker delta times the factorial factor.

ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4k:ih: h, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h)) = (∏ j Finset.range k, (2 - j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]hstep: (h' : Fin k Fin 4), c, generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c))) (Fin.cons τ (Fin.cons ω (Fin.snoc h' c))) = (2 - k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h')) (Fin.cons τ (Fin.cons ω h'))(2 - k) * ((∏ j Finset.range k, (2 - j)) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω]) = (∏ x Finset.range k, (2 - x)) * (2 - k) * generalizedKroneckerDelta ![ρ, σ] ![τ, ω] All goals completed! 🐙

Symbol-level full contraction over Fin 4 → Fin 4.

j Finset.range 4, (4 - j) = 24 All goals completed! 🐙

Symbol-level triple contraction, one free pair σ, τ.

σ:Fin 4τ:Fin 4(∏ j Finset.range 3, (3 - j)) * δ[σ,τ] = 6 * δ[σ,τ] All goals completed! 🐙

Symbol-level double contraction, two free pairs.

ρ:Fin 4σ:Fin 4τ:Fin 4ω:Fin 4hdet:generalizedKroneckerDelta ![ρ, σ] ![τ, ω] = δ[ρ,τ] * δ[σ,ω] - δ[ρ,ω] * δ[σ,τ](∏ j Finset.range 2, (2 - j)) * (δ[ρ,τ] * δ[σ,ω] - δ[ρ,ω] * δ[σ,τ]) = 2 * (δ[ρ,τ] * δ[σ,ω] - δ[ρ,ω] * δ[σ,τ]) All goals completed! 🐙