Compact open covered sets

In this file we define the notion of a compact-open covered set with respect to a family of maps fᵢ : X i → S. A set U is compact-open covered by the family fᵢ if it is the finite union of images of compact open sets in the X i.

This notion is not interesting, if the fᵢ are open maps (see IsCompactOpenCovered.of_isOpenMap).

This is used to define the fpqc topology of schemes, there a cover is given by a family of flat morphisms such that every compact open is compact-open covered.

Main results

• IsCompactOpenCovered.of_isOpenMap: If all the fᵢ are open maps, then every compact open of S is compact-open covered.

def IsCompactOpenCovered {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} (f : (i : ι) → X i → S) [(i : ι) → TopologicalSpace (X i)] (U : Set S) : Prop

A set U is compact-open covered by the family fᵢ : X i → S, if U is the finite union of images of compact open sets in the X i.

Equations

• One or more equations did not get rendered due to their size.

theorem IsCompactOpenCovered.empty {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [(i : ι) → TopologicalSpace (X i)] : IsCompactOpenCovered f ∅

theorem IsCompactOpenCovered.iff_of_unique {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [(i : ι) → TopologicalSpace (X i)] {U : Set S} [Unique ι] : IsCompactOpenCovered f U ↔ ∃ (V : TopologicalSpace.Opens (X default)), IsCompact V.carrier ∧ f default '' V.carrier = U

theorem IsCompactOpenCovered.id_iff_isOpen_and_isCompact {S : Type u_1} {U : Set S} [TopologicalSpace S] : IsCompactOpenCovered (fun (x : Unit) => id) U ↔ IsOpen U ∧ IsCompact U

theorem IsCompactOpenCovered.iff_isCompactOpenCovered_sigmaMk {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [(i : ι) → TopologicalSpace (X i)] {U : Set S} : IsCompactOpenCovered f U ↔ IsCompactOpenCovered (fun (x : Unit) (p : (i : ι) × X i) => f p.fst p.snd) U

theorem IsCompactOpenCovered.of_iUnion_eq_of_finite {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [(i : ι) → TopologicalSpace (X i)] {U : Set S} (s : Set (Set S)) (hs : ⋃ t ∈ s, t = U) (hf : s.Finite) (H : ∀ t ∈ s, IsCompactOpenCovered f t) : IsCompactOpenCovered f U

theorem IsCompactOpenCovered.exists_mem_of_isBasis {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [(i : ι) → TopologicalSpace (X i)] {B : (i : ι) → Set (TopologicalSpace.Opens (X i))} (hB : ∀ (i : ι), TopologicalSpace.Opens.IsBasis (B i)) (hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier) {U : Set S} (hU : IsCompactOpenCovered f U) : ∃ (n : ℕ) (a : Fin n → ι) (V : (i : Fin n) → TopologicalSpace.Opens (X (a i))), (∀ (i : Fin n), V i ∈ B (a i)) ∧ ⋃ (i : Fin n), f (a i) '' ↑(V i) = U

If U is compact-open covered and the X i have a basis of compact opens, U can be written as the union of images of elements of the basis.

theorem IsCompactOpenCovered.of_isOpenMap {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [(i : ι) → TopologicalSpace (X i)] [TopologicalSpace S] [∀ (i : ι), PrespectralSpace (X i)] (hfc : ∀ (i : ι), Continuous (f i)) (h : ∀ (i : ι), IsOpenMap (f i)) {U : Set S} (hs : ∀ x ∈ U, ∃ (i : ι) (y : X i), f i y = x) (hU : IsOpen U) (hc : IsCompact U) : IsCompactOpenCovered f U