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 (Profinite.of (Ultrafilter X))

Equations

• ⋯ = ⋯

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

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

Equations

• Profinite.projectivePresentation X = CategoryTheory.ProjectivePresentation.mk (Profinite.of (Ultrafilter ↑X.toCompHaus.toTop)) { toFun := Ultrafilter.extend id, continuous_toFun := ⋯ }

instance Profinite.instEnoughProjectivesProfiniteCategory : CategoryTheory.EnoughProjectives Profinite

Equations

• Profinite.instEnoughProjectivesProfiniteCategory = ⋯