English
If A is extremally disconnected, compact and T2, then A is projective in the CompactT2 sense.
Русский
Если A экстремально разобщимо, компактно и векторно-относительно T2, то A является проективной в смысле CompactT2.
LaTeX
$$$$ [ExtremallyDisconnected A] \\land [CompactSpace A] \\land [T2Space A] \\Rightarrow CompactT2.Projective A. $$$$
Lean4
theorem projective [DiscreteTopology X] : CompactT2.Projective (StoneCech X) :=
by
intro Y Z _tsY _tsZ _csY _t2Y _csZ _csZ f g hf hg g_sur
let s : Z → Y := fun z => Classical.choose <| g_sur z
have hs : g ∘ s = id := funext fun z => Classical.choose_spec (g_sur z)
let t := s ∘ f ∘ stoneCechUnit
have ht : Continuous t := continuous_of_discreteTopology
let h : StoneCech X → Y := stoneCechExtend ht
have hh : Continuous h := continuous_stoneCechExtend ht
refine ⟨h, hh, denseRange_stoneCechUnit.equalizer (hg.comp hh) hf ?_⟩
rw [comp_assoc, stoneCechExtend_extends ht, ← comp_assoc, hs, id_comp]
