Using matrix notation and calculation

Stream: new members

[Yakov Pechersky]

Trying to use the matrix.notation to do some calculation, but am having issues doing simple transformations on scalar \bu matrix. I had to write a new lemma that I think wasn't in data.matrix.notation to get the smul to even partially work. Looks like the current issue is that matrix.vec_empty isn't being inferred as the correct type. Am I misunderstanding something about the notation?

import data.real.basic
import data.matrix.notation
import tactic.fin_cases

universe u
variables {α : Type u} [semiring α]
variables {m n : ℕ} {m' n' : Type} [fintype m'] [fintype n']

@[simp] lemma smul_cons_cons (x : α) (v : n' → α) (A : matrix (fin m) n' α) :
  x • matrix.vec_cons v A = matrix.vec_cons (x • v) (x • A) :=
by { ext i, refine fin.cases _ _ i; simp }

example (x : ℝ) (A B : matrix (fin 1) (fin 1) ℝ) (hx : x = 2)
        (hA : A = ![![1]]) (hB : B = ![![2]]) :
        x • A = B :=
begin
  rw [hx, hA, hB],
  simp only [mul_one, smul_cons_cons, matrix.smul_cons, matrix.smul_empty], -- does not solve goal
  -- ⊢ matrix.vec_cons ![2] (2 • matrix.vec_empty) = ![![2]]
end

[Kenny Lau]

that's (2 : ℝ) • (@matrix.vec_empty (fin 1 → ℝ) : fin 0 → fin 1 → ℝ)

[Yakov Pechersky]

Do you mean that I did not notate my matrix properly?

[Kenny Lau]

I mean, the reason the goal has that 2 • matrix.vec_empty term is because that's (2 : ℝ) • (@matrix.vec_empty (fin 1 → ℝ) : fin 0 → fin 1 → ℝ)

[Kenny Lau]

so naturally matrix.smul_empty cannot solve that

[Kenny Lau]

you would need another simp lemma

[Kenny Lau]

import data.real.basic
import data.matrix.notation
import tactic.fin_cases

universe u
variables {α : Type u} [semiring α]
variables {m n : ℕ} {m' n' : Type} [fintype m'] [fintype n']

@[simp] lemma smul_cons_cons (x : α) (v : n' → α) (A : matrix (fin m) n' α) :
  x • matrix.vec_cons v A = matrix.vec_cons (x • v) (x • A) :=
by { ext i, refine fin.cases _ _ i; simp }

@[simp] lemma matrix.smul_empty' (x : α) : x • @matrix.vec_empty (m' → α) = matrix.vec_empty :=
matrix.ext $ λ i, fin.elim0 i

example (x : ℝ) (A B : matrix (fin 1) (fin 1) ℝ) (hx : x = 2)
        (hA : A = ![![1]]) (hB : B = ![![2]]) :
        x • A = B :=
begin
  rw [hx, hA, hB],
  simp only [mul_one, smul_cons_cons, matrix.smul_cons, matrix.smul_empty, matrix.smul_empty']
end

[Kenny Lau]

like this

[Yakov Pechersky]

Gotcha. I guess I can write another for matrices

[Yakov Pechersky]

Ah there it is. Would there be a way to write one single one for n-dim tensors as opposed to just what we have now for 1- and 2-dim?

[Kenny Lau]

no.

[Kenny Lau]

is there any theorem about n-dim tensors?

[Yakov Pechersky]

Not at the moment I don't think

[Yakov Pechersky]

Thanks for the insights here. I'll PR these two lemmas in, maybe I'll find some more on the way.

[Kenny Lau]

unless you invent a new notation for n-dim tensors (maybe using list), this wouldn't be possible

[Yakov Pechersky]

why wouldn't ![ ![ ![1] ] ] indicate a 1x1x1 tensor?

[Kenny Lau]

it will, but you can't say "forall n, ![![![... ( n times ) 1]]]"

[Kenny Lau]

because "... (n times)" isn't Lean

[Patrick Massot]

Yakov, I haven't been reading that thread, but I see you're doing linear algebra and matrices. If you don't know what to do next, then I suggest defining the determinant of a family of vectors with respect to a basis. This hole in mathlib is annoying for the sphere eversion project.

[Kenny Lau]

why isn't this just determinant?

[Kenny Lau]

aha you want to take determinant of a function \io \to M w.r.t. some basis \io \to M

[Yakov Pechersky]

Do you mean just finite dimensional \io -> M or functional determinants?

[Yakov Pechersky]

Regarding the tensor notation, I just meant a lemma that wasn't just for (x : α) : x • @matrix.vec_empty (m' → α) but for (x : α) : x • @matrix.vec_empty ( ... → ... → ... → α)

[Kenny Lau]

yes, and I'm saying there is no way to state it.

[Yakov Pechersky]

Got it.

[Patrick Massot]

I meant finite dimensional.

[Kenny Lau]

Kenny Lau said:

aha you want to take determinant of a function \io \to M w.r.t. some basis \io \to M

where \io is a fintype

[Patrick Massot]

Yes.

[Yakov Pechersky]

Something like this? Would your family of vectors be a finset? I might have the indices swapped here.

import linear_algebra.basis
import linear_algebra.determinant

variables {ι : Type*} {R : Type*} {M : Type*}
variables {v : ι → M}
variables [fintype ι] [decidable_eq ι]
variables [comm_ring R] [add_comm_group M] [module R M]
variables (hv : is_basis R v)

#check matrix.det (λ i j, is_basis.repr hv (v i) j)

[Patrick Massot]

Unless I'm misreading, you defined the number 1. You need a second family of vectors. And also note the actual work is to build a nice set of lemmas allowing to use it. For instance say v is your basis and w is your family of vectors, you want to know that w is a basis iff the determinant of w with respect to v is invertible.

[Patrick Massot]

Also note that I don't know what works over any commutative ring, even if you assume your module has a basis.

[Patrick Massot]

I would need to look it up in Bourbaki.

[Patrick Massot]

Also, you should think about using Sébastien's multilinear map stuff to get free lemmas.

[Patrick Massot]

https://leanprover-community.github.io/mathlib_docs/linear_algebra/multilinear.html#multilinear_map

[Kevin Buzzard]

Here's my guess as to what it looks like. If you have two maps from a fintype \i of size n to any torsion-free R-module M (R any commutative ring) and the image of the second is contained in the span of the image of the first, then there will be a well defined determinant, because in the nth wedge power of M the wedge power of the second will be a unique R-multiple of the nth wedge power of the first. There will be some id, symm and comp lemmas. If you drop the torsion free assumption then there will be some set of elements of R which work -- a coset of an ideal -- so it will be a predicate on R and there will be analogous symm and comp lemmas.

[Kevin Buzzard]

I don't think you need anything to be a basis of anything. Maybe a development of wedge powers is what's needed

[Patrick Massot]

Of course the proper way to do determinant would be develop exterior powers. That's why I wrote I was a bit sad to see people working towards an elementary proof of Cayley-Hamilton a couple of weeks ago. But having an elementary theory of determinants is better than nothing.

[Reid Barton]

Kenny Lau said:

is there any theorem about n-dim tensors?

There is some stuff like this under a non-math name I don't remember.

[Reid Barton]

holor

[Rob Lewis]

IIRC Alex originally used the name "tensor" and the mathematicians forced him to change it to "holor."

[Kenny Lau]

Etymology
Coined by Parry Hiram Moon, and ‎Domina Eberle Spencer, from holo- (“whole”).

Noun
holor (plural holors)

(mathematics) A mathematical entity made up of one or more independent quantities, or merates, as distinguished from a tensor.

[Yakov Pechersky]

Do you think it is worth restating matrix.notation defns and lemmas in terms of holor? Right now, with regards to the questions about arbitrary n-dim structures, I'm experimenting with something like:

import data.fintype.card
import data.matrix.basic
import tactic.fin_cases

namespace matrix

universe u
variables {α : Type u}

open_locale matrix

section matrix_notation
variables {ι : Type} [fintype ι]

def vec_empty : (fin 0 × ι) → α :=
λ ⟨n, i⟩, fin_zero_elim n

def vec_cons {n : ℕ} (h : ι → α) (t : (fin n × ι) → α) : (fin n.succ × ι) → α :=
λ ⟨⟨ni, hni⟩, mi⟩, dite (ni < n) (λ hn, t ⟨⟨ni, hn⟩, mi⟩) (λ _, h mi)

notation `![` l:(foldr `, ` (h t, vec_cons h t) vec_empty `]`) := l

def vec_head {n : ℕ} (v : (fin n.succ × ι) → α) : ι -> α :=
λ i, v ⟨⟨0, nat.succ_pos'⟩, i⟩

def vec_tail {n : ℕ} (v : (fin n.succ × ι) → α) : (fin n × ι) → α :=
λ ⟨⟨k, hn⟩, i⟩, v ⟨⟨k.succ, nat.succ_lt_succ hn⟩, i⟩

end matrix_notation