mathlib3 documentation

topology.category.CompHaus.projective

CompHaus has enough projectives #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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