toMatrix, collectedBasis, and fromBlocks?

Stream: general

[Arthur Tilley]

Context:

Foo is a LinearIsometryEquiv, and

noncomputable def bases_func  : (i : Fin 2) → (Module.Basis (mod_dim i) ℝ (submods i))
| ⟨0, _⟩ => (orth_B)
| ⟨1, _⟩ => (ax_B)

I have shown that

  LinearMap.toMatrix
  ((internal_pr).collectedBasis (bases_func))
  ((internal_pr).collectedBasis (bases_func)))
  (Foo).toLinearMap
  =
  Matrix.blockDiagonal' (fun i ↦
  match i with
  | ⟨0, _⟩ =>  !![θ.cos, -θ.sin; θ.sin, θ.cos]
  | ⟨1, _⟩ =>  !![1;]
  )

I’d like to convert this to show that

 LinearMap.toMatrix
(COB).toBasis
(COB).toBasis
(Foo).toLinearMap =

    !![
      θ.cos, -θ.sin, 0;
      θ.sin, θ.cos, 0;
      0, 0, 1;
    ]

(Where COB is a union of the bases in bases_fun.)

I would think there must be some Matlib lemma connecting toMatrix, collectedBasis and, say, fromBlocks, but I can’t find anything.

[Kevin Buzzard]

If you can beef up your question to make it a #mwe then this will make it easier for others to answer (and only one person does the work rather than all the people attempting to make your code compile given what you posted).

[Arthur Tilley]

Here you go:

import Mathlib

abbrev R3 :=  EuclideanSpace ℝ (Fin 3)
-- Context.  Take this for granted
def Foo : R3 ≃ₗᵢ[ℝ] R3 := sorry
def S1 : Submodule ℝ R3 := sorry
def S2 : Submodule ℝ R3 := sorry
def B1 : Module.Basis (Fin 2) ℝ S1 := sorry
def B2 : Module.Basis (Fin 1) ℝ S2 := sorry
def θ : ℝ := sorry


noncomputable def submods : (i: Fin 2) → (Submodule ℝ R3) := ![S1, S2]
lemma internal_pr: DirectSum.IsInternal submods := sorry

def mod_dim : (Fin 2) → Type
  | ⟨0,_⟩ => Fin 2
  | ⟨1,_⟩ => Fin 1

instance mod_dim_fintype (i : Fin 2) : Fintype (mod_dim i) := sorry
instance mod_dim_decidableEq (i : Fin 2) : DecidableEq (mod_dim i) := sorry


noncomputable def bases_func : (i : Fin 2) → (Module.Basis (mod_dim i) ℝ (submods i))
  | ⟨0, _⟩ => B1
  | ⟨1, _⟩ => B2

lemma known: LinearMap.toMatrix
  (internal_pr.collectedBasis bases_func)
  (internal_pr.collectedBasis bases_func)
  Foo.toLinearMap =
    Matrix.blockDiagonal' (fun i ↦
      match i with
      | ⟨0, _⟩ =>  !![θ.cos, -θ.sin; θ.sin, θ.cos]
      | ⟨1, _⟩ =>  !![1;]
      ) := sorry


-- You get to fill this in.  Should be some kind of union of B1 and B2
def COB : Module.Basis (Fin 3) ℝ R3 := sorry

-- Prove me
lemma goal: LinearMap.toMatrix COB COB Foo.toLinearMap =
    !![
      θ.cos, -θ.sin, 0;
      θ.sin, θ.cos, 0;
      0, 0, 1;
    ] := sorry