English
The ultrafilter case provides projectivity: Ultrafilter objects are projective in Profinite, via a concrete explicit construction.
Русский
Расширенный случай ультрафильтра обеспечивает проективность: объекты Ultrafilter являются проективными в Profinite, с явной конструкцией.
LaTeX
$$$\\text{Projective}(\\mathrm{of}(\\mathrm{Ultrafilter}\\; X))$$$
Lean4
instance projective_ultrafilter (X : Type u) : 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
simp only [h]
convert denseRange_pure.equalizer (g.hom.continuous.comp hh) f.hom.continuous _
have : g.hom ∘ g' = id := hg'.comp_eq_id
rw [comp_assoc, ultrafilter_extend_extends, ← comp_assoc, this, id_comp]
rfl
