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 #
Let X be a profinite set.
Profinite.projective_ultrafilter: the spaceultrafilter Xis a projective objectProfinite.projective_presentation: the natural mapultrafilter X → Xis a projective presentation
@[protected, instance]
For any profinite X, the natural map ultrafilter X → X is a projective presentation.
Equations
- X.projective_presentation = {P := Profinite.of (ultrafilter ↥X) _, projective := _, f := {to_fun := ultrafilter.extend id, continuous_to_fun := _}, epi := _}
@[protected, instance]