# The full preimage condition determines the quotient topology

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-quotient-topology/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

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



## Goal and scope

Compute a quotient topology for a three-to-two-point surjection and show an open-image failure.

Use the total-surjection quotient convention; the final topology of any total map remains uniquely defined.





## Givens and symbols


- sets
- topology
- definition_here


- G1 — X={a,b,c}, tau_X={empty,{a},X}; Y={u,v}; q(a)=q(c)=u,q(b)=v.


- q — surjective quotient map
- \tau_q — preimage-defined quotient topology





## Rules and sources


- mko_definition · cited — In finite models first qualify q:X→Y as a total surjection and enumerate every fiber. Define tau_q={U⊆Y:q^(-1)(U) is open in X}; enumerate the entire family and verify its topology axioms, continuity of q and the final property: h:Y→Z is continuous if and only if h∘q is continuous. Only saturated open subsets of X can be full preimages of quotient opens; images of arbitrary opens need not be open. For every total map, including a nonsurjection, the defining preimage-if-and-only-if condition still uniquely determines the final topology on Y. Requiring only continuity of q is generally weaker and does not uniquely determine that topology. Unhit points do not invalidate this definition, but under the convention used in this node a nonsurjection is not called a quotient map. · mko-quotient-topology
- sets · prerequisite — Compute unions, intersections, complements, inclusion and preimages element by element.
- topology · prerequisite — A topology contains empty and whole sets and is closed under arbitrary unions and finite intersections; a finite family admits exhaustive checks.
- definition_here · prerequisite — For total surjective q, a quotient subset U is open iff q^{-1}(U) is open; continuity alone requires only open preimages; a fiber is a singleton preimage.





## Main derivation

S01 · impliesBefore

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

After

\tau_X\text{ is a topology}

Conditions: none

Rule: topology · Uses: G1

Leaf basis: topology

The chain with endpoints is union/intersection closed and qualifies the full parent topology.



S02 · impliesBefore

q:X\to Y

After

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

Conditions: none

Rule: sets · Uses: G1

Leaf basis: sets

Every source has a value; the two nonempty fibers partition X, proving total surjectivity.



S03 · definitionBefore

U\subseteq Y

After

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

Conditions: none

Rule: definition_here · Uses: S02

Leaf basis: definition_here

All four subsets of the two-point carrier must undergo the preimage test.



S04 · equivalentBefore

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

After

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

Conditions: none

Rule: sets · Uses: G1, S02, S03

Leaf basis: sets

The middle two are not open; only empty and whole have open preimages.



S05 · definitionBefore

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

After

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

Conditions: none

Rule: definition_here · Uses: S04

Leaf basis: definition_here

The indiscrete two-member family is union/intersection closed, and all its open preimages are already open.



S06 · impliesBefore

O=\{a\}\in\tau_X

After

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

Conditions: none

Rule: sets · Uses: G1, S02, S05

Leaf basis: sets

O is not saturated and its image is not open; full preimages are unions of fibers.



S07 · equivalentBefore

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

After

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

Conditions: none

Rule: sets · Uses: S05

Leaf basis: sets

For any h:Y to Z and each Z-open, the quotient definition makes the continuity tests equivalent.



S08 · equivalentBefore

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

After

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

Conditions: none

Rule: definition_here · Uses: S07, definition_here

Leaf basis: definition_here

Quantifying every W gives the final property; the same preimage iff uniquely specifies a final topology even for nonsurjective total maps.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · inverse_equivalence · S07, definition_here — A nonsurjection fails this node's quotient-map naming convention, not uniqueness of its final topology.
- S07 · inverse_equivalence · S05 — The iff for each W is required, not only one-way continuity of q.
- S06 · premise_audit · G1, S02, S05 — Arbitrary open images are not substituted for the quotient-open definition.
- S05 · premise_audit · S04 — Continuity follows from the full iff definition; continuity alone does not uniquely determine a topology.
- S04 · inverse_equivalence · G1, S02, S03 — The full ambient topology excludes {a,c} and {b}.
- S03 · premise_audit · S02 — The list is exhaustive, not a supplied sample.
- S02 · premise_audit · G1 — Surjectivity for the quotient convention is checked separately, not inferred from continuity.
- S01 · premise_audit · G1 — Not every singleton is assumed open.





## Error controls and negative controls

SaturationAn open image is not automatically quotient-open; test its full fiber-union preimage.

Definition strengthKeep the full iff separate from continuity alone.


- q({a}) must be open. → reject — Its full preimage {a,c} is not open.
- Continuity of q alone uniquely determines the target topology. → reject — For example the identity from a discrete two-point source is continuous for several target topologies.
- Nonsurjectivity prevents the full preimage iff from uniquely defining a final topology. → reject — The iff directly decides openness of every target subset; unhit points do not destroy uniqueness.





## Result and limitations

The quotient topology is {empty,Y}; the image of open {a} is not quotient-open.







## Verification and source binding

0 declared checks for this guide; only the listed expressions are covered.


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: e3acece65d8f1e8503d30855403d0b3e7a114149189059e4a2b0110fc27add3b
- original source SHA-256: 4cd44e2f685149a647ce5fdcb3335184fae51c6359027b3e9726a468797bbf1e
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-quotient-topology-01.json)