Definition of a covering of a topological space?

Stream: mathlib4

[David Loeffler]

Do we currently have a unified definition of what it means for a family of sets in a topological space X to be a covering of X (or of a set in X)?

There seem to be quite a few lemmas (e.g. docs#IsCompact.elim_finite_subcover, docs#quasiSober_of_open_cover, etc) whose names, and docstrings, refer to the notion of "cover", but whose formal statements spell out explicitly what "cover" means. Is this something we should add to mathlib? Or is there already a definition lurking somewhere in the axiomatic theory of covers and sieves under Mathlib.CategoryTheory.Sites?

(This came up in reviewing #21079, which adds further results about covers of topological spaces, which could be more slickly formulated if we had a standard definition of cover.)

[Johan Commelin]

I think it is a good idea to abstract this notion into its own definition with some API around it. But I'm saying that without have tried anything in Lean.

[Andrew Yang]

I mainly used an indexed family of TopologicalSpace.Opens with a proof that the iSup is top. e.g. docs#isEmbedding_iff_of_iSup_eq_top
But I agree we would definitely benefit from a unified API.

[Chris Birkbeck]

Oddly enough we do have docs#HasSeparatingCover and some API for that

[David Loeffler]

There’s a design question here: should a covering be an indexed family of opens, or just a Set (Opens X)? If we build the indexing into the definition then there are universe issues in trying to make sense of “the type of all open covers of X” - probably these issues can be dealt with but it would complicate the API.

[David Loeffler]

@Andrew Yang is there a specific reason why you prefer to work with a separate index type?

[Anatole Dedecker]

Indexed families are in general nicer to work with in my opinion: for example, writing down the pullback of an open cover by a continuous map in the « set of opens » version involves throwing existentials into the mix, which is not the case with the indexed approach.

[Anatole Dedecker]

On top of that, if you naturally have a set of opens, you can just take the inclusion as the corresponding indexed family, while to go the other direction you again have to introduce pointless existentials

[David Loeffler]

Anatole Dedecker said:

Indexed families are in general nicer to work with in my opinion: for example, writing down the pullback of an open cover by a continuous map in the « set of opens » version involves throwing existentials into the mix, which is not the case with the indexed approach.

I don't understand; it looks to me as if defining the pullback of an open cover is about equally difficult (i.e. not absolutely immediate but not terribly difficult either) with the indexed and non-indexed approaches.

[David Loeffler]

Here's the "set-like" version:

/-- A collection of open sets whose union is `X`. -/
structure SOpenCover (α : Type*) [TopologicalSpace α]where
  carrier : Set (Opens α)
  sSup_eq_top' : ⨆ u ∈ carrier, u = ⊤

/-- An open cover is a special kind of set of opens. -/
instance : SetLike (SOpenCover α) (Opens α) :=
  ⟨SOpenCover.carrier, fun _ _ ↦ (SOpenCover.mk.injEq ..).mpr⟩

namespace SOpenCover

variable (U : SOpenCover α)

lemma iSup_eq_top : ⨆ u ∈ U, u = ⊤ := U.sSup_eq_top'

lemma iSup_set_eq_univ : ⋃ u ∈ U, (u : Set α) = univ := by
  simpa [← SetLike.coe_set_eq] using U.iSup_eq_top

def comap {α β : Type*} [TopologicalSpace α] [TopologicalSpace β]
    (f : C(α, β)) (U : SOpenCover β) :
    SOpenCover α :=
  ⟨Opens.comap f '' U, by simp [← preimage_iUnion, iSup_set_eq_univ]⟩

end SOpenCover

and here's the "indexed" version:

/-- An indexed family of open sets whose union is `X`. -/
structure IOpenCover (ι α : Type*) [TopologicalSpace α] where
  toFun : ι → Opens α
  iSup_eq_top' : iSup toFun = ⊤

/-- An open cover is a special kind of function into  opens. -/
instance : FunLike (IOpenCover ι α) ι (Opens α) :=
  ⟨IOpenCover.toFun, fun _ _ ↦ (IOpenCover.mk.injEq ..).mpr⟩

namespace IOpenCover

variable (U : IOpenCover ι α)

lemma iSup_eq_top : ⨆ i, U i = ⊤ := U.iSup_eq_top'

lemma iSup_set_eq_univ : ⋃ i, (U i : Set α) = univ := by
  simpa [← SetLike.coe_set_eq] using U.iSup_eq_top

def comap {α β : Type*} [TopologicalSpace α] [TopologicalSpace β]
    (f : C(α, β)) (U : IOpenCover ι β) :
    IOpenCover ι α :=
  ⟨fun i ↦ Opens.comap f (U i), by simp [← preimage_iUnion, iSup_set_eq_univ]⟩

end IOpenCover

Where are the "pointless existentials"?

[Edward van de Meent]

I'm guessing at the point of turning one into the other

[Christian Merten]

I think Anatole is referring to the existential in Opens.comap f '' U?

[Anatole Dedecker]

The pointless existentials are hidden where you take the image of some set. This is of course completely manageable, but when you need to break everything down it does introduce some annoying rcases.

[Anatole Dedecker]

Note also that in the first verson the simp call has to do the extra work of using docs#Set.biUnion_image (or something like that) to reindex the union

[David Loeffler]

Edward van de Meent said:

I'm guessing at the point of turning one into the other

Trivial one-liner:

def SOpenCover.ofIndexed {α ι : Type*} [TopologicalSpace α] {U : ι → Opens α} (hU : iSup U = ⊤) :
    SOpenCover α :=
  ⟨Set.range U, by simpa only [← sSup_eq_iSup] using hU⟩

[David Loeffler]

I really don't understand the enthusiasm here for indexed families here, to be honest. If someone can give an example of a natural argument which is substantially simpler using the IOpenCover definition than the SOpenCover then I'd be happy to be persuaded.

[Anatole Dedecker]

Very concrete one: imagine that all of our API for open covers was made using sets of opens, and you wanted to prove that a compact space is docs#TotallyBounded in the usual way (e.g not the current mathlib proof using ultrafilters). Since you want to get a finite set of points of your space, it's really natural to consider all the coverings as indexed by your space. With your version, one would first need to consider the set of all balls, then extract a finite subset of balls, and then do the extra step of finding back a center of that ball.

[Anatole Dedecker]

I'm not saying this is hard (it's really not), but it's an extra step.

[Anatole Dedecker]

This does raise another point: I think all of our things that look like coverings are indexed in the current state of Mathlib. E.g docs#IsCompact.elim_finite_subcover, docs#LocallyFinite, docs#BumpCovering (this one is for functions but still)

[Anatole Dedecker]

Ok I guess docs#quasiSober_of_open_cover is your counterexample

[David Loeffler]

I've made a PR #21442 which adds a def IsOpenCover (a predicate on indexed families of opens in a topological space), and refactors a few lemmas in other files to use this. I'd be interested in feedback as to whether this is a reasonable approach.

[Andrew Yang]

Looks nice!
Im not sure if we still want the iSup_eq_top lemmas though.

[David Loeffler]

Andrew Yang said:

Looks nice!
Im not sure if we still want the iSup_eq_top lemmas though.

Sure, I was just waiting to see if there was a consensus in favour of the change before removing the old lemmas. I've pushed a commit deprecating them to the PR (awaiting CI to tell me what breaks downstream).

[Antoine Chambert-Loir]

I just noticed the initial question.

There are two types of coverings that are useful in general topology: open coverings, and locally finite closed coverings. For examples, these two kind of coverings allow to prove that a function is continuous by proving that the restrictions to the covering sets are continuous.

They have a common generalization: take a family $(V_i)_{i\in I}$ of locally closed subsets of a topological space $X$, and say it covers $X$ if for every point $x\in X$, there exists a finite subset $I_x$ of $I$ such that $x\in V_i$ for all $i\in I_x$, and the union of the $V_i$, for $i\in I_x$, is a neighborhood of $x$ in $X$. (This could be called the Grothendieck topology of locally closed subsets.)