Dimension of matrix

Stream: new members

[Yakov Pechersky]

Still trying to get my lean-sea-legs. Currently, I'd like to show that the dimension of a A : M_n(R) is n^2. Mathlib-wise, that seems to mean going from matrix -> linear operator -> basis/rank -> vector space -> dimension. Is that correct? What's the best way of searching the mathlib docs to figure out the right incantations to go down this path?

[Scott Morrison]

I'm not sure what exactly your chain of arrows means.

[Scott Morrison]

You need a vector_space R (matrix n n r) instance, and a finite_dimensional R (matrix n n r) in order to be able to assert findim R (matrix n n r) = n.card^2.

[Scott Morrison]

(And certainly you should do this for rectangular matrices, anyway.)

[Scott Morrison]

There are probably already these instances for function types, so in an ideal world it may just be a matter of unfolding the definition of matrix and running apply_instance.

[Yakov Pechersky]

On my way to trying to understand what you mean, here's a related example of what I think should be possible to prove:

@[reducible] def Mn (α : Type u) (n : ℕ) := matrix (fin n) (fin n) α
@[reducible] def MnR (n : ℕ) := Mn ℝ n

example : rank ((1 : MnR 2).to_lin) = 2 :=
by sorry

[Yakov Pechersky]

Scott Morrison said:

You need a vector_space R (matrix n n r) instance, and a finite_dimensional R (matrix n n r) in order to be able to assert findim R (matrix n n r) = n.card^2.

findim is not found in the mathlib docs by the supplied Google search, but github got my back.
It "corrected" findim to "findom". It does find findim.

[Yakov Pechersky]

I can't find the lemma that would give us the product of the dimensions from the linear map version of the matrix as ((n → R) →ₗ[R] n → R). I see the simp lemma finite_dimensional.findim_fin_fun, which gives us what we would be multiplying.

[Scott Morrison]

Yes, I agree this lemma is missing.

[Scott Morrison]

Presumably one should prove that a finitely generated module tensored with a noetherian module is again noetherian.

[Scott Morrison]

But maybe that's more than you want to bite off for now!

[Scott Morrison]

In any case, that won't immediately calculate the dimension for you, just show that it is finite dimensional.

[Yakov Pechersky]

Yeah, you're right that working with modules is going a little far from me.

[Yakov Pechersky]

Just trying to learn how to speak mathlib. How does one work with the fintype.card structure, which I get from the following?

example : rank (1 : (MnR 2)).to_lin = 2 :=
begin
  rw <-matrix.diagonal_one,
  rw matrix.rank_diagonal, --↑(fintype.card {i // 1 ≠ 0}) = 2
  simp, --↑(fintype.card {i // true}) = 2
  sorry
end

[Scott Morrison]

You might have to do a #mwe.

[Scott Morrison]

But my guess is that you want some theorem that says fintype.card is constant along equivalences, and provide the equivalence { x : X // true } with X.

[Scott Morrison]

src#fintype.card_congr

[Scott Morrison]

import data.equiv.basic

example {X : Type} : {x : X // true} ≃ X := by library_search

[Scott Morrison]

So for your dimension calculation, if you don't want to level up to noetherian modules quite yet, there's probably a way to just explicitly construct and verify a basis.

[Yakov Pechersky]

Scott Morrison said:

You might have to do a #mwe.

import data.nat.basic
import data.real.basic
import data.matrix.basic
import linear_algebra.basic
import linear_algebra.matrix

universes u v

-- we specialize matrix for n × n matrices
-- with a reducible definition because it's just a shell defn
@[reducible] def Mn (α : Type u) (n : ℕ) := matrix (fin n) (fin n) α

-- and a shortcut for Mn(ℝ)
@[reducible] def MnR (n : ℕ) := Mn ℝ n
example : rank (1 : (MnR 2)).to_lin = 2 :=
begin
  rw <-matrix.diagonal_one,
  rw matrix.rank_diagonal, --↑(fintype.card {i // 1 ≠ 0}) = 2
  simp, --↑(fintype.card {i // true}) = 2
  sorry
end

[Scott Morrison]

@Yakov Pechersky almost certainly what you want to do is show that currying is linear. Then you can use that matrix n m X is linearly equivalent to (n * m) -> X, which you already know the dimension of.

[Yakov Pechersky]

That makes sense. Right now I'm down a seemingly dark path of

example (m n : ℕ) : ∃ (f : (fin m × fin n) -> matrix (fin m) (fin n) ℝ), is_basis ℝ f :=
begin
  use (λ ⟨si, sj⟩, λ i j, ite ((i = si) ∧ (j = sj)) (1 : ℝ) 0),
  split,
  { apply linear_independent.of_subtype_range,
    { rintros ⟨ia, ja⟩ ⟨ib, jb⟩ f,
      dsimp [_example._match_1] at f,
      by_cases hi : ia = ib,
      by_cases hj : ja = jb,
      rw [hi, hj],
      sorry,
      -- f : (λ (i : fin m) (j : fin n), ite (i = ia ∧ j = ja) 1 0)
      --      = λ (i : fin m) (j : fin n), ite (i = ib ∧ j = jb) 1 0,
      },
     }
end

[Yakov Pechersky]

Which seems like an interpretation of your currying statement. It's probably more complicated to prove that currying statement in the context of the ite and matrix structures.

[Johan Commelin]

@Yakov Pechersky Yup, I think that a bit more abstraction will actually make your life easier.

[Johan Commelin]

Not that you aren't using anything about fin n apart from it being a fintype.

[Johan Commelin]

So you might as well try to work with arbitrary fintypes

[Kenny Lau]

import data.matrix.basic linear_algebra.dimension

universes u v

variables {m n : Type u} [fintype m] [fintype n]
variables {F : Type v} [field F]

theorem dim_matrix : vector_space.dim F (matrix m n F) = fintype.card m * fintype.card n :=
show vector_space.dim F (m → n → F) = ↑(fintype.card m) * ↑(fintype.card n), -- why doesn't unfold work?
by rw [dim_fun_eq_lift_mul, dim_fun', cardinal.lift_nat_cast]

[Johan Commelin]

Now you only need finite_dimensional and you can use findim so that you avoid the cardinals.

[Kenny Lau]

import data.matrix.basic linear_algebra.finite_dimensional

universes u v

variables {m n : Type u} [fintype m] [fintype n]
variables {F : Type v} [field F]

theorem dim_matrix : vector_space.dim F (matrix m n F) = fintype.card m * fintype.card n :=
show vector_space.dim F (m → n → F) = ↑(fintype.card m) * ↑(fintype.card n), -- why doesn't unfold work?
by rw [dim_fun_eq_lift_mul, dim_fun', cardinal.lift_nat_cast]

instance finite_dimensional_matrix : finite_dimensional F (matrix m n F) :=
by { rw [finite_dimensional.finite_dimensional_iff_dim_lt_omega, dim_matrix, ← nat.cast_mul],
exact cardinal.nat_lt_omega _ }

theorem findim_matrix : finite_dimensional.findim F (matrix m n F) = fintype.card m * fintype.card n :=
by rw [← cardinal.nat_cast_inj.{max u v}, finite_dimensional.findim_eq_dim, dim_matrix, nat.cast_mul]

[Yakov Pechersky]

Specialized to N:

variables {m n : ℕ}
variables {F : Type v} [field F]

theorem dim_matrix : vector_space.dim F (matrix (fin m) (fin n) F) =  m * n :=
show vector_space.dim F (fin m → fin n → F) = m * n, -- why doesn't unfold work?
by rw [dim_fun_eq_lift_mul, dim_fin_fun]; simp

[Yakov Pechersky]

So the crucial point was to recognize (η → V) in the docs as a matrix, because the underlying definition of a matrix is a function.

[Yakov Pechersky]

Per Scott's suggestion, I'm also trying the exercise of showing that currying is linear. What's the incantation to unravel the prod.rec in the following? I want to supply the proof that addition of matrices is linear.

import data.fintype.basic
import data.matrix.basic
import linear_algebra.basic

universes u v

lemma linear_prod {k : Type u} {m n : Type v} [field k] [fintype m] [fintype n] :
  linear_equiv k (matrix m n k) ((m × n) -> k) :=
begin
  refine {to_fun := λ M, λ ⟨i, j⟩, M i j, .. },
  { intros x y,
    simp,
    -- prod.rec (λ (fst : m) (snd : n), id_rhs k (x fst snd + y fst snd)) =
    -- prod.rec (λ (fst : m) (snd : n), id_rhs k (x fst snd))
    --  + prod.rec (λ (fst : m) (snd : n), id_rhs k (y fst snd))
    sorry,
  },
  sorry,
end

[Johan Commelin]

Note that there are already definitions function.curry and function.uncurry.

[Kevin Buzzard]

  { intros x y,
    ext z,
    cases z,
    refl,
  },

[Johan Commelin]

You probably want to use those

[Kevin Buzzard]

Do you know about hole commands?

lemma linear_prod {k : Type u} {m n : Type v} [field k] [fintype m] [fintype n] :
  linear_equiv k (matrix m n k) ((m × n) -> k) :=
{! !}

and then click on the lightbulb and select "generate a skeleton for the structure under construction"

[Yakov Pechersky]

I saw it before in some of the tutorials, but didn't grok it to remember to use it.

[Bryan Gin-ge Chen]

That should be a def not a lemma, by the way.

[Yakov Pechersky]

Thanks for all the patience!

[Yakov Pechersky]

I think I got the instance finally:

import data.fintype.basic
import data.matrix.basic
import linear_algebra.basic
import linear_algebra.finite_dimensional

universes u v

def linear_prod {k : Type u} {m n : Type v} [field k] [fintype m] [fintype n] :
  linear_equiv k (matrix m n k) ((m × n) -> k) :=
{ to_fun := λ M ⟨i, j⟩, M i j,
  add := λ x y, by ext z; cases z; refl,
  smul := λ c x, by ext z; cases z; refl,
  inv_fun := function.curry,
  left_inv := λ M, rfl,
  right_inv := λ M, by { ext z, cases z, refl } }

instance matrix_fin_dim {k : Type u} {m n : Type v} [field k] [fintype m] [fintype n] :
  finite_dimensional k (matrix m n k) :=
begin
  apply @linear_equiv.finite_dimensional k (m × n -> k),
  symmetry,
  exact linear_prod,
end

[Yakov Pechersky]

Now to figure out how it makes the findim call nice and easy.

[Johan Commelin]

@Yakov Pechersky One tip: don't make k, m, and n implicit in linear_prod.

[Johan Commelin]

In this special case, lean can figure them out, but usually it won't.

[Yakov Pechersky]

It wasn't really figuring them out, that's why I had to do the @linear_equiv after a lot of struggling

[Yakov Pechersky]

How do I know in general when to make the explicit? The definition of linear_prod seemed to me like the k m n would be arbitrary and inferred.

[Mario Carneiro]

Make parameters implicit when they can be inferred by later hypotheses

[Yakov Pechersky]

OK, I think this is it, finally!

import data.real.basic
import data.fintype.basic
import data.matrix.basic
import linear_algebra.basic
import linear_algebra.finite_dimensional

universes u v

def linear_prod (k : Type u) (m n : Type v) [field k] [fintype m] [fintype n] :
  linear_equiv k (matrix m n k) ((m × n) -> k) :=
{ to_fun := λ M ⟨i, j⟩, M i j,
  add := λ x y, by ext z; cases z; refl,
  smul := λ c x, by ext z; cases z; refl,
  inv_fun := function.curry,
  left_inv := λ M, rfl,
  right_inv := λ M, by { ext z, cases z, refl } }

instance matrix_fin_dim {k : Type u} {m n : Type v} [field k] [fintype m] [fintype n] :
  finite_dimensional k (matrix m n k) :=
begin
  apply @linear_equiv.finite_dimensional k (m × n -> k),
  symmetry,
  apply linear_prod,
end

@[reducible] def Mn (α : Type u) (n : ℕ) := matrix (fin n) (fin n) α

@[reducible] def MnR (n : ℕ) := Mn ℝ n

example (n : ℕ) : finite_dimensional.findim ℝ (MnR n) = n^2 :=
begin
  rw @linear_equiv.findim_eq ℝ (MnR n) _ _ _ _ _ _ (linear_prod ℝ (fin n) (fin n)),
  simp [nat.pow_two],
end

[Scott Morrison]

Looking good.

[Scott Morrison]

Notice your first def linear_prod now has nothing to do with matrices or fintypes at all.

[Scott Morrison]

You could generalise this just to linear_equiv k (m -> n -> k) ((m × n) -> k).

[Yakov Pechersky]

Just did that in my file, and placed _ for the unused lambda vars

[Yakov Pechersky]

Then the [fintype m] seem to be unnecessary too

[Scott Morrison]

There's also the existing definition src#equiv.arrow_arrow_equiv_prod_arrow

[Patrick Massot]

The body of that def is pretty spicy.

[Scott Morrison]

which you could use to write four of the fields, e.g. as something like

{ add := sorry,
   smul := sorry,
   ..equiv.arrow_arrow_equiv_prod_arrow m n k }

[Scott Morrison]

Another good exercise here would be to golf away the begin ... end block in matrix_fin_dim: you can write that directly in term mode with no trouble.

[Yakov Pechersky]

That's pretty awesome. What would have been a good way to find the equiv.arrow.*, just practice and familiarity with the codebase?

[Scott Morrison]

I found it by opening up the file data/equiv/basic.lean, and searching for the word curry.

[Scott Morrison]

Sadly curry wasn't actually in the name, but it's used in the construction.

[Scott Morrison]

But presumably library_search will find it.

[Scott Morrison]

Often the trick with good library_search use is to write an example that states exactly what you want.

[Patrick Massot]

import data.equiv.basic
example (α β γ : Sort*) : (α → β → γ) ≃ (α × β → γ) :=
begin
  library_search,
end

[Yakov Pechersky]

Ah. I searched the docs for curry, and found data/equiv/basic.lean too, but didn't look at the source, and didn't realize that the curry_uncurry theorem was exactly what left_inv meant.

[Patrick Massot]

You can even switch sides and library_search still finds it

[Yakov Pechersky]

Patrick also hints well that understanding that the ≃ relationship is a subset of the ≃ₗ helps identify where to find pieces to put together.

[Scott Morrison]

Looks like another PR soon! :-)

[Patrick Massot]

This linear version of equiv.arrow_arrow_equiv_prod_arrow is clearly needed.

[Patrick Massot]

And of course applying it to compute dimension of matrix spaces is also very welcome.

[Bryan Gin-ge Chen]

Scott Morrison said:

There's also the existing definition src#equiv.arrow_arrow_equiv_prod_arrow

We probably want to add "curry" or "uncurry" to the docstring here (and in any other related places).

[Mario Carneiro]

we could also just call it curry_equiv if people prefer that name

[Mario Carneiro]

We should really find a better way to use aliases for this kind of thing

[Yakov Pechersky]

Patrick Massot said:

This linear version of equiv.arrow_arrow_equiv_prod_arrow is clearly needed.

Would a PR of this be preferred in this general curry form, or in the language of linear maps →ₗ[R]?

[Yakov Pechersky]

I currently have a definition going:

import linear_algebra.basic

universes u v w

section curry

/-- Linear equivalence between an uncurried and curried function. -/
protected def curry (R : Type u) (V : Type v) (V₂ : Type w) [semiring R]:
  (V → V₂ → R) ≃ₗ[R] (V × V₂ → R) :=
{ add := λ _ _, by ext z; cases z; refl,
  smul := λ _ _, by ext z; cases z; refl,
  .. equiv.arrow_arrow_equiv_prod_arrow _ _ _}

end curry

but when trying to use it as a regular linear_equiv, I get the following error:

#check linear_equiv.curry.symm
-- type mismatch at application
--   linear_equiv.curry.symm
-- term
--   linear_equiv.curry
-- has type
--   (?m_2 → ?m_3 → ?m_1) ≃ₗ[?m_1] ?m_2 × ?m_3 → ?m_1 : Type (max (max ? ? ?) (max ? ?) ?)
-- but is expected to have type
--   ?m_2 ≃ₗ[?m_1] ?m_3 : Type (max ? ?)

[Jalex Stark]

Is the problem that you're missing arguments to curry?

[Jalex Stark]

import linear_algebra.basic

universes u
/-- Linear equivalence between an uncurried and curried function. -/
protected def curry (R : Type u) (V : Type u) (V₂ : Type u) [semiring R]:
  (V → V₂ → R) ≃ₗ[R] (V × V₂ → R) :=
{ add := λ _ _, by ext z; cases z; refl,
  smul := λ _ _, by ext z; cases z; refl,
  .. equiv.arrow_arrow_equiv_prod_arrow _ _ _}

variables (R : Type u) (V : Type v) (V₂ : Type w) [semiring R]

This first one works and the second gives the same error as you.

#check (curry R V V₂).symm
#check (curry _ _ _).symm

[Yakov Pechersky]

That was super informative -- I was relying on the implicit arguments in the module, and had to make them explicit with a variables (R ...) call. Now I understand what that call does. Before, it was unclear what it was doing without type information.

[Yakov Pechersky]

Finally: https://github.com/leanprover-community/mathlib/pull/3013

[Yakov Pechersky]

Which allows for:

example (n : ℕ) : finite_dimensional.findim R (matrix (fin n) (fin n) R) = n^2 :=
  by simp [nat.pow_two]

[Yakov Pechersky]

Once everything works, it's very concise. Getting there is quite the journey.