English
If X is a compact Hausdorff space that is projective (in CompHaus), then its underlying topological space X.toTop.carrier is extremally disconnected.
Русский
Если X — компактно-гаммфтовое пространство над которым реализована проективность в категории CompHaus, то основанное на нём топологическое пространство X.toTop.carrier является экстремально неразложимым.
LaTeX
$$$\text{ExtremallyDisconnected}(X^{\text{top}})\quad\text{for }X:\text{CompHaus with }\text{Projective }X$$$
Lean4
/-- `Projective` implies `ExtremallyDisconnected`. -/
instance (X : CompHaus.{u}) [Projective X] : ExtremallyDisconnected X :=
by
apply CompactT2.Projective.extremallyDisconnected
intro A B _ _ _ _ _ _ f g hf hg hsurj
let A' : CompHaus := CompHaus.of A
let B' : CompHaus := CompHaus.of B
let f' : X ⟶ B' := CompHausLike.ofHom _ ⟨f, hf⟩
let g' : A' ⟶ B' := CompHausLike.ofHom _ ⟨g, hg⟩
have : Epi g' := by
rw [CompHaus.epi_iff_surjective]
assumption
obtain ⟨h, hh⟩ := Projective.factors f' g'
refine ⟨h, h.hom.2, ?_⟩
ext t
apply_fun (fun e => e t) at hh
exact hh
