Quasi-compact covers

A cover of a scheme is quasi-compact if every affine open of the base can be covered by a finite union of images of quasi-compact opens of the components.

This is used to define the fpqc (faithfully flat, quasi-compact) topology, where covers are given by flat covers that are quasi-compact.

class AlgebraicGeometry.QuasiCompactCover {S : Scheme} (𝒰 : CategoryTheory.PreZeroHypercover S) : Prop

A cover of a scheme is quasi-compact if every affine open of the base can be covered by a finite union of images of quasi-compact opens of the components.

• isCompactOpenCovered_of_isAffineOpen {U : S.Opens} (hU : IsAffineOpen U) : IsCompactOpenCovered (fun (x : 𝒰.I₀) => ⇑(CategoryTheory.ConcreteCategory.hom (𝒰.f x).base)) ↑U

theorem AlgebraicGeometry.quasiCompactCover_iff {S : Scheme} (𝒰 : CategoryTheory.PreZeroHypercover S) : QuasiCompactCover 𝒰 ↔ ∀ {U : S.Opens}, IsAffineOpen U → IsCompactOpenCovered (fun (x : 𝒰.I₀) => ⇑(CategoryTheory.ConcreteCategory.hom (𝒰.f x).base)) ↑U

theorem AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered {S : Scheme} (𝒰 : CategoryTheory.PreZeroHypercover S) [QuasiCompactCover 𝒰] {U : S.Opens} (hU : IsAffineOpen U) : IsCompactOpenCovered (fun (x : 𝒰.I₀) => ⇑(CategoryTheory.ConcreteCategory.hom (𝒰.f x).base)) ↑U

theorem AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isCompact {S : Scheme} (𝒰 : CategoryTheory.PreZeroHypercover S) [QuasiCompactCover 𝒰] {U : S.Opens} (hU : IsCompact ↑U) : IsCompactOpenCovered (fun (x : 𝒰.I₀) => ⇑(CategoryTheory.ConcreteCategory.hom (𝒰.f x).base)) ↑U

theorem AlgebraicGeometry.QuasiCompactCover.exists_isAffineOpen_of_isCompact {S : Scheme} (𝒰 : CategoryTheory.PreZeroHypercover S) [QuasiCompactCover 𝒰] {U : S.Opens} (hU : IsCompact ↑U) : ∃ (n : ℕ) (f : Fin n → 𝒰.I₀) (V : (i : Fin n) → (𝒰.X (f i)).Opens), (∀ (i : Fin n), IsAffineOpen (V i)) ∧ ⋃ (i : Fin n), ⇑(CategoryTheory.ConcreteCategory.hom (𝒰.f (f i)).base) '' ↑(V i) = ↑U

theorem AlgebraicGeometry.QuasiCompactCover.of_isOpenMap {S : Scheme} {K : CategoryTheory.Precoverage Scheme} {𝒰 : Scheme.Cover K S} [Scheme.JointlySurjective K] (h : ∀ (i : 𝒰.I₀), IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom (𝒰.f i).base)) : QuasiCompactCover 𝒰.toPreZeroHypercover

If the component maps of 𝒰 are open, 𝒰 is quasi-compact. This in particular applies if K is the fppf topology (i.e., flat and of finite presentation) and hence in particular for étale and Zariski covers.

instance AlgebraicGeometry.QuasiCompactCover.inst {S : Scheme} (𝒰 : S.OpenCover) : QuasiCompactCover 𝒰.toPreZeroHypercover

Any open cover is quasi-compact.

theorem AlgebraicGeometry.QuasiCompactCover.of_hom {S : Scheme} {𝒰 : CategoryTheory.PreZeroHypercover S} {𝒱 : CategoryTheory.PreZeroHypercover S} (f : 𝒱.Hom 𝒰) [QuasiCompactCover 𝒱] : QuasiCompactCover 𝒰

If 𝒱 is a refinement of 𝒰 such that 𝒱 is quasicompact, also 𝒰 is quasicompact.

instance AlgebraicGeometry.QuasiCompactCover.instPullback₁Scheme {S : Scheme} (𝒰 : CategoryTheory.PreZeroHypercover S) [QuasiCompactCover 𝒰] {T : Scheme} (f : T ⟶ S) : QuasiCompactCover (CategoryTheory.PreZeroHypercover.pullback₁ f 𝒰)

Stacks Tag 022D ((3))

instance AlgebraicGeometry.QuasiCompactCover.instPullback₂Scheme {S : Scheme} (𝒰 : CategoryTheory.PreZeroHypercover S) [QuasiCompactCover 𝒰] {T : Scheme} (f : T ⟶ S) : QuasiCompactCover (CategoryTheory.PreZeroHypercover.pullback₂ f 𝒰)

instance AlgebraicGeometry.QuasiCompactCover.instBindScheme {X : Scheme} (𝒰 : CategoryTheory.PreZeroHypercover X) [QuasiCompactCover 𝒰] (f : (x : 𝒰.I₀) → CategoryTheory.PreZeroHypercover (𝒰.X x)) [∀ (x : 𝒰.I₀), QuasiCompactCover (f x)] : QuasiCompactCover (𝒰.bind f)

Stacks Tag 022D ((2))

instance AlgebraicGeometry.QuasiCompactCover.of_finite {S : Scheme} {K : CategoryTheory.Precoverage Scheme} {𝒰 : Scheme.Cover K S} [Scheme.JointlySurjective K] [∀ (i : 𝒰.I₀), QuasiCompact (𝒰.f i)] [Finite 𝒰.I₀] : QuasiCompactCover 𝒰.toPreZeroHypercover

instance AlgebraicGeometry.QuasiCompactCover.homCover {P : CategoryTheory.MorphismProperty Scheme} {X S : Scheme} (f : X ⟶ S) (hf : P f) [Surjective f] [QuasiCompact f] : QuasiCompactCover (Scheme.Hom.cover f hf).toPreZeroHypercover

instance AlgebraicGeometry.QuasiCompactCover.singleton {S X : Scheme} (f : X ⟶ S) [Surjective f] [QuasiCompact f] : QuasiCompactCover (CategoryTheory.PreZeroHypercover.singleton f)

instance AlgebraicGeometry.QuasiCompactCover.instCoverOfIsIso {P : CategoryTheory.MorphismProperty Scheme} [P.ContainsIdentities] [P.RespectsIso] {X Y : Scheme} {f : X ⟶ Y} [CategoryTheory.IsIso f] : QuasiCompactCover (Scheme.coverOfIsIso f).toPreZeroHypercover

Stacks Tag 022D ((1))

def AlgebraicGeometry.Scheme.quasiCompactCover (S : Scheme) : CategoryTheory.ObjectProperty (CategoryTheory.PreZeroHypercover S)

The object property on the category of pre-0-hypercovers of a scheme given by quasi-compact covers.

Equations

• S.quasiCompactCover = AlgebraicGeometry.QuasiCompactCover

@[simp]

theorem AlgebraicGeometry.Scheme.quasiCompactCover_iff (S : Scheme) (𝒰 : CategoryTheory.PreZeroHypercover S) : S.quasiCompactCover 𝒰 ↔ QuasiCompactCover 𝒰

instance AlgebraicGeometry.Scheme.isClosedUnderIsomorphisms_quasiCompactCover (S : Scheme) : S.quasiCompactCover.IsClosedUnderIsomorphisms