English
For compact Hausdorff spaces A, projective property is equivalent to extremal disconnectedness.
Русский
Для компактно-гладких (компактных Хазерообразных) пространств A свойство проективности эквивалентно экстремально разобщенности.
LaTeX
$$$$ [CompactSpace A] \\land [T2Space A] \\Rightarrow (CompactT2.Projective A) \\leftrightarrow (ExtremallyDisconnected A). $$$$
Lean4
protected theorem extremallyDisconnected [CompactSpace X] [T2Space X] (h : CompactT2.Projective X) :
ExtremallyDisconnected X := by
refine { open_closure := fun U hU => ?_ }
let Z₁ : Set (X × Bool) := Uᶜ ×ˢ { true }
let Z₂ : Set (X × Bool) := closure U ×ˢ { false }
let Z : Set (X × Bool) := Z₁ ∪ Z₂
have hZ₁₂ : Disjoint Z₁ Z₂ := disjoint_left.2 fun x hx₁ hx₂ => by cases hx₁.2.symm.trans hx₂.2
have hZ₁ : IsClosed Z₁ := hU.isClosed_compl.prod (T1Space.t1 _)
have hZ₂ : IsClosed Z₂ := isClosed_closure.prod (T1Space.t1 false)
have hZ : IsClosed Z := hZ₁.union hZ₂
let f : Z → X := Prod.fst ∘ Subtype.val
have f_cont : Continuous f := continuous_fst.comp continuous_subtype_val
have f_sur : Surjective f := by
intro x
by_cases hx : x ∈ U
· exact ⟨⟨(x, false), Or.inr ⟨subset_closure hx, mem_singleton _⟩⟩, rfl⟩
· exact ⟨⟨(x, true), Or.inl ⟨hx, mem_singleton _⟩⟩, rfl⟩
haveI : CompactSpace Z := isCompact_iff_compactSpace.mp hZ.isCompact
obtain ⟨g, hg, g_sec⟩ := h continuous_id f_cont f_sur
let φ := Subtype.val ∘ g
have hφ : Continuous φ := continuous_subtype_val.comp hg
have hφ₁ : ∀ x, (φ x).1 = x := congr_fun g_sec
suffices closure U = φ ⁻¹' Z₂
by
rw [this, preimage_comp, ← isClosed_compl_iff, ← preimage_compl, ← preimage_subtype_coe_eq_compl Subset.rfl]
· exact hZ₁.preimage hφ
· rw [hZ₁₂.inter_eq, inter_empty]
refine (closure_minimal ?_ <| hZ₂.preimage hφ).antisymm fun x hx => ?_
· intro x hx
have : φ x ∈ Z₁ ∪ Z₂ := (g x).2
rcases this with hφ | hφ
· exact ((hφ₁ x ▸ hφ.1) hx).elim
· exact hφ
· rw [← hφ₁ x]
exact hx.1
