Super basic linear algebra in Mathlib?

Stream: new members

[Arien Malec]

Back at doing Axler in Lean, and I realize that I know next to nothing about how to put the Mathlib4 parts together. If I wanted to show that vectors in $R^n$ form a vector space, what is the most basic Mathlib setup?

[Richard Copley]

Maybe this?

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

#synth (n : ℕ) → Module ℝ (Fin n → ℝ)

There's some mention of modules in Section 8.2 of Mathematics in Lean 4, but the promised chapter on linear algebra doesn't appear to be there yet, unless I missed something.

[Eric Wieser]

(deleted: Richard posted a better version of the same thing!)

[Eric Wieser]

Though in case it's unclear, you could also write:

variable (n : ℕ)

#synth Module ℝ (Fin n → ℝ)

[Arien Malec]

Cool -- but seems like magic? I get fun n => Pi.module (Fin n) (fun a => ℝ) ℝ -- have I gotten for free proofs of the various laws for vector addition and scalar multiplication? If so, where did they come from? How might I have done them myself? There's this weird space in Mathlib where doing things from first principles is easy, and doing hard things is possible but doing easy things is seemingly hard....

[Eric Wieser]

Yes, you did indeed get them all for free! The message is telling you where the laws for scalar multiplication came from; docs#Pi.module

[Eric Wieser]

#synth AddCommGroup ℝ (Fin n → ℝ) will tell you where the laws for addition came from

[Eric Wieser]

Though the source code for either will not be particularly insightful

[Arien Malec]

Yeah, that was my first stop....

[Eric Wieser]

https://www.youtube.com/watch?v=L_VDsP9_ty8 or https://leanprover-community.github.io/mathematics_in_lean/C06_Structures.html#algebraic-structures has an exercise that has you prove that {x, y, z} structures form an additive group

[Eric Wieser]

I don't know if we have any exercises for doing the analogous thing for vector spaces

[Eric Wieser]

(note that both links come with corresponding exercise files)

[Arien Malec]

Where did the instance for Add and SMul for (Fin n → ℝ) come from?

[Jireh Loreaux]

docs#Pi.instAdd docs#Pi.instSMul

[Jireh Loreaux]

Basically, when the codomain has some operation, you can put an operation onto the functions by just defining that operation pointwise.

[Arien Malec]

If I've got this right, this is the non-magic version?

import Mathlib.Tactic

@[ext]
structure Rn (n: ℕ ) where
  term: Fin n → ℝ

instance addRn: Add (Rn n) where
  add a b := ⟨fun n => a.term n + b.term n⟩

@[simp]
theorem add_ext {a b : (Rn n)} {x: Fin n}: (a + b).term x = a.term x + b.term x := rfl

instance smulRn: SMul ℝ (Rn n) where
  smul x a := ⟨fun n => x * a.term n⟩

@[simp]
theorem smul_ext {a : Rn n} {x: ℝ} {y: Fin n}: (x • a).term y = x • (a.term y) := rfl

instance zeroRn: Zero (Rn n) where
  zero := ⟨fun _ => 0⟩

@[simp]
theorem zero_ext: (0 :Rn n).term x = 0 := rfl

instance addCommMonoidRn: AddCommMonoid (Rn n) where
  add_comm a b := by  ext ; simp [add_comm]
  add_assoc a b c := by ext ; simp [add_assoc]
  zero := zeroRn.zero
  add_zero a := by ext ; simp only [add_ext, add_zero, zero_ext]
  zero_add a := by ext ; simp only [add_ext, zero_add, zero_ext]

instance moduleRn: Module ℝ (Rn n) where
  one_smul a := by ext; simp
  zero_smul a := by ext; simp
  smul_zero a := by ext; simp
  smul_add a b c := by ext; simp [mul_add]
  add_smul a b c := by ext; simp [add_mul]
  mul_smul a b c := by ext; simp [mul_assoc]

[Eric Wieser]

That looks good to me: though your lemmas are strangely named, we would normally call your add_ext term_add_apply since it's applying term to add

[Arien Malec]

How would I generalize the declaration of Rn to Fn where it works across any field? Axler wants proofs that work for what he defines as F which is real or complex (I know there's a "real or complex" type somewhere in Mathlib as well).

If I do

import Mathlib.Tactic
import Mathlib.Algebra.Field.Basic

@[ext]
structure Rn [Field F] (n: ℕ) where
  term: Fin n → F

instance addRn: Add (Rn n) where
  add a b := ⟨fun n => a.term n + b.term n⟩

I get a typeclass instance stuck issue.

[Richard Copley]

instance addRn [Field F] : Add (Rn n) where
  add a b := ⟨fun n => a.term n + b.term n⟩

[Eric Wieser]

Surely that doesn't work Richard; does lean really guess F?

[Eric Wieser]

@Arien Malec: can you add imports and any variables to your example?

[Arien Malec]

Oops, forgot the MWE norms. Done.

[Arien Malec]

Can confirm adding [Field F] doesn't work...

[Richard Copley]

Eric Wieser said:

Surely that doesn't work Richard; does lean really guess F?

I assumed there was a variable {F : Type*} somewhere, rather than the F in Rn being an autoImplicit.

@Arien Malec, since the F you're implicitly passing to Rn has no name in addRn, there's no way to tell Lean that it is a field. Something like this should work:

import Mathlib.Tactic
import Mathlib.Algebra.Field.Basic

set_option autoImplicit false

@[ext]
structure Rn (F : Type*) [Field F] (n: ℕ) where
  term: Fin n → F

instance addRn (F : Type*) [Field F] (n : ℕ) : Add (Rn F n) where
  add a b := ⟨fun n => a.term n + b.term n⟩

[Arien Malec]

Was racking my brain trying to see the difference between what I did and this until I saw the explicit F... Thanks!

[Arien Malec]

Also realized you need to change F from being explicit to being implicit....

[Arien Malec]

import Mathlib.Tactic
import Mathlib.Algebra.Field.Basic

variable (F: Type _)
variable [Field F]

@[ext]
structure Fn (n: ℕ) where
  term: Fin n → F

variable {F}

instance addRn {n: ℕ}: Add (Fn F n) where
  add a b := ⟨fun n => a.term n + b.term n⟩

@[simp]
theorem term_add_apply {n: ℕ} {a b : (Fn F n)} {x: Fin n}: (a + b).term x = a.term x + b.term x := rfl

instance smulRn: SMul F (Fn F n) where
  smul x a := ⟨fun n => x * a.term n⟩

@[simp]
theorem term_smul_apply {a : Fn F n} {x: F} {y: Fin n}: (x • a).term y = x • (a.term y) := rfl

instance zeroRn: Zero (Fn F n) where
  zero := ⟨fun _ => 0⟩

@[simp]
theorem zero_term: (0 :Fn F n).term x = 0 := rfl

instance addCommMonoidRn: AddCommMonoid (Fn F n) where
  add_comm a b := by  ext ; simp [add_comm]
  add_assoc a b c := by ext ; simp [add_assoc]
  zero := zeroRn.zero
  add_zero a := by ext ; simp only [term_add_apply, add_zero, zero_term]
  zero_add a := by ext ; simp only [term_add_apply, zero_add, zero_term]

instance moduleRn: Module F (Fn F n) where
  one_smul a := by ext; simp
  zero_smul a := by ext; simp
  smul_zero a := by ext; simp
  smul_add a b c := by ext; simp [mul_add]
  add_smul a b c := by ext; simp [add_mul]
  mul_smul a b c := by ext; simp [mul_assoc]

[Arien Malec]

Where again the automagic version is
#synth (n: ℕ) → Module F (Fin n → F)