線形写像¶
V →ₗ[K] W は K 線形写像の型です．
これは関数と線形性の証明をまとめた bundled map です．
線形写像は関数として適用できますが，合成には LinearMap.comp または ∘ₗ を使います．
#check LinearMap
#check LinearEquiv
section LinearMaps
variable {K : Type*} [Field K]
variable {V W U : Type*}
variable [AddCommGroup V] [Module K V]
variable [AddCommGroup W] [Module K W]
variable [AddCommGroup U] [Module K U]
example (φ : V →ₗ[K] W) (a : K) (v : V) : φ (a • v) = a • φ v := by
exact map_smul φ a v
example (φ : V →ₗ[K] W) (v w : V) : φ (v + w) = φ v + φ w := by
exact map_add φ v w
example (φ : V →ₗ[K] W) (ψ : W →ₗ[K] U) : V →ₗ[K] U :=
ψ.comp φ
example (φ : V →ₗ[K] W) (ψ : W →ₗ[K] U) : V →ₗ[K] U :=
ψ ∘ₗ φ
example : V →ₗ[K] V :=
LinearMap.id
example (a : K) : V →ₗ[K] V :=
LinearMap.lsmul K V a
#check (LinearMap.lsmul K V : K →ₗ[K] V →ₗ[K] V)
end LinearMaps
線形写像どうしも加法やスカラー倍を持ちます． そのため，線形写像の空間そのものをベクトル空間として扱えます．
section LinearMapSpace
variable {K : Type*} [Field K]
variable {V W : Type*}
variable [AddCommGroup V] [Module K V]
variable [AddCommGroup W] [Module K W]
example (φ ψ : V →ₗ[K] W) (a : K) : V →ₗ[K] W :=
a • φ + ψ
example (φ ψ : V →ₗ[K] W) (v : V) : (φ + ψ) v = φ v + ψ v := by
rfl
end LinearMapSpace
演習問題¶
線形写像は 0 を 0 に送ることを示してください．