CompHaus has 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 CompHaus has enough projectives.
Main results #
Let X be a compact Hausdorff space.
CompHaus.projective_ultrafilter: the spaceultrafilter Xis a projective objectCompHaus.projective_presentation: the natural mapultrafilter X → Xis a projective presentation
Reference #
See [Mir06] Chapter 21 for a proof that CompHaus has enough projectives.
@[protected, instance]
For any compact Hausdorff space X,
the natural map ultrafilter X → X is a projective presentation.
Equations
- X.projective_presentation = {P := CompHaus.of (ultrafilter ↥X) _, projective := _, f := {to_fun := ultrafilter.extend id, continuous_to_fun := _}, epi := _}
@[protected, instance]