CompHaus has enough projectives

In this file we show that CompHaus has enough projectives.

Main results

Let X be a compact Hausdorff space.

• CompHaus.projective_ultrafilter: the space Ultrafilter X is a projective object
• CompHaus.projectivePresentation: the natural map Ultrafilter X → X is a projective presentation

Reference

See [miraglia2006introduction] Chapter 21 for a proof that CompHaus has enough projectives.

instance CompHaus.projective_ultrafilter (X : Type u_1) : CategoryTheory.Projective (of (Ultrafilter X))

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

For any compact Hausdorff space X, the natural map Ultrafilter X → X is a projective presentation.

Equations

• One or more equations did not get rendered due to their size.

instance CompHaus.instEnoughProjectives : CategoryTheory.EnoughProjectives CompHaus