Zulip Chat Archive

Stream: new members

Topic: Basis dependence


Nicolò Cavalleri (Aug 21 2020 at 09:57):

I am trying to understand how to work with linear algebra in Lean. I watched the video by @Anne Baanen and it is mentioned that determinant is defined for matrices because it is easier than for endomorphisms. I wonder what in general is the approach, if there is any, in Lean to define concepts which are defined through bases but do not depend on the specific basis, like the determinant for an endomorphism. Is there a way to tell Lean pick a random basis for a finite dimensional vector space and do things with that, and then prove it does not depend on that basis, or is there maybe a way to register a "standard basis" for a finite vector space (maybe using type class inference?) and work with that? Any comment on this is welcomed!

Nicolò Cavalleri (Aug 21 2020 at 10:01):

(I ask because I did not find any specific implementation of determinant for endomorphisms in Lean)

Anne Baanen (Aug 21 2020 at 10:02):

I guess the current way would be to compose matrix.det with linear_map.to_matrix.

Anne Baanen (Aug 21 2020 at 10:03):

That is also how the trace of a linear map is defined:

/-- The trace of an endomorphism given a basis. -/
def trace_aux (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M]
  {ι : Type w} [decidable_eq ι] [fintype ι] {b : ι  M} (hb : is_basis R b) :
  (M [R] M) [R] R :=
(matrix.trace ι R R).comp $ linear_equiv_matrix hb hb

Nicolò Cavalleri (Aug 21 2020 at 10:06):

Ok what is [decidable_eq \iota] and why do I need such instance?

Anne Baanen (Aug 21 2020 at 10:14):

decidable_eq ι means that given any two i j : ι, there is an algorithm for deciding whether i = j or not. This makes it possible to write out the identity matrix indexed by ι: 1 i j = if i = j then 1 else 0, for example in a tactic that solves a problem by computing with matrices.

Patrick Massot (Aug 21 2020 at 10:15):

This is all about actual computations, not reasoning.

Anne Baanen (Aug 21 2020 at 10:16):

If you want to write proofs, you probably don't care about doing computations, so you can write open_locale classical to automatically get a noncomputable instance of decidable_eq on everything.

Nicolò Cavalleri (Aug 21 2020 at 11:28):

Anne Baanen said:

If you want to write proofs, you probably don't care about doing computations, so you can write open_locale classical to automatically get a noncomputable instance of decidable_eq on everything.

Ok cool thanks this is useful

Nicolò Cavalleri (Aug 21 2020 at 11:31):

As for the definition of the actual trace :

/-- Trace of an endomorphism independent of basis. -/
def trace (R : Type u) [comm_ring R] (M : Type v) [add_comm_group M] [module R M] :
  (M [R] M) [R] R :=
if H :  s : finset M, is_basis R (λ x, x : (s : set M)  M)
then trace_aux R (classical.some_spec H)
else 0

How does lean know that it is not important what base you use? Is it implicit in the classical.some? Why was not this trick used for the determinant as well?

Reid Barton (Aug 21 2020 at 11:59):

Lean does not know that the choice of basis does not matter and from this definition alone you cannot tell.
Maybe there is a separate lemma that says that trace agrees with the trace computed from any provided basis.

Anne Baanen (Aug 21 2020 at 12:14):

Indeed:

theorem trace_eq_matrix_trace (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M]
  {ι : Type w} [fintype ι] {b : ι  M} (hb : is_basis R b) (f : M [R] M) :
  trace R M f = matrix.trace ι R R (linear_equiv_matrix hb hb f) :=

Kevin Buzzard (Aug 21 2020 at 12:40):

@Nicolò Cavalleri Lean makes a random choice of basis, as we do, when making the definition. The definition involves the choice. The theorem that it's independent of the choice is a different object in Lean. Lean's version of the axiom of choice is super-strong. It chooses once and for all, at the beginning of time, an element from each nonempty type, and then we never change those choices.

Reid Barton (Aug 21 2020 at 12:46):

The difference is in math we don't consider something like this to be a definition until we've checked that it is independent of the choices involved.

Reid Barton (Aug 21 2020 at 12:46):

That's how we know it is a sensible notion that behaves as expected under isomorphisms, etc.

Nicolò Cavalleri (Aug 21 2020 at 16:55):

Ok thanks. I cannot really use the lemma that the trace definition use, namely:

lemma exists_is_basis_finset [finite_dimensional K V] :
   b : finset V, is_basis K (coe : (b : set V)  V)

I do not understand what coe is as it is both a Lean operator and a normal function. What is it exactly? I'll try to cook up a mwe in the next message

Nicolò Cavalleri (Aug 21 2020 at 17:05):

What I now explain makes no sense at all mathematically but it is a great simplification of the problem I am trying to solve so don't judge it mathematically haha. Suppose the sum of the components of a vector in a vector space were a well defined number, independent of the basis (this is infacts not that different than the trace but in the case of the trace I do not understand what is going on because there is too many aux definitions). To define the function that implements this fantastic concept, what I'd try to do is

import linear_algebra.finite_dimensional

variables {𝕜 : Type*} [field 𝕜]
{E : Type*} [add_comm_group E] [vector_space 𝕜 E] [finite_dimensional 𝕜 E]

def test (v : E) : 𝕜 :=
begin
  have h := finite_dimensional.exists_is_basis_finset 𝕜 E,
  let b := classical.some h,
  have hb := classical.some_spec h,
  let i := hb.repr,
  let result := finset.sum b (λ w, i v w),
end

This clearly gives an error, I do not expect this to work: it is just to show my intentions. What I'd think is that I should somehow use the function named coe but coe is an operator so I am clearly very confused about what I should do here

Johan Commelin (Aug 21 2020 at 17:09):

import linear_algebra.finite_dimensional

variables {𝕜 : Type*} [field 𝕜]
{E : Type*} [add_comm_group E] [vector_space 𝕜 E] [finite_dimensional 𝕜 E]

open_locale big_operators

def test (v : E) : 𝕜 :=
begin
  have h := finite_dimensional.exists_is_basis_finset 𝕜 E,
  let b := classical.some h,
  have hb := classical.some_spec h,
  let i := hb.repr,
  let result :=  w : (b : set E), i v w,
end

Nicolò Cavalleri (Aug 21 2020 at 17:12):

Ok thanks if I understand correctly b is supposed to be the set of the elements of the basis then not a set of indexes right?

Johan Commelin (Aug 21 2020 at 17:15):

Right, in this example it is both


Last updated: Dec 20 2023 at 11:08 UTC