Profinite sets have enough projectives #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
In this file we show that
Profinite has enough projectives.
Main results #
X be a profinite set.
For any profinite
X, the natural map
ultrafilter X → X is a projective presentation.