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.projective_presentation: 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

• (_ : CategoryTheory.Projective (CompHaus.of (Ultrafilter X))) = (_ : CategoryTheory.Projective (CompHaus.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

• CompHaus.projectivePresentation X = CategoryTheory.ProjectivePresentation.mk (CompHaus.of (Ultrafilter ↑X.toTop)) (ContinuousMap.mk (Ultrafilter.extend id))

instance CompHaus.instEnoughProjectivesCompHausCategory : CategoryTheory.EnoughProjectives CompHaus

Equations

• CompHaus.instEnoughProjectivesCompHausCategory = (_ : CategoryTheory.EnoughProjectives CompHaus)