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.projectivePresentation: the natural map Ultrafilter X → X is a projective presentation

instance Profinite.projective_ultrafilter (X : Type u) : CategoryTheory.Projective (of (Ultrafilter X))

def Profinite.projectivePresentation (X : Profinite) : CategoryTheory.ProjectivePresentation X

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

Equations

• One or more equations did not get rendered due to their size.

instance Profinite.instEnoughProjectives : CategoryTheory.EnoughProjectives Profinite