部分空間・部分加群¶

Submodule K V は，V の K 部分空間，より一般には部分加群です． Subgroup や Ideal と同じく，台集合と閉性の証明を持つ bundled structure です．

#check Submodule
#check Submodule.span

section Submodules

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

variable (S T : Submodule K V)

example {x y : V} (hx : x ∈ S) (hy : y ∈ S) : x + y ∈ S := by
  exact S.add_mem hx hy

example {x : V} (a : K) (hx : x ∈ S) : a • x ∈ S := by
  exact S.smul_mem a hx

example : ((S ⊓ T : Submodule K V) : Set V) = (S : Set V) ∩ (T : Set V) := by
  rfl

example (x : V) : x ∈ (⊥ : Submodule K V) ↔ x = 0 := by
  exact Submodule.mem_bot (R := K)

example (s : Set V) {x : V} (hx : x ∈ s) : x ∈ Submodule.span K s := by
  exact Submodule.subset_span hx

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

example : Submodule K W :=
  Submodule.map φ S

example : Submodule K V :=
  Submodule.comap φ U

example (x : V) : x ∈ Submodule.comap φ U ↔ φ x ∈ U := by
  rfl

#check LinearMap.ker
#check LinearMap.range

end Submodules

Submodule.span K s は集合 s : Set V で張られる部分空間です．部分空間の像と逆像は，線形写像に沿って map と comap で表されます．これは実践編 Chapter 01 の部分群と同じ設計です．

演習問題¶

kernel の元は，定義通り f x = 0 を満たすことを示してください．

example {K V W : Type*} [Field K]
    [AddCommGroup V] [Module K V]
    [AddCommGroup W] [Module K W]
    (f : V →ₗ[K] W) (x : V) :
    x ∈ LinearMap.ker f ↔ f x = 0 := by
  -- `rfl` で閉じるか確認する．
  -- 解答例: rfl
  sorry

Submodule.map と Submodule.comap の membership を読み替えてください．

example {K V W : Type*} [Field K]
    [AddCommGroup V] [Module K V]
    [AddCommGroup W] [Module K W]
    (f : V →ₗ[K] W) (S : Submodule K V) (y : W) :
    y ∈ Submodule.map f S ↔ ∃ x ∈ S, f x = y := by
  -- `Submodule.mem_map` を調べる．
  -- 解答例: exact Submodule.mem_map
  sorry

線形写像の range が部分空間であることを確認してください．

example {K V W : Type*} [Field K]
    [AddCommGroup V] [Module K V]
    [AddCommGroup W] [Module K W]
    (f : V →ₗ[K] W) :
    Submodule K W :=
  LinearMap.range f