English
The Ultrafilter space Ultrafilter X is a projective object in CompHaus for every type X.
Русский
Пространство ультрафильтров Ultrafilter X является проективным объектом в CompHaus для любого типа X.
LaTeX
$$$\forall X,\ \mathrm{Projective}(\mathrm{CompHaus.of}(\mathrm{Ultrafilter}(X)))$$$
Lean4
instance projective_ultrafilter (X : Type*) : Projective (of <| Ultrafilter X) where
factors {Y Z} f g
hg := by
rw [epi_iff_surjective] at hg
obtain ⟨g', hg'⟩ := hg.hasRightInverse
let t : X → Y := g' ∘ f ∘ (pure : X → Ultrafilter X)
let h : Ultrafilter X → Y := Ultrafilter.extend t
have hh : Continuous h := continuous_ultrafilter_extend _
use CompHausLike.ofHom _ ⟨h, hh⟩
apply ConcreteCategory.coe_ext
have : g.hom ∘ g' = id := hg'.comp_eq_id
convert
denseRange_pure.equalizer (g.hom.continuous.comp hh) f.hom.continuous
_
-- This used to be `rw`, but we need `rw; rfl` after https://github.com/leanprover/lean4/pull/2644
rw [comp_assoc, ultrafilter_extend_extends, ← comp_assoc, this, id_comp]
rfl
