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 (CompHaus.of (Ultrafilter X))

Equations

• ⋯ = ⋯

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

• X.projectivePresentation = CategoryTheory.ProjectivePresentation.mk (CompHaus.of (Ultrafilter ↑X.toTop)) { toFun := Ultrafilter.extend id, continuous_toFun := ⋯ }

instance CompHaus.instEnoughProjectives : CategoryTheory.EnoughProjectives CompHaus

Equations

• CompHaus.instEnoughProjectives = ⋯