exists_compact_surjective_zorn_subset

English

Given a continuous surjection X: D → A with A,T1 and D compact, there exists a compact subset E ⊆ D mapping onto A with a Zorn-subset property: for every proper closed E0 ⊂ E, the image X''E0 ≠ A.

Русский

Существует компактное подмножество E ⊆ D, которое образует X(E) = A и удовлетворяет условию Зорна: для каждого замкнутого E0 ⊂ E верно X''E0 ≠ A.

LaTeX

$$$$ \\exists E \\subseteq D,\\; CompactSpace E \\;\\land\\; X''E = univ \\;\\land\\; \\forall E_0 \\subsetneq E, IsClosed E_0 \\rightarrow X''E_0 \\neq univ. $$$$

Lean4

/-- Lemma 2.4 in [Gleason, *Projective topological spaces*][gleason1958]:
a continuous surjection $\pi$ from a compact space $D$ to a Fréchet space $A$ restricts to
a compact subset $E$ of $D$, such that $\pi$ maps $E$ onto $A$ and satisfies the
"Zorn subset condition", where $\pi(E_0) \ne A$ for any proper closed subset $E_0 \subsetneq E$. -/
theorem exists_compact_surjective_zorn_subset [T1Space A] [CompactSpace D] {X : D → A} (X_cont : Continuous X)
    (X_surj : X.Surjective) :
    ∃ E : Set D, CompactSpace E ∧ X '' E = univ ∧ ∀ E₀ : Set E, E₀ ≠ univ → IsClosed E₀ → E.restrict X '' E₀ ≠ univ :=
  by
  -- suffices to apply Zorn's lemma on the subsets of $D$ that are closed and mapped onto $A$

  let S : Set <| Set D := {E : Set D | IsClosed E ∧ X '' E = univ}
  suffices ∀ (C : Set <| Set D) (_ : C ⊆ S) (_ : IsChain (· ⊆ ·) C), ∃ s ∈ S, ∀ c ∈ C, s ⊆ c
    by
    rcases zorn_superset S this with ⟨E, E_min⟩
    obtain ⟨E_closed, E_surj⟩ := E_min.prop
    refine ⟨E, isCompact_iff_compactSpace.mp E_closed.isCompact, E_surj, ?_⟩
    intro E₀ E₀_min E₀_closed
    contrapose! E₀_min
    exact
      eq_univ_of_image_val_eq <|
        E_min.eq_of_subset ⟨E₀_closed.trans E_closed, image_image_val_eq_restrict_image ▸ E₀_min⟩ image_val_subset
  intro C C_sub C_chain
  refine
    ⟨iInter (fun c : C => c), ⟨isClosed_iInter fun ⟨_, h⟩ => (C_sub h).left, ?_⟩, fun c hc _ h =>
      mem_iInter.mp h ⟨c, hc⟩⟩
      -- prove intersection of chain is mapped onto $A$

  by_cases hC : Nonempty C
  · refine
      eq_univ_of_forall fun a =>
        inter_nonempty_iff_exists_left.mp
          ?_
            -- apply Cantor's intersection theorem

    refine
      iInter_inter (ι := C) (X ⁻¹' { a }) _ ▸
        IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _ ?_ (fun c => ?_)
          (fun c => IsClosed.isCompact ?_) (fun c => ?_)
    · replace C_chain : IsChain (· ⊇ ·) C := C_chain.symm
      have : ∀ s t : Set D, s ⊇ t → _ ⊇ _ := fun _ _ => inter_subset_inter_left <| X ⁻¹' { a }
      exact (directedOn_iff_directed.mp C_chain.directedOn).mono_comp (· ⊇ ·) this
    · rw [← image_inter_nonempty_iff, (C_sub c.mem).right, univ_inter]
      exact singleton_nonempty a
    all_goals exact (C_sub c.mem).left.inter <| (T1Space.t1 a).preimage X_cont
  · rw [@iInter_of_empty _ _ <| not_nonempty_iff.mp hC, image_univ_of_surjective X_surj]

Похожие утверждения