# 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.

@[protected, instance]
def CompHaus.projective_ultrafilter (X : Type u_1) :
noncomputable def CompHaus.projective_presentation (X : CompHaus) :

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

Equations
@[protected, instance]