Zulip Chat Archive

Stream: maths

Topic: finite covers


view this post on Zulip Floris van Doorn (Jun 12 2020 at 04:18):

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.

view this post on Zulip Floris van Doorn (Jun 12 2020 at 04:18):

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

view this post on Zulip Floris van Doorn (Jun 12 2020 at 04:28):

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

view this post on Zulip Johan Commelin (Jun 12 2020 at 04:40):

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

view this post on Zulip Johan Commelin (Jun 12 2020 at 04:41):

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.

view this post on Zulip Scott Morrison (Jun 12 2020 at 04:41):

I was about to say the same.

view this post on Zulip Mario Carneiro (Jun 12 2020 at 04:41):

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

view this post on Zulip Mario Carneiro (Jun 12 2020 at 04:43):

src#compact.elim_finite_subcover

view this post on Zulip Floris van Doorn (Jun 12 2020 at 04:55):

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.

view this post on Zulip Mario Carneiro (Jun 12 2020 at 04:57):

true, your particular statement about T2 spaces is not proven

view this post on Zulip Mario Carneiro (Jun 12 2020 at 04:58):

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)?

view this post on Zulip Floris van Doorn (Jun 12 2020 at 05:05):

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.

view this post on Zulip Reid Barton (Jun 12 2020 at 11:26):

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

view this post on Zulip Reid Barton (Jun 12 2020 at 11:27):

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

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 11:27):

Roadmaps should be more widely used and more widely known.

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 11:29):

@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.

view this post on Zulip Patrick Massot (Jun 12 2020 at 12:02):

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.

view this post on Zulip Reid Barton (Jun 12 2020 at 12:14):

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.

view this post on Zulip Floris van Doorn (Jun 12 2020 at 20:34):

@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.

view this post on Zulip Reid Barton (Jun 12 2020 at 20:40):

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


Last updated: May 09 2021 at 10:11 UTC