Show the basis vectors of R^n sum to R^n

Stream: new members

[Arien Malec]

It's been a while, but I'm working on Axler's LADL in Lean done natively in Mathlib (that is, using the actual Mathlib structures and proofs rather than recreating Axler's definitions).

I did a tour of MiL, then completed the proof that Axler's direct sum and Mathlib's notion of modeling \sup + IsCompl are equivalent.

Now we have the very basic notion that the canonical basis of R^n sums to R^n(in Axler's terms, the direct sum across all the subspaces formed form the span of each of the canonical vectors of R^n is R^n).

I see docs#Pi.basisFun ...

[Arien Malec]

There should probably have been a question: What's the Mathlib setup or statement to prove that the sum of all the submodules formed from the individual canonical basis vectors are \top (I guess).

[Richard Copley]

Do you mean like this?

import Mathlib.LinearAlgebra.StdBasis
import Mathlib.Data.Real.Basic

example (n : ℕ) : Submodule.span ℝ (Set.range ⇑(Pi.basisFun ℝ (Fin n))) = ⊤ :=
  (Pi.basisFun ℝ (Fin n)).span_eq

[Richard Copley]

Or this?

import Mathlib.LinearAlgebra.StdBasis
import Mathlib.Data.Real.Basic

example (n : ℕ) : (⨆ i, ℝ ∙ (Pi.basisFun ℝ (Fin n) i)) = ⊤ := by
  sorry

(R ∙ x is short for span R (singleton x); see docs#mem_span_singleton etc.)

[Arien Malec]

Perfect!

[Arien Malec]

Any hints for proving the last one?

[Arien Malec]

Obviously the first is the more natural formulation, but the second seems like it reveals better what's going on "under the covers".

[Arien Malec]

I think rw [← Submodule.span_range_eq_iSup] gets me close to the first form?

[Arien Malec]

Got it but had do do This One Weird Trick

import Mathlib.LinearAlgebra.StdBasis
import Mathlib.Data.Real.Basic

example (n : ℕ) : (⨆ i, ℝ ∙ (Pi.basisFun ℝ (Fin n) i)) = ⊤ := by
  rw [← Submodule.span_range_eq_iSup]
  have : (fun i => (Pi.basisFun ℝ (Fin n)) i) = ⇑(Pi.basisFun ℝ (Fin n)) := by rw [@DFunLike.coe_fn_eq]
  rw [this, (Pi.basisFun ℝ (Fin n)).span_eq]

[Arien Malec]

Slightly Less Weird Trick

example (n : ℕ) : (⨆ i, ℝ ∙ (Pi.basisFun ℝ (Fin n) i)) = ⊤ := by
  rw [← Submodule.span_range_eq_iSup]
  simp only [DFunLike.coe_fn_eq, (Pi.basisFun ℝ (Fin n)).span_eq]

[Arien Malec]

No tricks:

example (n : ℕ) : (⨆ i, F ∙ (Pi.basisFun ℝ (Fin n) i)) = ⊤ := by
  simp only [← Submodule.span_range_eq_iSup, (Pi.basisFun ℝ (Fin n)).span_eq]

So the simp machinery knows how to handle the conversion in the background while rw doesn't?

[Andrew Yang]

There are cases involving dependent types where simp is stronger than rw, but I think in this case they both work?

import Mathlib.LinearAlgebra.StdBasis
import Mathlib.Data.Real.Basic

example (n : ℕ) : (⨆ i, ℝ ∙ (Pi.basisFun ℝ (Fin n) i)) = ⊤ := by
  rw [← Submodule.span_range_eq_iSup, (Pi.basisFun ℝ (Fin n)).span_eq]

[Arien Malec]

So it does! I was trying to get the conversion to work and that wasn't working cleanly in rw without the hoops.

[Arien Malec]

Richard Copley said:

Or this?

import Mathlib.LinearAlgebra.StdBasis
import Mathlib.Data.Real.Basic

example (n : ℕ) : (⨆ i, ℝ ∙ (Pi.basisFun ℝ (Fin n) i)) = ⊤ := by
  sorry

(R ∙ x is short for span R (singleton x); see docs#mem_span_singleton etc.)

What dot is this? It's not \cdot or \smul

[Arien Malec]

I can't seem to get VS Code to tell me.

[Arien Malec]

Sometimes Unicode notation is great, sometimes:

  /- Note that the character `∙` U+2219 used below is different from the scalar multiplication
character `•` U+2022. -/
R " ∙ " x => span R (singleton x)

[Kevin Buzzard]

Indeed it's not in the VS Code list of abbreviations https://github.com/leanprover/vscode-lean/blob/master/src/abbreviation/abbreviations.json . Make a PR! You'll have to think of a good abbreviation for it :-)

[Arien Malec]

'\span'?

[Kevin Buzzard]

Looks good -- right now we have \spadesuit but nothing matching span.

[Arien Malec]

PR #447 to https://github.com/leanprover/vscode-lean4

I'll create a PR for Mathlib/LinearAlgebra/Span.lean itself, which has incorrect docu

[Arien Malec]

mathlib4#13039