Automatic Quotient and Continuous Descent

Abstract

Compact-to-Hausdorff continuous surjections are automatically closed and quotient, enabling unique continuous descent.

Theorem 1.1 (Compact-to-Hausdorff maps descend continuously).

$$\begin{array}{c}\forall X,B,Y:\mathrm{Type},\\ [\mathrm{TopologicalSpace}\left(X\right)],[\mathrm{TopologicalSpace}\left(B\right)],[\mathrm{TopologicalSpace}\left(Y\right)],\\ [\mathrm{CompactSpace}\left(X\right)],[T2Space\left(B\right)],\\ q:\mathrm{ContinuousMap}\left(X,B\right),\mathrm{Surjective}\left(q\right),\\ T:\mathrm{ContinuousMap}\left(X,Y\right),\mathrm{FactorsThrough}\left(T,q\right)\\ \Rightarrow \mathrm{IsClosedMap}\left(q\right)\wedge \mathrm{IsQuotientMap}\left(q\right)\wedge \\ \exists !factor:\mathrm{ContinuousMap}\left(B,Y\right),T=factor\circ q.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Transport/CompactHausdorffDescent.compact_hausdorff_automatic_quotient (✓ std3). ∎

Source. Repository-derived.

Commentary.

The source is compact, the intermediate space is Hausdorff, and q is a continuous surjection. The conclusion exposes both closedness and quotientness of q.

The continuous map T is constant on q-fibers. The imported continuous-descent theorem then constructs the unique continuous factor through q.

References

• Truth anchor: D5/S3/ConceptDynamics/Transport/CompactHausdorffDescent.compact_hausdorff_automatic_quotient
• Dependency: D5/S3/ConceptDynamics/Transport/ContinuousDescent