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.

source

🔶 coverage

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₀) => ⇑(𝒰.f x)) ↑U

Instances

source

📐 coverage

theorem AlgebraicGeometry.quasiCompactCover_iff {S : Scheme} (𝒰 : CategoryTheory.PreZeroHypercover S) :

QuasiCompactCover 𝒰 ↔ ∀ {U : S.Opens}, IsAffineOpen U → IsCompactOpenCovered (fun (x : 𝒰.I₀) => ⇑(𝒰.f x)) ↑U

source

📐 coverage

theorem AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered {S : Scheme} (𝒰 : CategoryTheory.PreZeroHypercover S) [QuasiCompactCover 𝒰] {U : S.Opens} (hU : IsAffineOpen U) :

IsCompactOpenCovered (fun (x : 𝒰.I₀) => ⇑(𝒰.f x)) ↑U

source

📐 coverage

theorem AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isCompact {S : Scheme} (𝒰 : CategoryTheory.PreZeroHypercover S) [QuasiCompactCover 𝒰] {U : S.Opens} (hU : IsCompact ↑U) :

IsCompactOpenCovered (fun (x : 𝒰.I₀) => ⇑(𝒰.f x)) ↑U

source

📐 coverage

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), ⇑(𝒰.f (f i)) '' ↑(V i) = ↑U

source

📐 coverage

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

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.

source

📐 coverage

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

QuasiCompactCover 𝒰.toPreZeroHypercover

Any open cover is quasi-compact.

source

📐 coverage

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.

source

📐 coverage

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))

source

📐 coverage

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

QuasiCompactCover (CategoryTheory.PreZeroHypercover.pullback₂ f 𝒰)

source

📐 coverage

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))

source

📐 coverage

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

source

📐 coverage

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

source

📐 coverage

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

QuasiCompactCover (CategoryTheory.PreZeroHypercover.singleton f)

source

📐 coverage

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))

source

📐 coverage

instance AlgebraicGeometry.QuasiCompactCover.instSumScheme {S : Scheme} {𝒰 : CategoryTheory.PreZeroHypercover S} {𝒱 : CategoryTheory.PreZeroHypercover S} [QuasiCompactCover 𝒰] :

QuasiCompactCover (𝒰.sum 𝒱)

source

📐 coverage

instance AlgebraicGeometry.QuasiCompactCover.instSumScheme_1 {S : Scheme} {𝒰 : CategoryTheory.PreZeroHypercover S} {𝒱 : CategoryTheory.PreZeroHypercover S} [QuasiCompactCover 𝒱] :

QuasiCompactCover (𝒰.sum 𝒱)

source

📐 coverage

theorem AlgebraicGeometry.QuasiCompactCover.exists_hom {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} (𝒰 : Scheme.Cover (Scheme.precoverage P) S) [P.RespectsLeft IsOpenImmersion] [CompactSpace ↥S] [QuasiCompactCover 𝒰.toPreZeroHypercover] :

∃ (𝒱 : Scheme.AffineCover P S) (f : 𝒱.cover ⟶ 𝒰), Finite 𝒱.I₀ ∧ ∀ (j : 𝒱.cover.I₀), IsOpenImmersion (f.h₀ j)

source

🔸 coverage

noncomputable def AlgebraicGeometry.QuasiCompactCover.ulift {S : Scheme} (𝒰 : CategoryTheory.PreZeroHypercover S) [QuasiCompactCover 𝒰] :

CategoryTheory.PreZeroHypercover S

Lift a quasi-compact cover of a u-scheme in an arbitrary universe to u. The indexing type is constructed by choosing finitely many compact opens above every affine open. This cover is again quasi-compact.

Equations

Instances For

source

🔸 coverage