mathlib documentation

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.

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

Equations