kronecker symbol

Stream: maths

[Sebastien Gouezel]

Do we have the kronecker symbol somewhere in mathlib (I mean, δ R i j which is equal to (1 : R) if i = j, and (0 : R) otherwise)?

[Scott Morrison]

Pretty sure not. I was tempted to introduce it once but didn't have the enthusiasm to use it everywhere it could be.

[Sebastien Gouezel]

I am doing some elementary linear algebra with matrices, and it would prove pretty useful there!

[Scott Morrison]

I think it's a great idea.

[Scott Morrison]

If we had square brackets to spare I'd love if we could just write [P] for if P then 1 else 0, and then write [i = j] for the Kronecker delta. Maybe that's too hard notationally.

[Scott Morrison]

But I would happily endorse introducing it somewhere, and leaving it to later to use in the rest of the library.

[Anne Baanen]

It's sometimes spelled using docs#function.update, δ i j = function.update 0 i 1 j

[Scott Morrison]

Terse, but not super readable. :-)

[Eric Rodriguez]

I feel like if anything it could just be notation for ite, because there's enough API there

[Anne Baanen]

Or even docs#pi.single i 1 j, apparently

[Utensil Song]

After reading this topic, I'm confused that I couldn't make any of the following #mwe work in Lean 4:

import Mathlib

variable (I : Type*) [DecidableEq I] (R : Type*) [Zero R] [One R]

/-
invalid universe level, ?u.2023 is not greater than 0
-/
def δ (i j : I) : R := Function.update 0 i 1 j


/-
type mismatch
  Pi.single i 1 j
has type
  ?m.213 j : Type ?u.210
but is expected to have type
  R : Type u_2
-/
def δ' (i j : I) : R := Pi.single i 1 j

def mapToOne : I → R := 1

/-
type mismatch
  Pi.single i ?m.2610 j
has type
  ?m.2582 j : Type ?u.2579
but is expected to have type
  R : Type u_2
-/
def δ'' (i j : I) : R := Pi.single i mapToOne j

[Utensil Song]

Signatures like [(i : I) → Zero (f i)] confuses me, I don't know how to make it happy.

[Vincent Beffara]

It is also Set.indicator {i} 1 j

[Utensil Song]

Vincent Beffara said:

It is also Set.indicator {i} 1 j

Thanks, I'm getting this, but in this case one expects a computable version?

/-
failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Set.indicator', and it does not have executable code
-/
def δ''' (i j : I) : R := Set.indicator {i} 1 j

[Utensil Song]

The solution doesn't generalize to the generalized Kronecker delta too.

[Eric Wieser]

This works:

def δ (i j : I) : R := Pi.single (f := fun _ => R) i (1 : R) j

[Eric Wieser]

As does

def δ (i j : I) : R := (Pi.single i 1 : _ → R) j

[Utensil Song]

Ah, thanks, the fix seems to be in a similar spirit as this topic.