Rank of a vector space

Stream: Is there code for X?

[Yakov Pechersky]

After the basis refactor, what is the right way to say that the dimension of the vector space of n x n matrices over \R is n x n? Before, I had the following:

variables {n m : ℕ}

-- An n × n matrix has some finite basis of cardinality n ^ 2
example : ∃ (b : finset (matrix (fin n) (fin n) ℝ)),
            (is_basis ℝ (subtype.val : (b : set (MnR n)) → (MnR n)) ∧
            (finset.card b = n ^ 2)) :=
begin
  obtain ⟨s, s_basis⟩ := finite_dimensional.exists_is_basis_finset ℝ (MnR n),
  refine ⟨s, s_basis, _⟩,
  rw [←finite_dimensional.finrank_eq_card_finset_basis s_basis,
      matrix.finrank_matrix, fintype.card, finset.card_fin, pow_two]
end

-- An m × n matrix has some finite basis of cardinality m * n
example : ∃ (b : finset (matrix (fin m) (fin n) ℝ)),
            (is_basis ℝ
              (subtype.val : (b : set (matrix (fin m) (fin n) ℝ)) → (matrix (fin m) (fin n) ℝ)) ∧
            (finset.card b = m * n)) :=
begin
  obtain ⟨s, s_basis⟩ := finite_dimensional.exists_is_basis_finset ℝ (matrix (fin m) (fin n) ℝ),
  refine ⟨s, s_basis, _⟩,
  rw [←finite_dimensional.finrank_eq_card_finset_basis s_basis,
      matrix.finrank_matrix],
  repeat { rw [fintype.card, finset.card_fin] }
end

[Yakov Pechersky]

@Anne Baanen

[Johan Commelin]

@Yakov Pechersky Can't you write findim (matrix (fin m) (fin n) ℝ) = m * n?

[Yakov Pechersky]

Yes, but that doesn't state that there is some finset with finset.card or fintype with fintype.card that could form a basis.

[Johan Commelin]

Hmm, but that's not specific to matrices. So we should prove that as a general lemma.

[Johan Commelin]

If you are finite dimensional:

• Then there exists a finset that is a basis
• Any two bases have the same fintype.card
• Any basis has cardinality findim

[Johan Commelin]

I hope that some of those are already in mathlib, but I haven't used this part much...

[Yakov Pechersky]

Yes, is there such a lemma? My examples above are from an offshoot repo that showcases mathlib with simple undergrad examples

[Kevin Buzzard]

While we're here, what's the right way to say that an add_comm_group $\Lambda$ is finite and free as a $\Z$-module, i.e. isomorphic to $\Z^n$ for some $n\geq0$?

[Johan Commelin]

We need to turn finite_free from LTE into a typeclass predicate on R-modules, and build some API around it.

[Anne Baanen]

Yakov Pechersky said:

Yes, but that doesn't state that there is some finset with finset.card or fintype with fintype.card that could form a basis.

These kinds of results can (still) be found in finite_dimensional.lean. I did have to rename/adapt them slightly, but there should be nothing missing.

So exists_is_basis_finset is now docs#finite_dimensional.finset_basis and docs#finite_dimensional.finrank_eq_card_finset_basis is still the same.

[Anne Baanen]

Johan Commelin said:

If you are finite dimensional:

• Then there exists a finset that is a basis
• Any two bases have the same fintype.card
• Any basis has cardinality findim

• docs#finite_dimensional.finset_basis
• For potentially infinite-dimensional spaces: docs#mk_eq_mk_of_basis (we have that the map from cardinals to naturals is injective for fintypes, right?)
• docs#finite_dimensional.finrank_eq_card_basis and/or docs#finite_dimensional.finrank_eq_card_finset_basis (the latter being useful if your index set is already a finset)

[Anne Baanen]

Kevin Buzzard said:

While we're here, what's the right way to say that an add_comm_group $\Lambda$ is finite and free as a $\Z$-module, i.e. isomorphic to $\Z^n$ for some $n\geq0$?

At the moment you can say something like Σ (n : ℕ), basis (fin n) ℤ Λ like the conclusion for docs#submodule.basis_of_pid.

The finite_free typeclass sounds like a very good idea though!

[Anne Baanen]

Updated examples:

import data.real.basic
import linear_algebra.matrix

variables {n m : ℕ}

abbreviation MnR (n : ℕ) := matrix (fin n) (fin n) ℝ

-- An n × n matrix has some finite basis of cardinality n ^ 2
example : ∃ (s : finset (matrix (fin n) (fin n) ℝ))
            (b : basis ((s : set (MnR n)) : Type*) ℝ (MnR n)), -- Why isn't there a nice coe_to_sort on finset?
            (finset.card s = n ^ 2) :=
begin
  let s_basis := finite_dimensional.finset_basis ℝ (MnR n),
  refine ⟨_, s_basis, _⟩,
  rw [←finite_dimensional.finrank_eq_card_finset_basis s_basis,
      matrix.finrank_matrix, fintype.card, finset.card_fin, pow_two]
end

-- An m × n matrix has some finite basis of cardinality m * n
example : ∃ (s : finset (matrix (fin m) (fin n) ℝ))
            (b : basis ((s : set (matrix (fin m) (fin n) ℝ)) : Type*) ℝ (matrix (fin m) (fin n) ℝ)),
            (finset.card s = m * n) :=
begin
  let s_basis := finite_dimensional.finset_basis ℝ (matrix (fin m) (fin n) ℝ),
  refine ⟨_, s_basis, _⟩,
  rw [←finite_dimensional.finrank_eq_card_finset_basis s_basis,
      matrix.finrank_matrix],
  repeat { rw [fintype.card, finset.card_fin] }
end

[Johan Commelin]

-- Why isn't there a nice coe_to_sort on finset?

:this:

[Anne Baanen]

#7575

[Eric Wieser]

Should finset be set_like?

[Eric Wieser]

It wasn't originally what I was trying to do when I created set_like, but is maybe still appropriate