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

[Arthur Tilley]

Arthur Tilley said:

Here you go:

(And EDIT: As of 1 Jan 2026, this is the one remaining sorry in the Banach-Tarski project)

import Mathlib

abbrev R3 :=  EuclideanSpace ℝ (Fin 3)
-- Context.  Take all these sorries as being filled in until the comment at the bottom.
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

[Kevin Buzzard]

I just proved these in FLT recently:

lemma foo {R M N P ι j : Type*} [Fintype ι] [DecidableEq ι] [Fintype j]
    [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup P]
    [Module R P] (φ : M ≃ₗ[R] P) (α : P →ₗ[R] N)
    (b : Module.Basis ι R M) (c : Module.Basis j R N) :
    LinearMap.toMatrix (b.map φ) c α = LinearMap.toMatrix b c (α ∘ₗ φ) := rfl

lemma bar {R M N P ι j : Type*} [Fintype ι] [DecidableEq ι] [Fintype j]
    [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup P]
    [Module R P] (φ : N ≃ₗ[R] P) (α : M →ₗ[R] P)
    (b : Module.Basis ι R M) (c : Module.Basis j R N) :
    LinearMap.toMatrix b (c.map φ) α = LinearMap.toMatrix b c (φ.symm ∘ₗ α) := rfl

which makes me wonder whether you should define COB as Module.Basis.map of the obvious basis for S1 \times S2 under the obvious linear isomorphism. These lemmas will then hopefully reduce your claim to a claim about LinearMap.toMatrix B1 B1 [something] and LinearMap.toMatrix B2 B2 [something].

[Arthur Tilley]

Kevin Buzzard said:

I just proved these in FLT recently:

lemma foo {R M N P ι j : Type*} [Fintype ι] [DecidableEq ι] [Fintype j]
    [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup P]
    [Module R P] (φ : M ≃ₗ[R] P) (α : P →ₗ[R] N)
    (b : Module.Basis ι R M) (c : Module.Basis j R N) :
    LinearMap.toMatrix (b.map φ) c α = LinearMap.toMatrix b c (α ∘ₗ φ) := rfl

lemma bar {R M N P ι j : Type*} [Fintype ι] [DecidableEq ι] [Fintype j]
    [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup P]
    [Module R P] (φ : N ≃ₗ[R] P) (α : M →ₗ[R] P)
    (b : Module.Basis ι R M) (c : Module.Basis j R N) :
    LinearMap.toMatrix b (c.map φ) α = LinearMap.toMatrix b c (φ.symm ∘ₗ α) := rfl

which makes me wonder whether you should define COB as Module.Basis.map of the obvious basis for S1 \times S2 under the obvious linear isomorphism. These lemmas will then hopefully reduce your claim to a claim about LinearMap.toMatrix B1 B1 [something] and LinearMap.toMatrix B2 B2 [something].

Thanks @Kevin Buzzard . I gave one more look at the re-indexing theorems, with a little prompting from Claude, and the two of us landed upon

def fTS_fun: Fin 3 →  ((i : Fin 2) × mod_dim i) :=
    (fun k => match k with
      | ⟨0, _⟩ => ⟨⟨0, by norm_num⟩, ⟨0, by norm_num⟩⟩
      | ⟨1, _⟩ => ⟨⟨0, by norm_num⟩, ⟨1, by norm_num⟩⟩
      | ⟨2, _⟩ => ⟨⟨1, by norm_num⟩, ⟨0, by norm_num⟩⟩
    )

lemma fTS_fun_bij : Function.Bijective fTS_fun := ...

-- Define an equivalence between Fin 3 and the sigma type
noncomputable def finToSigma : Fin 3 ≃ ((i : Fin 2) × mod_dim i) := ...

-- Reindex the collected basis
noncomputable def COB_MB (ax: S2): Module.Basis (Fin 3) ℝ R3 :=
  ((internal_pr ax).collectedBasis (sm_bases ax)).reindex finToSigma.symm

Using known to show the desired theorem was still quite "manual" (required doing a fin_cases over ever cell and showing the equality between the two. But it was pretty straightforward.

I'm happy to say the BT project is now sorry-free. :face_with_open_eyes_and_hand_over_mouth: Time to turn the linter back on an make things a bit more presentable.