English
Theorem: In a compact, Hausdorff space, extremal disconnectedness implies projectivity.
Русский
Теорема: в компактном Хаусдорфовом пространстве экстремальная разобщенность влечет за собой проективность.
LaTeX
$$$$ \\text{If } X \\text{ is extremally disconnected, then } CompactT2.Projective X. $$$$
Lean4
/-- Theorem 2.5 in [Gleason, *Projective topological spaces*][gleason1958]:
in the category of compact spaces and continuous maps,
the projective spaces are precisely the extremally disconnected spaces. -/
protected theorem projective [ExtremallyDisconnected A] [CompactSpace A] [T2Space A] : CompactT2.Projective A := by
-- let $B$ and $C$ be compact; let $f : B \twoheadrightarrow C$ and $\phi : A \to C$ be continuous
intro B C _ _ _ _ _ _ φ f φ_cont f_cont f_surj
let D : Set <| A × B := {x | φ x.fst = f x.snd}
have D_comp : CompactSpace D :=
isCompact_iff_compactSpace.mp (isClosed_eq (φ_cont.comp continuous_fst) (f_cont.comp continuous_snd)).isCompact
let X₁ : D → A := Prod.fst ∘ Subtype.val
have X₁_cont : Continuous X₁ := continuous_fst.comp continuous_subtype_val
have X₁_surj : X₁.Surjective := fun a => ⟨⟨⟨a, _⟩, (f_surj <| φ a).choose_spec.symm⟩, rfl⟩
rcases exists_compact_surjective_zorn_subset X₁_cont X₁_surj with
⟨E, _, E_onto, E_min⟩
-- apply Lemma 2.3 to get homeomorphism $\pi_1|_E : E \to A$
let ρ : E → A := E.restrict X₁
have ρ_cont : Continuous ρ := X₁_cont.continuousOn.restrict
have ρ_surj : ρ.Surjective := fun a => by rcases (E_onto ▸ mem_univ a : a ∈ X₁ '' E) with ⟨d, ⟨hd, rfl⟩⟩;
exact ⟨⟨d, hd⟩, rfl⟩
let ρ' := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
let X₂ : D → B := Prod.snd ∘ Subtype.val
have X₂_cont : Continuous X₂ := continuous_snd.comp continuous_subtype_val
refine ⟨E.restrict X₂ ∘ ρ'.symm, ⟨X₂_cont.continuousOn.restrict.comp ρ'.symm.continuous, ?_⟩⟩
suffices f ∘ E.restrict X₂ = φ ∘ ρ' by rw [← comp_assoc, this, comp_assoc, Homeomorph.self_comp_symm, comp_id]
ext x
exact x.val.mem.symm
