長めの例: K × K 上の線形写像と kernel

ここでは，2 次元ベクトル空間 K × K から K への線形写像 (x, y) ↦ x + y を作ります． 紙の数学では当たり前に線形写像と呼ぶものも，Lean では toFun，map_add'，map_smul' を与えて構造体として作ります．

section CoordinateLinearMaps

variable {K : Type*} [Field K]

def sumPairLinear : (K × K) →ₗ[K] K where
  toFun p := p.1 + p.2
  map_add' := by
    intro x y
    simp [add_left_comm, add_comm]
  map_smul' := by
    intro a x
    simp [mul_add]

example (x y : K) : sumPairLinear (x, y) = x + y := by
  rfl

example (x y : K) :
    (x, y) ∈ LinearMap.ker (sumPairLinear : (K × K) →ₗ[K] K) ↔ x + y = 0 := by
  rfl

この kernel は，方程式 x + y = 0 で定まる直線です． Lean では，kernel は Submodule K (K × K) です． つまり，単なる集合ではなく，線形部分空間としての閉性も持っています．

#check LinearMap.ker

example (p q : K × K)
    (hp : p ∈ LinearMap.ker (sumPairLinear : (K × K) →ₗ[K] K))
    (hq : q ∈ LinearMap.ker (sumPairLinear : (K × K) →ₗ[K] K)) :
    p + q ∈ LinearMap.ker (sumPairLinear : (K × K) →ₗ[K] K) := by
  exact (LinearMap.ker sumPairLinear).add_mem hp hq

example (a : K) (p : K × K)
    (hp : p ∈ LinearMap.ker (sumPairLinear : (K × K) →ₗ[K] K)) :
    a • p ∈ LinearMap.ker (sumPairLinear : (K × K) →ₗ[K] K) := by
  exact (LinearMap.ker sumPairLinear).smul_mem a hp