Calculating with 2 by 2 matrices

Stream: new members

[Phillip Harris]

Hi everyone. So I have a parameterization of SO(2) using Real.sin and Real.cos. I want to prove that conjugating a 2x2 matrix by a quarter-turn swaps the diagonal entries.

noncomputable def SO2 (theta : Real) : Matrix (Fin 2) (Fin 2) Real :=
  fun i j => match (i, j) with
    | (0,0) => theta.cos
    | (0,1) => theta.sin
    | (1,0) => -1*theta.sin
    | (1,1) => theta.cos

noncomputable def quarter_turn : Matrix (Fin 2) (Fin 2) Real
  := SO2 (Real.pi/2)

lemma quarter_turn_swaps_diagonal (A : Matrix (Fin 2) (Fin 2) Real)
  : (quarter_turn * A * quarter_turn⁻¹) 0 0 = A 1 1
  ∧ (quarter_turn * A * quarter_turn⁻¹) 1 1 = A 0 0
  := by
  unfold quarter_turn
  unfold SO2
  simp [Matrix.mul_apply, Matrix.inv, Matrix.det, Matrix.adjugate, Matrix.transpose, Matrix.detRowAlternating, MultilinearMap.alternatization, Matrix.of]

I thought I could do this by just simplifying the 2x2 matrix equation over and over, but eventually I end up with a summation over Fin 2 which seems like too much for it to handle. Is this the right approach or do I need to do something else?

[Eric Wieser]

You are likely to have a better time defining your matrix using !![ notation

[Eric Wieser]

docs#Matrix.det_fin_two will surely also help

[Eric Wieser]

Though I think you'd also do better to explicitly write down the inverse, and prove it is the inverse via showing the pair multiply to 1

[Phillip Harris]

I see thanks. I actually had that lemma already, I just felt like in principle I shouldn't need it lol. This is how I wrote it, is there a way to factor out the repeated simp and ring_nf steps in the 4 cases?

theorem SO2_inverse (theta : Real) : (SO2 theta)⁻¹ = SO2 (-theta) := by
  apply Matrix.inv_eq_left_inv
  ext i j
  simp [SO2, Matrix.mul_apply]
  match i, j with
  | 0, 0 => simp ; ring_nf ; simp [Real.cos_sq_add_sin_sq]
  | 0, 1 => simp ; ring_nf
  | 1, 0 => simp ; ring_nf
  | 1, 1 => simp ; ring_nf ; simp [Real.cos_sq_add_sin_sq]

[Eric Wieser]

#5863 would probably help you here...

[Eric Wieser]

If you just want to avoid the repetition, you can write

  apply Matrix.inv_eq_left_inv
  ext i j
  simp [SO2, Matrix.mul_apply]
  match i, j with
  | 0, 0
  | 0, 1
  | 1, 0
  | 1, 1 => simp ; ring_nf ; try simp [Real.cos_sq_add_sin_sq]

[Phillip Harris]

I see thanks! And I guess I'll just wait for that other PR.

[Eric Wieser]

A more typical approach here is fin_cases i <;> fin_cases j <:> a pile of hammers

[Phillip Harris]

So now I want to have SO(2) act on two coordinates i,j of a larger nxn matrix. I thought I could do this by viewing the larger matrix as a block matrix where one of the blocks is 2x2 using Mathlib.LinearAlgebra.Matrix.Reindex etc. But this is pretty painful so far. Is there a better way or should I continue trying to deal with block matrices?

[Kevin Buzzard]

So this cannot be expressed by matrix multiplication? You're just changing four entries of a large matrix? Or something else? I don't really know what you mean.

[Phillip Harris]

Sorry, yeah it is multiplication. I mean I have an n x n matrix R where the (i,j) entry is sin, the (j,i) entry is -sin, the (i,i) and (j,j) entries are cos and the rest is the identity matrix. And I have another n x n matrix A and I want to prove stuff about R A R^{-1} say.

So what I'm trying right now is wlog assume i = 0, j = 1, and then decompose R and A into blocks using finSumFinEquiv etc

[Kevin Buzzard]

It's hard to give advice unless you're a lot more precise about the "stuff" you're proving. Can you give a #mwe ?

[Phillip Harris]

Ok here's something I want to prove:

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse

noncomputable def big_SO2 (i j : Fin n) (t : ℝ)
  : Matrix (Fin n) (Fin n) ℝ
  := fun k l =>
    if k = i ∧ l = i then t.cos else
    if k = i ∧ l = j then t.sin else
    if k = j ∧ l = i then -t.sin else
    if k = j ∧ l = j then t.cos else
    if k = l then 1 else 0

noncomputable def big_quarter_turn (i j : Fin (n+2)) : Matrix (Fin (n+2)) (Fin (n+2)) ℝ
  := big_SO2 i j (Real.pi/2)

lemma big_quarter_turn_swaps_diagonal
  (A : Matrix (Fin (n+2)) (Fin (n+2)) ℝ)
  (i j : Fin (n+2))
  : ((big_quarter_turn i j) * A * (big_quarter_turn i j)⁻¹ ) i i = A j j
  ∧ ((big_quarter_turn i j) * A * (big_quarter_turn i j)⁻¹ ) j j = A i i
  := by sorry

[Eric Wieser]

I think this might be useful (edit: moved to a new thread)

[Eric Wieser]

Combined with

@[simps]
def SpecialLinearGroup.fromBlocks : SpecialLinearGroup m R × SpecialLinearGroup n R →* SpecialLinearGroup (m ⊕ n) R where
  toFun MN := ⟨Matrix.fromBlocks MN.1 0 0 MN.2, by simp⟩
  map_one' := sorry
  map_mul' _ _ := sorry

[Eric Wieser]

and

@[simps]
def SpecialLinearGroup.reindexMulEquiv (e : m ≃ n) : SpecialLinearGroup m R ≃* SpecialLinearGroup n R where
  toFun M := ⟨M.1.reindex e e, by simp⟩
  map_mul' _ _ := sorry

[Eric Wieser]

I think those second two together (with the sorries filled) would be a nice first PR to mathlib, if you're interested in making one (or an $n^\mathrm{th}$ if you've already made some!)

[Phillip Harris]

Gotcha, so it seems like my big_quarter_turn lemma might be a bit ambitious and I should work on smaller lemmas first?

[Eric Wieser]

It's often better to work in the most general setting - for instance, in this case the distraction of trigonometry goes away

[Kevin Buzzard]

Are you sure that theorem is true if i=j?

[Phillip Harris]

Ah yeah, need to assume i \neq j. I'm still just struggling with the block matrix API.

[Kevin Buzzard]

With that hypothesis in place it should be possible to grind out the matrix calculations. Matrix multiplication is defined in the obvious way and so the coefficients are sums, so you could start by proving lemmas such as "if k=l=j then the entry is this" and "if l isn't k or i or I then it's zero" and when you have these then you invoke lemmas of the form "this arbitrary finite sum is equal to a sum over this set of size 3 because the summand vanishes outside those three entries" etc. It will be a bit of a grind but it's definitely doable. The problem with Eric's idea is that your middle matrix is not in block form so I think it might have limited applicability, not sure. In general there is no nice formula for your entries so in some sense your example is not good, you have all this trig and then the calculation relies essentially on cos(pi/2) being zero which makes the matrix even more degenerate.

Oh in fact here's what I'd do to prove your example -- I'd show that big_quarter_turn is a permutation matrix and then it's easy.

[Phillip Harris]

I ended up grinding it out with the block matrix API. It's long (like 200+ lines) but I'm probably not doing it the most efficient way.

I have another question about coercions (should I make another thread?). Basically I have a situation like this:

import Mathlib.Data.Matrix.Basic

theorem myTheorem
  (A : Matrix (Fin (n+1+1)) (Fin (n+1+1)) ℕ)
  (h : A 0 0 = 0)
  : ∃ A' : Matrix (Fin (2+n)) (Fin (2+n)) ℕ, B ⟨0, by omega⟩ ⟨0, by omega⟩ = 0
  := by
  have eq : n + 1 + 1 = 2 + n := by omega
  rw [eq] at A
  sorry

The problem is after I change the type of A, the hypothesis that A 0 0 = 0 refers to an old version of A with a cross after it. How do I clean up the type of A while still remembering the hypotheses?

[Kevin Buzzard]

Don't rewrite at A at all, you'll end up in dependent type hell. Just make a new matrix A' of size 2+n by exploiting a bijection (which you should not think of as the identity) between Fin(2+n) and Fin(n+2) etc etc. Better still, rethink your strategy so as to not have to move between Fin(2+n) and Fin(n+2) at all.

[Kevin Buzzard]

It's true that the informal textbooks spend a lot of time thinking about matrices indexed by {1,2,...,n} but this is not how Lean's matrix API works at all, lean is happy to index rows and columns of a matrix with general types, and things which you're trying to do with explicit sets of numbers are probably better done by thinking more flexibly in lean in terms of bijections rather than concrete indexing sets.

[Kevin Buzzard]

Basically you've been brainwashed by the paper literature

[Phillip Harris]

Ok I guess n+1+1 is definitionally equal to n+2, so I could change it so that the 2x2 block is on the right instead of the left. I was getting +1 +1 by using the succ case twice.

[Kevin Buzzard]

Yes this would be one workaround. Another would be to get used to whatever the API is for changing index types, is it something like docs#Matrix.reorder etc? I don't really ever use matrices, I stick to linear maps...

[Kevin Buzzard]

Yeah it's not that, sorry, there's definitely a way of moving between matrix rings given a bijection of the index types, this is the way that you should probably be encouraged to do this.

[Eric Wieser]

docs#Matrix.reindex

[Kevin Buzzard]

What would be more useful here would be a ring isomorphism between square matrices over bijective index types

[Phillip Harris]

Yeah there's Matrix.reindexLinearEquiv_mul and then the lemma that says reindexing respects inverse is Matrix.inv_reindex

[Eric Wieser]

docs#Matrix.reindexAlgEquiv