mathlibdocumentation

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.

• CompHaus.projective_ultrafilter: the space ultrafilter X is a projective object
• CompHaus.projective_presentation: the natural map ultrafilter X → X is a projective presentation

Reference #

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

@[instance]
def CompHaus.projective_ultrafilter (X : Type u_1) :

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

Equations