# 對角線的商空間 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-quotient-vector-space/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-quotient-vector-space-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 R²/span{(1,1)}的基底為[(0,1)]，維度1；零coset是整條對角線。 有限維實商空間的完整等價與良定性；不談拓撲商。 ## 已知條件與符號 - calc - G1 — V=R²，W={t(1,1):t∈R}；[v]=v+W，q(x,y)=y−x。 - [v] — 完整coset - q — coset標籤y−x - b — (0,1)基底代表 ## 規則與來源 - calc · prerequisite — 假設通常實數域與座標向量運算、矩陣乘法、線性獨立及生成的定義；所用消去均為可逆初等列運算。 - mko_definition · cited — v與u代表同一coset恰當v-u在W；quotient元素是cosets而非唯一representatives。核[v]+[u]=[v+u]與lambda[v]=[lambda v]的代表元獨立性。有限維時dim(V/W)=dimV-dimW，零coset是W。 · mko-quotient-vector-space ## 逐步主鏈 S01 · implies操作前 W=\{(t,t):t\in\mathbb R\} 操作後 0\in W,\quad(s,s)+(t,t)=(s+t,s+t),\quad\lambda(t,t)=(\lambda t,\lambda t) 條件：無 規則：calc · 依賴：G1 葉節點依據：calc 全稱封閉認證W子空間，非零(1,1)為完整一項基底。 S02 · equivalent操作前 v=(x,y),\quad u=(a,b) 操作後 v-u\in W\iff y-b=x-a\iff q(v)=q(u) 條件：無 規則：calc · 依賴：G1, S01 葉節點依據：calc 兩代表同類恰當q相同，cosets是固定y−x的整條線。 S03 · implies操作前 v'=v+w_1,\quad u'=u+w_2,\quad w_1,w_2\in W 操作後 (v'+u')-(v+u)=w_1+w_2\in W 條件：無 規則：calc · 依賴：G1, S01, S02 葉節點依據：calc 任意代表替換使和只差W元素，商加法良定。 S04 · implies操作前 v'=v+w,\quad w\in W,\quad\lambda\in\mathbb R 操作後 \lambda v'-\lambda v=\lambda w\in W 條件：無 規則：calc · 依賴：G1, S01, S02 葉節點依據：calc 任意實純量仍保持同類，商純量乘法良定。 S05 · implies操作前 [0]=0+W 操作後 [0]=W,\quad[(1,1)]=[(0,0)] 條件：無 規則：mko_definition · 依賴：G1, S01, S02 葉節點依據：mko_definition 零商元素是整個W，不是單元素集合。 S06 · implies操作前 v=(x,y),\quad b=(0,1) 操作後 v-(y-x)b=(x,x)\in W\Rightarrow[v]=(y-x)[b] 條件：無 規則：calc · 依賴：G1, S02, S04 葉節點依據：calc 每個coset都是[b]的實倍數，完整生成。 S07 · implies操作前 \lambda[b]=[0] 操作後 (0,\lambda)\in W\iff\lambda=0 條件：無 規則：calc · 依賴：G1, S01, S04, S05 葉節點依據：calc 對角向量第一座標零則第二也零，因此[b]獨立且非零。 S08 · implies操作前 \{[b]\}\text{ independent and spanning} 操作後 \dim(V/W)=1=2-1=\dim V-\dim W 條件：無 規則：mko_definition · 依賴：G1, S01, S06, S07 葉節點依據：mko_definition 以三個完整基底核此例維度差公式：V兩項，W一項，商一項。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S08 · premise_audit · G1, S01, S06, S07 — 這是實例證書，不把它當抽象一般定理證明。 - S07 · premise_audit · G1, S01, S04, S05 — 非零向量不保證非零coset，此處另核b不在W。 - S06 · premise_audit · G1, S02, S04 — 使用已證良定的商純量乘法，不是數值除法。 - S05 · premise_audit · G1, S01, S02 — 兩個向量代表不相等但差在W，故cosets相等。 - S04 · premise_audit · G1, S01, S02 — 包含λ=0與負純量，無額外限制。 - S03 · premise_audit · G1, S01, S02 — 使用W加法封閉，非只測特定代表。 - S02 · inverse_equivalence · G1, S01 — 雙向等價涵蓋全部實座標，不是有限membership測試。 - S01 · premise_audit · G1 — 先認證子空間才能建立向量商。 ## 錯誤控制與反例 零型別零商元素是W本身，非唯一代表。 雙良定性加法用W封閉，純量用λW⊆W，都須全稱。 - 零coset只有(0,0)。 → reject — 它是W，含全部(t,t)。 - [(1,0)]與[(2,1)]不同。 → reject — 差為(1,1)在W中。 - 每個非零向量代表非零coset。 → reject — (1,1)非零但屬W。 ## 結論與限制 R²/span{(1,1)}的基底為[(0,1)]，維度1；零coset是整條對角線。 ## 驗證及來源綁定 1 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 771c4e584bb1897c89adcfcd5b4e225c158db4a9c6492ad3ea24f5772b21d017 - original source SHA-256: f3cefaafea5ecc2a3034c11fb42fd17ee54ad688f67e38f2f43a3a14ed5f3351 - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-quotient-vector-space-01.json)