Compact open covered sets

Stream: maths

[Christian Merten]

Does the following have a name or a better description?

import Mathlib
open TopologicalSpace

/-- A set `U` of `S` is compact open covered by a family of maps `X i → S`,
if it is the finite union of images of compact and open sets of the `X i`. -/
def IsCompactOpenCovered {S ι : Type*} {X : ι → Type*} (f : ∀ i, X i → S)
    [∀ i, TopologicalSpace (X i)] (U : Set S) : Prop :=
  ∃ (s : Set ι) (_ : s.Finite) (V : ∀ i ∈ s, Opens (X i)),
    (∀ (i : ι) (h : i ∈ s), IsCompact (V i h).1) ∧
    ⋃ (i : ι) (h : i ∈ s), (f i) '' (V i h) = U

For context: I am defining the fpqc topology on schemes. For this I defined a predicate Cover.QuasiCompact on docs#AlgebraicGeometry.Scheme.Cover where the condition is that every compact open is IsCompactOpenCovered by the maps of the cover (this is equivalent to the stacks project definition linked above, because affine opens form a basis).

[Andrew Yang]

If your U is compact, then you can probably drop s and demand one V on each ι?

[Christian Merten]

No, because the f i might not be open maps (in fact, in the fpqc case, they won't be).

[Christian Merten]

(IsCompactOpenCovered U is even automatic for U compact open if all the f i are open maps)

[Andrew Yang]

I wonder if it is easier to say that $\amalg X_i =: X \to S$ is fpqc, i.e. every $x \in X$ has a compact neighborhood whose image is affine.

[Christian Merten]

Andrew Yang said:

I wonder if it is easier to say that $\amalg X_i =: X \to S$ is fpqc, i.e. every $x \in X$ has a compact neighborhood whose image is affine.

My plan is to get this as an equivalent description and my guess is that we want both characterizations anyway.

[Andrew Yang]

I feel like the "better description" you are looking for is a topological version of the above (replace coprod with disjoint union and affine with compact and some more modifications)

[Christian Merten]

So you are suggesting this?

import Mathlib
open TopologicalSpace

def IsCompactOpenCovered' {S ι : Type*} {X : ι → Type*} (f : ∀ i, X i → S)
    [∀ i, TopologicalSpace (X i)] (U : Set S) : Prop :=
  ∃ (V : Opens (Σ i, X i)), IsCompact V.1 ∧ (fun p ↦ f p.1 p.2) '' V.1 = U

[Andrew Yang]

I guess the question I should ask is: do you really need a family of covers when you are developing api for it or is it enough to consider the cover with one component?

[Andrew Yang]

It would be useful to have them as characterizations to apply to actual covers in practice but for the abstract theory do you need anything more?

[Christian Merten]

We need a definition of "quasicompact" for arbitrary covers, because we need to be able to talk about fpqc covers that are not given by a single morphism (e.g. Zariski covers). And also to develop the basic API for how quasicompact behaves under pullback, refinement etc. we need the statements for arbitrary covers.