Documentation

Mathlib.Topology.Category.CompHaus.Projective

CompHaus has enough projectives #

In this file we show that CompHaus has enough projectives.

Main results #

Let X be a compact Hausdorff space.

Reference #

See [Mir06] Chapter 21 for a proof that CompHaus has enough projectives.

For any compact Hausdorff space X, the natural map Ultrafilter X → X is a projective presentation.

Equations
Instances For