finite covers

Stream: maths

[Floris van Doorn]

I want to formalize the following theorem:

Given a finite open cover Uᵢ of a compact set K, there exists a compact sets Kᵢ ⊆ Uᵢ such that K = ⋃ᵢ Kᵢ (in a T2 space)

I don't really know how to formulate it in the most convenient way. There are many ways we can formulate a finite collection of things:
(1) U : ι → opens α with [fintype ι]
(2) U : t → opens α for (t : finset ι)
(3) U : fin n → opens α
(4) U : finset (opens α)
(5) U : multiset (opens α)
(6) U : finsupp ι (opens α)
(7) U : ι → opens α and (t : finset ι) (ignoring all values outside t)
among others... (we can also use set α + is_open hypothesis, but I don't really care about that now)

However, not all of them are equally convenient:

• I need to relate K i and U i. This is ugly with (4) and (5).
• I want to apply it in a situation where U might not be injective. This is not possible with (4).
• In the proof, I want to do induction on the number of sets. This is hard with (1), and (6) (for (6), there is finsupp.induction, but it's formulated only for monoids. I'm wondering about the boilerplate needed to use that opens are a monoid under unions)
• I want to talk about unions of K i and U i, and would like library support. This doesn't exist/is limited for I think (2), (3), (5) and (6) (with (2) the problem is that the function U depends on the hypothesis i ∈ t in contrast to all bUnion lemmas)
• (7) is problematic, because K i is only nicely defined when i ∈ t, so K needs to have the type of (2) (resulting in the same problems). Or you define K i to be empty outside t, but I'm not sure if that is convenient.

I have actually already proved it for (4), but it was not pretty. Furthermore, when I apply my lemma, I have a U as in situation (2), and it would require some extra reasoning in the (stupid) case that U is non-injective.

[Floris van Doorn]

Here is my code for (4):

import topology.opens

open set topological_space

variables {α : Type*} [topological_space α]

/-- The compact sets of a topological space. See also `nonempty_compacts`. -/
def compacts (α : Type*) [topological_space α] : set (set α) := { s : set α | compact s }

instance compacts.has_emptc : has_emptyc (compacts α) :=
⟨⟨∅, compact_empty⟩⟩

@[simp] lemma compacts.empty_val : (∅ : compacts α).1 = ∅ := rfl

lemma diff_inter_diff {s t u : set α} : s \ t ∩ (s \ u) = s \ (t ∪ u) :=
by { ext x, simp only [mem_inter_eq, mem_union_eq, mem_diff], tauto }

/-- If a compact set is covered by two open sets, then we can cover it by two compact subsets. -/
lemma compact.binary_compact_cover [t2_space α] {K U V : set α} (hK : compact K)
  (hU : is_open U) (hV : is_open V) (h2K : K ⊆ U ∪ V) :
  ∃ K₁ K₂ : set α, compact K₁ ∧ compact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂ :=
begin
  rcases compact_compact_separated (compact_diff hK hU) (compact_diff hK hV)
    (by rwa [diff_inter_diff, diff_eq_empty]) with ⟨O₁, O₂, h1O₁, h1O₂, h2O₁, h2O₂, hO⟩,
  refine ⟨_, _, compact_diff hK h1O₁, compact_diff hK h1O₂,
    by rwa [diff_subset_comm], by rwa [diff_subset_comm], by rw [← diff_inter, hO, diff_empty]⟩
end

/-- For every finite open cover `Uᵢ` of a compact set, there exists a compact cover `Kᵢ ⊆ Uᵢ`. -/
lemma compact.finite_compact_cover' [t2_space α] {s : set α} (hs : compact s)
  (C : finset (opens α)) (hsC : s ⊆ ⋃ (U ∈ C), (U : opens α).1) :
  ∃ K : {s // s ∈ C } → compacts α, (∀ U, (K U).1 ⊆ U.1) ∧ s = ⋃ i, (K i).1 :=
begin
  classical, revert s hs hsC,
  refine finset.induction _ _ C,
  { intros, refine ⟨λ _, ∅, λ U, empty_subset _, _⟩,
    simpa only [subset_empty_iff, finset.not_mem_empty, Union_neg, Union_empty, not_false_iff,
      compacts.empty_val] using hsC },
  { intros U C hU ih s hs hsC, simp only [finset.bUnion_insert] at hsC,
    rcases hs.binary_compact_cover U.2 (is_open_bUnion $ λ U (h : U ∈ C), (U : opens α).2) hsC
      with ⟨K₁, K₂, h1K₁, h1K₂, h2K₁, h2K₂, hK⟩,
    rcases ih h1K₂ h2K₂ with ⟨K, h1K, h2K⟩,
    refine ⟨λ x, if h : x.1 ∈ C then K ⟨x, h⟩ else ⟨K₁, h1K₁⟩, _, _⟩,
    { rintro ⟨V, hV⟩, simp only [subtype.coe_mk], dsimp only,
      simp only [finset.mem_insert] at hV, rcases hV with rfl|h2V,
      simpa only [dif_neg hU] using h2K₁, simp only [dif_pos, h2V], apply h1K },
    { ext x, simp only [mem_Union, subtype.exists, subtype.coe_mk, hK],
      split,
      { rintro (hx|hx),
        exact ⟨U, by simp only [true_or, eq_self_iff_true, finset.mem_insert],
          by simp only [dif_neg hU, hx]⟩,
        simp only [h2K, mem_Union, subtype.exists] at hx, rcases hx with ⟨V, h1V, h2V⟩,
        refine ⟨V, by simp only [h1V, or_true, finset.mem_insert], _⟩,
        dsimp only, simp only [h1V, dif_pos, h2V] },
      { rintro ⟨V, h1V, h2V⟩, simp only [finset.mem_insert] at h1V,
        rcases h1V with rfl|h3V, simp only [dif_neg hU] at h2V, exact or.inl h2V,
        simp only [dif_pos h3V] at h2V,
        simp only [h2K, mem_Union, subtype.exists, mem_union_eq], exact or.inr ⟨V, h3V, h2V⟩ }}}
end

[Floris van Doorn]

Thinking about it again, (7) might be the most convenient way after all.

[Johan Commelin]

@Floris van Doorn I would guess (1) or (7).

[Johan Commelin]

There is already a small API to do induction in the setting of (1). I think we should just create fintype.induction and flesh it out a bit more.

[Scott Morrison]

I was about to say the same.

[Mario Carneiro]

There are also already some theorems like this about compact sets IIRC

[Mario Carneiro]

src#compact.elim_finite_subcover

[Floris van Doorn]

I tried (7) now, and it's working a lot nicer than I thought. Setting K i empty outside t is not as much hassle as I thought.

It would be nice to have induction for fintypes, but I'm not sure how to get that in a nice way (without univalence)

Yes, I saw these properties Mario. I don't think there is anything similar to this statement though.

[Mario Carneiro]

true, your particular statement about T2 spaces is not proven

[Mario Carneiro]

It is worth noting that the linked statement uses finset (set A) with the assumption that all sets are open. Do we have finset (opens A) versions of these statements? Or should we stick to using finset (set A)?

[Floris van Doorn]

I don't think there is a are versions of compact.elim_finite_subcover that use opens.
I could change my version to also the set _ instead of opens _/compacts _. The glue between the two different versions is very minimal though.

[Reid Barton]

By the way, I think you should formalize this version of the statement instead: https://ncatlab.org/nlab/show/shrinking+lemma#ShrinkinglemmaForFiniteCovers

[Reid Barton]

Oh, I even wrote it down in https://github.com/leanprover-community/mathlib/blob/master/roadmap/topology/shrinking_lemma.lean

[Kevin Buzzard]

Roadmaps should be more widely used and more widely known.

[Kevin Buzzard]

@Patrick Massot I think beginning to formalise a roadmap for sphere eversion would be very cool. I have been telling PhD students at Imperial "oh, go formalise DVRs". I think that a better approach would have been to start on a roadmap.

[Patrick Massot]

Scott started doing that for one lemma, and I certainly intend to do it much more. But I'd like to empty some of my PR backlog first before it gets too outdated.

[Reid Barton]

Oops I didn't look closely enough at what I wrote earlier, and it is the general locally finite version. I really had in mind just generalizing the hypotheses of Floris's statement to a normal space with appropriate adjustments to the conclusion. But maybe what I said is true anyways.

[Floris van Doorn]

@Reid Barton that lemma also would be nice to have, but it's not what I need right now, since I don't want to assume more separatedness than T2.

[Reid Barton]

Compact Hausdorff spaces are also normal, but now maybe this is getting a bit awkward for your use case...