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} {κ : Type u_4} [Finite κ] (s : κ → Set S) (hs : ⋃ (i : κ), s i = U) (H : ∀ (i : κ), IsCompactOpenCovered f (s i)) : IsCompactOpenCovered f U

theorem IsCompactOpenCovered.of_biUnion_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.of_biUnion_eq_of_isCompact {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [(i : ι) → TopologicalSpace (X i)] [TopologicalSpace S] {U : Set S} (hU : IsCompact U) (s : Set (TopologicalSpace.Opens S)) (hs : ⋃ t ∈ s, ↑t = U) (H : ∀ t ∈ s, IsCompactOpenCovered f ↑t) : IsCompactOpenCovered f U

theorem IsCompactOpenCovered.of_isCompact_of_forall_exists_isCompactOpenCovered {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [(i : ι) → TopologicalSpace (X i)] [TopologicalSpace S] {U : Set S} (hU : IsCompact U) (H : ∀ x ∈ U, ∃ t ⊆ U, x ∈ t ∧ IsOpen t ∧ IsCompactOpenCovered f t) : IsCompactOpenCovered f U

theorem IsCompactOpenCovered.image {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [(i : ι) → TopologicalSpace (X i)] {i : ι} (V : TopologicalSpace.Opens (X i)) (hV : IsCompact ↑V) : IsCompactOpenCovered f (f i '' ↑V)

theorem IsCompactOpenCovered.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} {κ : Type u_4} [Finite κ] (a : κ → ι) (V : (k : κ) → TopologicalSpace.Opens (X (a k))) (hV : ∀ (k : κ), IsCompact (V k).carrier) (hU : ⋃ (k : κ), f (a k) '' ↑(V k) = U) : 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_finite_of_isSpectralMap {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [(i : ι) → TopologicalSpace (X i)] [Finite ι] [TopologicalSpace S] (hf : ∀ (i : ι), IsSpectralMap (f i)) {U : Set S} (hs : ∀ x ∈ U, ∃ (i : ι), x ∈ Set.range (f i)) (hU : IsOpen U) (hc : IsCompact U) : IsCompactOpenCovered f U

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 : ι), x ∈ Set.range (f i)) (hU : IsOpen U) (hc : IsCompact U) : IsCompactOpenCovered f U

theorem IsCompactOpenCovered.of_comp {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), PrespectralSpace (X i)] [TopologicalSpace S] {σ : Type u_4} {Y : σ → Type u_5} [(i : σ) → TopologicalSpace (Y i)] (g : (i : σ) → Y i → S) {a : σ → ι} (t : (i : σ) → Y i → X (a i)) (ht : ∀ (i : σ), Continuous (t i)) (hge : ∀ (i : σ), g i = f (a i) ∘ t i) (hf : ∀ (i : ι), Continuous (f i)) {U : Set S} (ho : IsOpen U) (hU : IsCompactOpenCovered g U) : IsCompactOpenCovered f U

Being compact open covered descends along refinements if the spaces are prespectral.