# 完整逆像條件決定商拓撲

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-quotient-topology/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-quotient-topology-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

由三點到兩點的滿射計算商拓撲與開像失敗。

本例採 total surjection 的商映射慣例；一般 total map 的 final topology 仍唯一。





## 已知條件與符號


- sets
- topology
- definition_here


- G1 — X={a,b,c}, tau_X={空集,{a},X}; Y={u,v}; q(a)=q(c)=u,q(b)=v。


- q — 滿射商映射
- \tau_q — 逆像定義的商拓撲





## 規則與來源


- mko_definition · cited — finite models先驗q為total surjection並完整列出fibers。定義tau_q={U⊆Y:q^{-1}(U)∈tau_X}，直接枚舉並驗拓撲公理、q的連續性與final-property：h:Y→Z連續當且僅當h∘q連續。只有saturated open subsets of X能作商開集的完整逆像；直接取open images一般錯誤。對任何total map（含非滿射），上述完整逆像的「當且僅當」條件仍唯一決定Y上的final topology；只有要求q連續則通常不唯一。未被命中的點不妨礙preimage-iff定義，但依此節點採用的慣例，非滿射q不稱為quotient map。 · mko-quotient-topology
- sets · prerequisite — 集合的聯、交、補集、包含與函數逆像以逐元素定義計算。
- topology · prerequisite — 拓撲含空集與全集，對任意聯及有限交封閉；有限集合族可完整核對。
- definition_here · prerequisite — 滿射 total q 的商拓撲以 U 開 iff q^{-1}(U) 開定義；連續性只要求正向開集逆像條件；fiber 是單點逆像。





## 逐步主鏈

S01 · implies操作前

\varnothing\subset\{a\}\subset X

操作後

\tau_X\text{ is a topology}

條件：無

規則：topology · 依賴：G1

葉節點依據：topology

含兩端鏈對聯交封閉，完整母拓撲合法。



S02 · implies操作前

q:X\to Y

操作後

q^{-1}(\{u\})=\{a,c\},\quad q^{-1}(\{v\})=\{b\}

條件：無

規則：sets · 依賴：G1

葉節點依據：sets

三個來源各有值，兩個 fiber 非空且分割 X，故 q 是 total surjection。



S03 · definition操作前

U\subseteq Y

操作後

U\in\{\varnothing,\{u\},\{v\},Y\}

條件：無

規則：definition_here · 依賴：S02

葉節點依據：definition_here

兩點載體的全部四個子集都須測逆像。



S04 · equivalent操作前

q^{-1}(\varnothing),q^{-1}(\{u\}),q^{-1}(\{v\}),q^{-1}(Y)

操作後

\varnothing,\{a,c\},\{b\},X

條件：無

規則：sets · 依賴：G1, S02, S03

葉節點依據：sets

中間兩項不開，只有空集與全集的逆像開。



S05 · definition操作前

\tau_q=\{U\subseteq Y:q^{-1}(U)\in\tau_X\}

操作後

\tau_q=\{\varnothing,Y\}\text{ is a topology, and }q\text{ continuous}

條件：無

規則：definition_here · 依賴：S04

葉節點依據：definition_here

這個僅含空集與 Y 的兩項開集族對聯、交封閉；其全部開集的逆像已核為開集。



S06 · implies操作前

O=\{a\}\in\tau_X

操作後

q(O)=\{u\}\notin\tau_q,\quad q^{-1}(q(O))=\{a,c\}\ne O

條件：無

規則：sets · 依賴：G1, S02, S05

葉節點依據：sets

O 未飽和，其開像不開；完整逆像一定是 fiber 聯。



S07 · equivalent操作前

W\text{ open in }Z,\quad(q\text{ then }h)^{-1}(W)=q^{-1}(h^{-1}(W))

操作後

h^{-1}(W)\in\tau_q\iff q^{-1}(h^{-1}(W))\in\tau_X

條件：無

規則：sets · 依賴：S05

葉節點依據：sets

對任意 h:Y→Z 及每個 Z 開集，商定義把連續性測試逐項等價化。



S08 · equivalent操作前

\forall W\in\tau_Z\text{ the preceding iff holds}

操作後

h\text{ continuous}\iff h\circ q\text{ continuous}

條件：無

規則：definition_here · 依賴：S07, definition_here

葉節點依據：definition_here

量化全部 W 得 final property；同一逆像 iff 亦唯一決定非滿射 total map 的 final topology。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · inverse_equivalence · S07, definition_here — 非滿射不符合本節 quotient map 命名慣例，但不是 final topology 不唯一。
- S07 · inverse_equivalence · S05 — 需要逐 W 的 iff，不是僅 q 連續的單向條件。
- S06 · premise_audit · G1, S02, S05 — 沒有把任意開像拿來替代商開集定義。
- S05 · premise_audit · S04 — 連續性是完整 iff 定義的後果，不能反過來僅由連續性唯一決定。
- S04 · inverse_equivalence · G1, S02, S03 — 完整母拓撲排除 {a,c} 與 {b}。
- S03 · premise_audit · S02 — 此清單完整，沒有以供給樣本取代。
- S02 · premise_audit · G1 — 商慣例所需滿射已另核，並非從連續性取得。
- S01 · premise_audit · G1 — 未假設所有單點開。





## 錯誤控制與反例

飽和性開像不等於商開；先測完整 fiber 聯的逆像。

定義強度完整 iff 與只要求連續明確分開。


- q({a}) 必開。 → reject — 其完整逆像 {a,c} 不開。
- 只要求 q 連續即唯一決定目標拓撲。 → reject — 例如離散兩點來源的恆等 q 對多種目標拓撲皆連續。
- 非滿射使完整逆像 iff 不能唯一決定 final topology。 → reject — 該 iff 對每個目標子集直接判開性，未命中點也不破壞唯一性。





## 結論與限制

商拓撲為 {空集,Y}；{a} 的開像不是商開集。







## 驗證及來源綁定

0 個本稿宣告算術檢查；只支持所列算式。


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: e3acece65d8f1e8503d30855403d0b3e7a114149189059e4a2b0110fc27add3b
- original source SHA-256: 4cd44e2f685149a647ce5fdcb3335184fae51c6359027b3e9726a468797bbf1e
- 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-topology-01.json)