Basis dependence

Stream: new members

[Nicolò Cavalleri]

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]

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

[Anne Baanen]

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

[Anne Baanen]

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]

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

[Anne Baanen]

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]

This is all about actual computations, not reasoning.

[Anne Baanen]

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]

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]

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]

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]

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]

@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]

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]

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

[Nicolò Cavalleri]

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]

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]

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]

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]

Right, in this example it is both