長めの例: 標準基底が `K × K` を張る¶

次に，e₁ = (1, 0) と e₂ = (0, 1) が K × K 全体を張ることを示します．ここでは Basis を作るのではなく，まず Submodule.span だけを使います．

証明の中心は，任意の p : K × K について

p = p.1 • e₁ + p.2 • e₂

を示すことです．

def planeE1 : K × K :=
  (1, 0)

def planeE2 : K × K :=
  (0, 1)

example : Submodule.span K ({planeE1, planeE2} : Set (K × K)) = ⊤ := by
  ext p
  constructor
  · intro _
    trivial
  · intro _
    have hp : p = p.1 • planeE1 + p.2 • planeE2 := by
      ext <;> simp [planeE1, planeE2]
    rw [hp]
    apply Submodule.add_mem
    · exact Submodule.smul_mem _ _ (Submodule.subset_span (by simp [planeE1]))
    · exact Submodule.smul_mem _ _ (Submodule.subset_span (by simp [planeE2]))

end CoordinateLinearMaps

この例では ext p で部分空間の等式を元ごとの同値に変換しています．その後，⊤ への所属は自明なので，全ての p が左辺の span に入ることを示せば十分です．

このような proof は，線形代数の形式化で頻繁に使う基本パターンです．

span に生成元が入る: Submodule.subset_span
span がスカラー倍で閉じる: Submodule.smul_mem
span が和で閉じる: Submodule.add_mem
座標計算: ext と simp

演習問題¶

K × K 上の線形写像 (x, y) ↦ x - y を LinearMap として作ってください．

def diffPairLinear {K : Type*} [Field K] : (K × K) →ₗ[K] K where
  toFun p := p.1 - p.2
  map_add' := by
    -- 座標計算．
    -- 解答例:
    --   intro x y
    --   simp [sub_eq_add_neg, add_assoc, add_comm, add_left_comm]
    sorry
  map_smul' := by
    -- スカラー倍の分配法則．
    -- 解答例:
    --   intro a x
    --   simp [mul_sub]
    sorry

sumPairLinear の kernel が x + y = 0 であることを，rfl ではなく simp で証明してください．

example {K : Type*} [Field K] (x y : K) :
    (x, y) ∈ LinearMap.ker (sumPairLinear : (K × K) →ₗ[K] K) ↔ x + y = 0 := by
  -- `show` でゴールを見てから `simp [sumPairLinear]` を試す．
  -- 解答例: simpa [sumPairLinear]
  sorry

planeE1 と planeE2 が一次独立であることを示してください．これは少し難しい問題です．まず #check LinearIndependent で statement の形を確認してください．

example {K : Type*} [Field K] :
    LinearIndependent K (fun i : Fin 2 =>
      if i = 0 then (planeE1 : K × K) else planeE2) := by
  -- 方針: `linearIndependent_iff` 系の補題を探す．
  -- 解答例:
  --   rw [linearIndependent_iff]
  --   intro s hzero
  --   ext i
  --   fin_cases i
  --   · have h1 := congrArg Prod.fst hzero
  --     simp [Finsupp.linearCombination, planeE1, planeE2, Finsupp.sum_fintype] at h1
  --     simpa using h1
  --   · have h2 := congrArg Prod.snd hzero
  --     simp [Finsupp.linearCombination, planeE1, planeE2, Finsupp.sum_fintype] at h2
  --     simpa using h2
  sorry

K × K の任意の点を planeE1 と planeE2 の線形結合として書いてください．

example {K : Type*} [Field K] (p : K × K) :
    p = p.1 • planeE1 + p.2 • planeE2 := by
  -- ヒント: `ext <;> simp [planeE1, planeE2]`
  -- 解答例: ext <;> simp [planeE1, planeE2]
  sorry

長めの例: 標準基底が K × K を張る¶

演習問題¶

長めの例: 標準基底が `K × K` を張る¶