# mathlibdocumentation

topology.category.Profinite.projective

# Profinite sets have enough projectives #

In this file we show that Profinite has enough projectives.

## Main results #

Let X be a profinite set.

• Profinite.projective_ultrafilter: the space ultrafilter X is a projective object
• Profinite.projective_presentation: the natural map ultrafilter X → X is a projective presentation
@[protected, instance]
def Profinite.projective_ultrafilter (X : Type u) :
noncomputable def Profinite.projective_presentation (X : Profinite) :

For any profinite X, the natural map ultrafilter X → X is a projective presentation.

Equations
@[protected, instance]