10. Linear algebra

10.1. Vector spaces and linear maps

10.1.1. Vector spaces

“let \(K\) be a field and let \(V\) be a vector space over \(K\)”:

-- ``AddCommGroup`` only support multiplication with ℕ or ℤ
-- ``Field K`` provides scalar multiplication
variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

example (a : K) (u v : V) : a • (u + v) = a • u + a • v :=
  smul_add a u v

example (a b : K) (u : V) : (a + b) • u = a • u + b • u :=
  add_smul a b u

example (a b : K) (u : V) : a • b • u = b • a • u :=
  smul_comm a b u

10.1.2. Linear maps

Structure LinearMap between two K-vector spaces V and W is denoted by V →ₗ[K] W. The subscript l stands for linear.

variable {W : Type*} [AddCommGroup W] [Module K W]

variable (φ : V →ₗ[K] W)

example (a : K) (v : V) : φ (a • v) = a • φ v :=
  map_smul φ a v

example (v w : V) : φ (v + w) = φ v + φ w :=
  map_add φ v w

variable (ψ : V →ₗ[K] W)

#check (2 • φ + ψ : V →ₗ[K] W)

We need to use LinearMap.comp or the notation ∘ₗ.

variable (θ : W →ₗ[K] V)

#check (φ.comp θ : W →ₗ[K] W)
#check (φ ∘ₗ θ : W →ₗ[K] W)

Construct linear maps:

example : V →ₗ[K] V where
  toFun v := 3 • v
  map_add' _ _ := smul_add ..
  map_smul' _ _ := smul_comm ..

10.1.3. Sums and products of vector spaces

We can build new vector spaces out of old ones using direct sums and direct products.

section binary_product

variable {W : Type*} [AddCommGroup W] [Module K W]
variable {U : Type*} [AddCommGroup U] [Module K U]
variable {T : Type*} [AddCommGroup T] [Module K T]

-- First projection map
example : V × W →ₗ[K] V := LinearMap.fst K V W

-- Second projection map
example : V × W →ₗ[K] W := LinearMap.snd K V W

10.2. Subspaces

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

example (U : Submodule K V) {x y : V} (hx : x ∈ U) (hy : y ∈ U) :
    x + y ∈ U :=
  U.add_mem hx hy

example (U : Submodule K V) {x : V} (hx : x ∈ U) (a : K) :
    a • x ∈ U :=
  U.smul_mem a hx

10.2.1. Subspace spanned by a set

example {s : Set V} (E : Submodule K V) : Submodule.span K s ≤ E ↔ s ⊆ E :=
  Submodule.span_le

10.3. Endomorphisms

10.4. Matrices, bases and dimension

10.4.1. Matrices

For concrete vectors: ![…], where components are separated by commas.
For concrete matrices: !![…], rows are separated by “;”
- When entries have a computable type such as ℕ or ℚ, we can use the eval command to play with basic operations.

section matrices

-- Adding vectors
#eval ![1, 2] + ![3, 4]  -- ![4, 6]

-- Adding matrices
#eval !![1, 2; 3, 4] + !![3, 4; 5, 6]  -- !![4, 6; 8, 10]

-- Multiplying matrices
#eval !![1, 2; 3, 4] * !![3, 4; 5, 6]  -- !![13, 16; 29, 36]

Vector is neither a row vector nor a column vector: Matrix.vecMul: Multiplication of a matrix with
- a vector from the left ᵥ*: interprets as a row vector
- a vector from the right *ᵥ: interprets as a column vector

open Matrix

-- matrices acting on vectors on the left
#eval !![1, 2; 3, 4] *ᵥ ![1, 1] -- ![3, 7]

-- matrices acting on vectors on the left, resulting in a size one matrix
#eval !![1, 2] *ᵥ ![1, 1]  -- ![3]

-- matrices acting on vectors on the right
#eval  ![1, 1, 1] ᵥ* !![1, 2; 3, 4; 5, 6] -- ![9, 12]

Other familiar operations include the vector dot product, matrix transpose, and, for square matrices, determinant and trace.

-- vector dot product
#eval ![1, 2] ⬝ᵥ ![3, 4] -- `11`

-- matrix transpose
#eval !![1, 2; 3, 4]ᵀ -- `!![1, 3; 2, 4]`

-- determinant
#eval !![(1 : ℤ), 2; 3, 4].det -- `-2`

-- trace
#eval !![(1 : ℤ), 2; 3, 4].trace -- `5`

Different from computable types like ℕ ℤ, when entries are of noncomputable type, e.g. ℝ, we cannot use #eval!

We can use the simp and norm_num tactics in proofs, or their command counter-part for quick exploration.

#simp !![(1 : ℝ), 2; 3, 4].det -- `4 - 2*3`

#check (2 : ℝ)
#eval (2 : ℝ) + (2 : ℝ)

#norm_num !![(1 : ℝ), 2; 3, 4].det -- `-2`

#norm_num !![(1 : ℝ), 2; 3, 4].trace -- `5`

variable (a b c d : ℝ) in
#simp !![a, b; c, d].det -- `a * d – b * c`

Inversion A⁻¹ (only for invertible matrices):

#norm_num [Matrix.inv_def] !![(1 : ℝ), 2; 3, 4]⁻¹ -- !![-2, 1; 3 / 2, -(1 / 2)]

10.4.2. Bases

Basis ι K V: Bases indexed by a type ι of vector space K V
- ι is the set of possible indices, an element i : ι is an index chosen from that set.
- ι →₀ K: functions from ι to K with finite support; ₀ indicates finite support

The isomorphism is called Basis.repr.

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

section

open Module

variable {ι : Type*} (B : Basis ι K V) (v : V) (i : ι)

-- The basis vector with index ``i``
#check (B i : V)

-- the component function of ``v``
#check (B.repr v : ι →₀ K)

-- the component of ``v`` with index ``i``
#check (B.repr v i : K)

We can express any vector as a linear combination of basis vectors.

example [Fintype ι] : ∑ i : ι, B.repr v i • (B i) = v :=
  B.sum_repr v

10.4.3. Dimension

Bases are also useful to define the concept of dimension.

Module.finrank: get the dimension (ℕ) of finite-dimensional vector spaces.

section

#check (Module.finrank K V : ℕ)

-- `Fin n → K` is the archetypical space with dimension `n` over `K`.
example (n : ℕ) : Module.finrank K (Fin n → K) = n :=
  Module.finrank_fin_fun K

-- Seen as a vector space over itself, `ℂ` has dimension one.
example : Module.finrank ℂ ℂ = 1 :=
  Module.finrank_self ℂ

-- But as a real vector space it has dimension two.
example : Module.finrank ℝ ℂ = 2 :=
  Complex.finrank_real_complex