Working with basis and linear transforms

Stream: new members

[David Chanin]

I'm going through the book "Linear Algebra Done Right", and thought I'd try to do some of the proof exercises from the book in Lean. I'm really struggling to understand how to deal with linear transforms and basis of vector spaces in lean. The proof I'm trying to write is of the following statement:

Suppose V and W are finite-dimensional and T is a linear transform from V to W.
Show that with respect to each choice of bases of V and W, the matrix of
T has at least dim range T nonzero entries.

I'm able to express V and W in Lean as the following, based on what I found in a Xena lecture on Youtube:

import linear_algebra.finite_dimensional

variables {K: Type} [field K]
variables {V: Type} [add_comm_group V] [module K V] [finite_dimensional K V]
variables {W: Type} [add_comm_group W] [module K W] [finite_dimensional K W]

What I'm struggling to express is the idea of a Linear Transform T which maps from V to W, and how to write the basis of V and W. And then how to express the idea of the range of T in Lean. I see there's linear_algebra/basis.lean, and there's linear_algebra/basic.lean which mentions linear maps, but in a syntax I can't follow. I can't figure out how to use the concepts in these files though - are there examples somewhere of how to work with Linear Transforms and Basis of vector spaces in Lean?

[Anne Baanen]

A linear transform is called docs#linear_map in Mathlib, and a K-linear transform is written (T : V →ₗ[K] W). You have to indicate which field (ring) it's linear over, because V and W could also be vector spaces over other fields.

[Anne Baanen]

An arbitrary basis of V is written as {ι : Type*} (b : basis ι K V). To choose a fixed, but unkown, basis for a vector space, use docs#basis.of_vector_space.

[Anne Baanen]

More specifically, basis ι K V is the type of all #ι-dimensional bases for the K-vector space V, where #ι is the cardinality of ι. So basis (fin 4) K V is the type of all 4-dimensional bases.

[David Chanin]

Aah thank you so much! I tried adding the following 2 lines:

variables (T : V →ₗ[K] W)
variables {bV: Type} [basis.of_vector_space K V]

The T definition seems to not give an error, but variables {bV: Type} [basis.of_vector_space K V] gives the following error:

invalid type ascription, term has type
  basis ↥(basis.of_vector_space_index K V) K V : Type
but is expected to have type
  Sort ? : Type ?

I don't understand what this means. Apologies I'm sure this is an extremely basic misunderstanding on my part!

[Riccardo Brasca]

What do you want to say with variables {bV: Type} [basis.of_vector_space K V]? Do you want to fix a basis?

[David Chanin]

I want to say "bv is a basis of V"

[Riccardo Brasca]

So you need to say variables (bv : basis (basis.of_vector_space_index K V) K V))

[Eric Wieser]

or just (bv : basis I K V)

[Eric Wieser]

No need to specify that it's one particular arbitrary index set

[Riccardo Brasca]

Oh sure, that's even better. basis I K V is the type (read set) of K-basis of V indexed by I (you need to introduce (I : Type*) before naming it).

[Riccardo Brasca]

Note that in mathlib basis have this index set, that is usually irrelevant in math. You can have a basis indexed the set {1,2,3} and a basis indexed by {a,b,c} (this is not precise, basis are indexed by types, but still), and even if the two basis "choose" the same elements of V, they're different.

[David Chanin]

Amazing! Thank you so much! That worked! I don't think I would have ever come up with that on my own :sweat_smile:

[Riccardo Brasca]

This is because we usually think that a basis is a set, but this is incorrect, since then we order the elements to build the matrix. Also, at least in principle, we allow repetitions (as in the exercise "the set {v, v}" is not linear independent since v-v = 0 is a non trivial linear combination equals to 0). The way this idea is formalized is that a basis is a function b : ι → V for some index type ι. Usually only its cardinality matters, but technically it is there.

[Kevin Buzzard]

David Chanin said:

Amazing! Thank you so much! That worked! I don't think I would have ever come up with that on my own :sweat_smile:

This is the way of things at the beginning. Even after I'd done 50 undergraduate problem sheet questions there were still plenty of problems where I couldn't even write down the question properly. Everything works, you just have to get the hang of the way mathlib thinks about mathematics.

[David Chanin]

Kevin Buzzard said:

David Chanin said:

Amazing! Thank you so much! That worked! I don't think I would have ever come up with that on my own :sweat_smile:

This is the way of things at the beginning. Even after I'd done 50 undergraduate problem sheet questions there were still plenty of problems where I couldn't even write down the question properly. Everything works, you just have to get the hang of the way mathlib thinks about mathematics.

That's encouraging to hear! I went through the natural number game and can do some basic proofs, but trying to prove things in the wild still feels really challenging

[David Chanin]

I'm struggling now to express the idea of "the matrix of T has at least dim range T nonzero entries". I think this really boils down to the idea that T(x) can be expressed as a sum of the T(coeffients * basis_of_v), and there should be at least dim range T non-zero coefficients in that equation. Is there a way I can express that T can be expressed be as ∑ a_i* T(basis_of_v_i), so that at least dim range T of those a_i must be non-zero?

[Yakov Pechersky]

Do you a linear_map? If so, you can make a matrix out of it, given a basis. Then you can form a multiset of the values in the matrix. And then you can say that dim range T <= multiset.card s - multiset.count s 0.

[David Chanin]

I have the following setup so far:

variables {K: Type} [field K]
variables {V: Type} [add_comm_group V] [module K V] [finite_dimensional K V]
variables {W: Type} [add_comm_group W] [module K W] [finite_dimensional K W]
variables {I : Type*}

variables (T : V →ₗ[K] W)
variables (bv : basis I K V)
variables (bw : basis I K W)

So, T is a linear map (I think), and bv and bw are bases. How can I form a matrix from T given bv?

[Yakov Pechersky]

The guessable name docs#linear_map.to_matrix

[David Chanin]

Apologies this is probably really obvious, but I can't seem to get that function to work. I'm trying the following:

variable T_matrix : linear_map.to_matrix bv bw T

[David Chanin]

In the docs it seems like it takes 2 bases and the linear map, but this seems like the wrong inputs

[Yakov Pechersky]

At this point, linear_map.to_matrix bv bw is a term, not a type

[David Chanin]

Does that mean I can't use variable to name this?

[Yakov Pechersky]

so you wouldn't say you have a variable of this type. you could have:

example (T_matrix : matrix V W) (h : T_matrix = linear_map.to_matrix bv bw T) : T_matrix  = T.to_matrix bv bw := h

There, I am using dot-notation to have a cleaner statement

[David Chanin]

ooh interesting. Hrm this is giving an error as well,

type expected at
  matrix V W
term has type
  Type ? → Type ?

[David Chanin]

The full code is:

import tactic
import linear_algebra.finite_dimensional
import linear_algebra.matrix.to_lin
import linear_algebra.matrix

variables {K: Type} [field K]
variables {V: Type} [add_comm_group V] [module K V] [finite_dimensional K V]
variables {W: Type} [add_comm_group W] [module K W] [finite_dimensional K W]
variables {I : Type*}

variables (T : V →ₗ[K] W)
variables (bv : basis I K V)
variables (bw : basis I K W)

example
  (T_matrix : matrix V W)
  (h : T_matrix = linear_map.to_matrix bv bw T)
:
  T_matrix = T.to_matrix bv bw
:=
  h

[Yakov Pechersky]

Ah, sorry. I was wrong about the syntax here.

[Yakov Pechersky]

This works

import tactic
import linear_algebra.finite_dimensional
import linear_algebra.matrix.to_lin
import linear_algebra.matrix

variables {K: Type} [field K]
variables {V: Type} [add_comm_group V] [module K V] [finite_dimensional K V]
variables {W: Type} [add_comm_group W] [module K W] [finite_dimensional K W]
variables {I : Type*}

variables (T : V →ₗ[K] W)
variables (bv : basis I K V)
variables (bw : basis I K W)

example
  [decidable_eq I]
  [fintype I]
  (T_matrix : matrix I I K)
  (h : T_matrix = linear_map.to_matrix bv bw T)
:
  T_matrix = linear_map.to_matrix bv bw T
:=
  h

[Yakov Pechersky]

So I couldn't get dot-notation working here. And I was missing the base ring argument of the matrix term, that was the error. And also I was confused about how to specify it -- I needed to give the indexing type. Then, I got errors about missing instances -- linear_map.to_matrix only really works on indexing types that can be finitely and distinctly enumerated, which is what [decidable_eq I] [fintype I] do.

[David Chanin]

I see so I refers to the length of the basis, so if I use the same I that means that both V and W are the same size space

[David Chanin]

How did you figure all of that out?

[Yakov Pechersky]

Going back to your original question about why variables T_matrix : linear_map.to_matrix ..., variables just means "let us have an x \mem X" in regular math speak

[Yakov Pechersky]

You are the one that said that both V and W are the same size space here:

variables (bv : basis I K V)
variables (bw : basis I K W)

[Yakov Pechersky]

You're saying there "I have this data package I will call bv, which is a set of vectors indexed by I that is a basis for the vector space V over the base field K"

[Yakov Pechersky]

Similarly for bw, W. So you can have two different I, I_prime to generalize.

[David Chanin]

That makes sense - I just updated the code to the following to fix that:

variables {Vi : Type*} [fintype Vi] [decidable_eq Vi]
variables {Wi : Type*} [fintype Wi] [decidable_eq Wi]

variables (T : V →ₗ[K] W)
variables (bv : basis Vi K V)
variables (bw : basis Wi K W)

example
  (T_matrix : matrix Wi Vi K)
  (h : T_matrix = linear_map.to_matrix bv bw T)
:
  T_matrix = linear_map.to_matrix bv bw T
:=
  h

[David Chanin]

hrm maybe this proof is too advanced for me. I'm still struggle to even write out the thing that I'm trying to prove :face_palm: . I think I want something like the following:

example
  (T_matrix : matrix Wi Vi K)
  (h : T_matrix = linear_map.to_matrix bv bw T)
:
  /- number of non-zero entries in T_matrix -/ ≤ finrank K T.range
:=
  sorry

[Yakov Pechersky]

If you were programming, how you would get the entries of a matrix?

[David Chanin]

I'd loop over the indices of the matrix

[Yakov Pechersky]

Great, so how would it look like explicitly here? If you can write it out, we can translate it to lean

[David Chanin]

or do something like (mat != 0).sum()

[David Chanin]

Using nested for-loops, it would be something like:

total_non_zero = 0
for i in len(mat):
  row = mat[i]
  for j in len(row[i]):
    if row[j] != 0:
      total_non_zero += 1

[Yakov Pechersky]

OK, so here, we're going to express it as a map. Really, a map of maps

[David Chanin]

I see a matrix.map function. Is that the correct thing to use?

[David Chanin]

Something like mat.map(elm -> elm == 0 ? 0 : 1) and then sum it somehow?

[Yakov Pechersky]

import tactic
import linear_algebra.finite_dimensional
import linear_algebra.fin
import linear_algebra.matrix.to_lin
import linear_algebra.matrix

variables {K: Type} [field K]
variables {V: Type} [add_comm_group V] [module K V] [finite_dimensional K V]
variables {W: Type} [add_comm_group W] [module K W] [finite_dimensional K W]

variables {Vi : Type*} [fintype Vi] [decidable_eq Vi]
variables {Wi : Type*} [fintype Wi] [decidable_eq Wi]

variables (T : V →ₗ[K] W)
variables (bv : basis Vi K V)
variables (bw : basis Wi K W)

noncomputable def values : multiset K :=
(finset.product (finset.univ : finset Vi) (finset.univ : finset Wi)).val.map
  (λ p, linear_map.to_matrix bv bw T p.2 p.1)

lemma target [decidable_eq K] :
  set.finrank K (T.range : set W) ≤ (values T bv bw).card - ((values T bv bw).count 0) :=
sorry

[Yakov Pechersky]

Yeah you could also do that

[David Chanin]

what does it mean to be noncomputable?

[Yakov Pechersky]

We don't have a matrix.sum, so even if we mapped the matrix, the count (which would be the sum), would require something similar

[David Chanin]

aah so I just need to prove the target lemma then!

[Yakov Pechersky]

noncomputable here just means that it does not generate VM code to execute this definition. That is because the linear_map.to_matrix construction is a axiom-of-choice-based construction

[David Chanin]

OK, at least that's something for me to start with

[David Chanin]

I see, if I delete "noncomputable" it says I need to add it back , so at least I can't ever forget to write that if it's needed

[Yakov Pechersky]

It's axiom-of-choice, because, consider an arbitrary distinct finite set that indexes our matrix. Sure, but in what order? The order of the indexing doesn't matter for it being a linear map. But you have to choose _some_ order for the matrix to actually exist.

[Yakov Pechersky]

That's not the full story, but it's close enough

[David Chanin]

Does that mean you can write theorems about matrices, but can never actually instantiate a specific matrix and run a computation with it?

[David Chanin]

like, I could never create the matrix [1 2; 3 4] and then compute the determinant or something?

[Yakov Pechersky]

Oh, you definitely can:

import data.matrix.notation
def M : matrix (fin 2) (fin 2) ℕ := !![1, 2; 3, 4]

#eval M 1 1 -- 4

[Yakov Pechersky]

But in lean, there are different modes of computation. There is the kernel, the VM, and also tactic based. Like this is tactic based from test/matrix.lean.

example {α : Type*} [comm_ring α] {a b c d e f g h i : α} :
  matrix.det !![a, b, c; d, e, f; g, h, i] =
    a * e * i - a * f * h - b * d * i + b * f * g + c * d * h - c * e * g :=
begin
  simp [matrix.det_succ_row_zero, fin.sum_univ_succ],
  /-
  Try this: simp only [det_succ_row_zero, fin.sum_univ_succ, neg_mul, cons_append,
  mul_one, fin.default_eq_zero, fin.coe_zero, cons_vec_bit0_eq_alt0, one_mul, cons_val_one,
  cons_vec_alt0, fin.succ_succ_above_one, fin.coe_succ, univ_unique, minor_apply, pow_one,
  fin.zero_succ_above, fin.succ_zero_eq_one, fin.succ_succ_above_zero, nat.neg_one_sq,
  finset.sum_singleton, cons_val_zero, cons_val_succ, det_fin_zero, head_cons, pow_zero]
   -/
  ring
end

[Yakov Pechersky]

Note, the #eval example had concrete explicit types. In the det example, I "computed" the determinant on an arbitrary type of values.

[Yakov Pechersky]

And yes, one can compute the det:

import data.matrix.notation
import linear_algebra.matrix.determinant
def M : matrix (fin 2) (fin 2) ℤ := !![1, 2; 3, 4]

#eval M.det -- -2

[David Chanin]

Seeing this is really helpful

[David Chanin]

Thank you so much for taking the time to walk me through all of this stuff!

[Yakov Pechersky]

Sure thing! My first foray into mathlib was also trying to prove stuff about matrices and determinants

[Yakov Pechersky]

That 3x3 determinant example was one of my first pushes to get all the lemmas in place and make simp; ring be able to solve it

[David Chanin]

ooh excellent - is any of that online? I didn't see a lot of examples of proving linear algebra stuff online

[Yakov Pechersky]

I kinda abandoned it, but you could look at https://github.com/pechersky/e222/tree/master/src

[Yakov Pechersky]

There are other people working on formalizing Axler

[Yakov Pechersky]

Here's another example of "computation": https://github.com/pechersky/e222/blob/master/src/problems02.lean#L49-L58

[Yakov Pechersky]

It's not only computing that these two matrices are the same, but also computing a proof certificate of that, that's via the norm_num tactic.

[David Chanin]

ah great, I'll take a look at these!

[Yakov Pechersky]

And here's the "proof-by-brute-force version":

import data.matrix.notation
import linear_algebra.matrix.determinant
def M : matrix (fin 2) (fin 2) ℤ := !![1, 2; 3, 4]

#eval M.det -- -2

example : M.det = -2 := by dec_trivial

[Yakov Pechersky]

Watch how a tiny change breaks the "proof-by-force":

import data.matrix.notation
import linear_algebra.matrix.determinant
def M : matrix (fin 2) (fin 2) ℚ := !![1, 2; 3, 4]

#eval M.det -- -2

example : M.det = -2 := by dec_trivial -- no longer works

[Yakov Pechersky]

So instead, "proof-by-tactic":

import data.matrix.notation
import linear_algebra.matrix.determinant
def M : matrix (fin 2) (fin 2) ℚ := !![1, 2; 3, 4]

#eval M.det -- -2

example : M.det = -2 := by norm_num [matrix.det_fin_two, M]

[Yakov Pechersky]

And yet another change:

import data.matrix.notation
import linear_algebra.matrix.determinant
import data.real.basic

def M : matrix (fin 2) (fin 2) ℝ := !![1, 2; 3, 4]

#eval M.det -- uhhh, what?? it's showing underlying impl, not 2

example : M.det = -2 := by norm_num [matrix.det_fin_two, M]

[David Chanin]

I can't get these examples to run, it doesn't seem to like the !![1, 2; 3, 4] syntax in Lean for me

[Yakov Pechersky]

Do you have data.matrix.notation imported? What mathlib commit are you on?

[Yakov Pechersky]

I am on current master, or maybe 13 commits behind

[David Chanin]

Mine is 16 days old, let me try updating...

[David Chanin]

oh yeah it works now! strange

[Yakov Pechersky]

It was a recent PR

[David Chanin]

Yakov Pechersky said:

And yet another change:

import data.matrix.notation
import linear_algebra.matrix.determinant
import data.real.basic

def M : matrix (fin 2) (fin 2) ℝ := !![1, 2; 3, 4]

#eval M.det -- uhhh, what?? it's showing underlying impl, not 2

example : M.det = -2 := by norm_num [matrix.det_fin_two, M]

whoa why does the #eval break so hard with real numbers? Stuff only works correctly on integers?

[Ruben Van de Velde]

Reals are equivalence classes of Cauchy sequences of rational numbers - it's not so obvious to compute with those

[Yaël Dillies]

It's not obvious what it even means to print out a real!

[David Chanin]

🤯 math is hard

[Eric Wieser]

@Yakov Pechersky, docs#linear_map.to_matrix uses choice for totally silly reasons (in order to state that a basis is a linear map to coordinates), the actual data is computed without it.

[Eric Wieser]

But you have to choose _some_ order for the matrix to actually exist.

Not true, docs#matrix and even docs#matrix.det requires no order

[Eric Wieser]

@Yaël Dillies, I was planning a PR such that reals that are coerced naturals have a reasonable repr

[Yakov Pechersky]

Sorry for the FUD. What's the silly reason for that basis issue?

[Eric Wieser]

docs#finsupp.has_add

[Eric Wieser]

To avoid earning a :butterfly:; by "totally silly" I mean "not mathematical" as opposed to "this was a bad design decision".

[Eric Wieser]

As a tip: you can hover over the word "noncomputable" in the docs to see why something is noncomputable

[Yaël Dillies]

Eric Wieser said:

Yaël Dillies, I was planning a PR such that reals that are coerced naturals have a reasonable repr

And fractions too?

[Anne Baanen]

Yaël Dillies said:

Eric Wieser said:

Yaël Dillies, I was planning a PR such that reals that are coerced naturals have a reasonable repr

And fractions too?

Currently not possible, but should be doable after #14894.