Quasi-compact precoverage

In this file we define the quasi-compact precoverage. A cover is covering in the quasi-compact precoverage if it is a quasi-compact cover, i.e., if every affine open of the base can be covered by a finite union of images of quasi-compact opens of the components.

The fpqc precoverage is the precoverage by flat covers that are quasi-compact in this sense.

@[simp]

theorem AlgebraicGeometry.Scheme.quasiCompactCover_shrink_iff {S : Scheme} (E : CategoryTheory.PreZeroHypercover S) : QuasiCompactCover E.shrink ↔ QuasiCompactCover E

def AlgebraicGeometry.Scheme.qcCoverFamily : CategoryTheory.PreZeroHypercoverFamily Scheme

The pre-0-hypercover family on the category of schemes underlying the fpqc precoverage.

Equations

• AlgebraicGeometry.Scheme.qcCoverFamily = { property := fun (X : AlgebraicGeometry.Scheme) => X.quasiCompactCover, iff_shrink := @AlgebraicGeometry.Scheme.qcCoverFamily._proof_1 }

@[simp]

theorem AlgebraicGeometry.Scheme.qcCoverFamily_property (X : Scheme) (a✝ : CategoryTheory.PreZeroHypercover X) : qcCoverFamily.property a✝ = X.quasiCompactCover a✝

def AlgebraicGeometry.Scheme.qcPrecoverage : CategoryTheory.Precoverage Scheme

The quasi-compact precoverage on the category of schemes is the precoverage given by quasi-compact covers. The intersection of this precoverage with the precoverage defined by jointly surjective families of flat morphisms is the fpqc-precoverage.

Equations

• AlgebraicGeometry.Scheme.qcPrecoverage = AlgebraicGeometry.Scheme.qcCoverFamily.precoverage

@[simp]

theorem AlgebraicGeometry.Scheme.presieve₀_mem_qcPrecoverage_iff {S : Scheme} {E : CategoryTheory.PreZeroHypercover S} : E.presieve₀ ∈ qcPrecoverage.coverings S ↔ QuasiCompactCover E

instance AlgebraicGeometry.Scheme.instHasIsosQcPrecoverage : qcPrecoverage.HasIsos

instance AlgebraicGeometry.Scheme.instIsStableUnderBaseChangeQcPrecoverage : qcPrecoverage.IsStableUnderBaseChange

instance AlgebraicGeometry.Scheme.instIsStableUnderCompositionQcPrecoverage : qcPrecoverage.IsStableUnderComposition

instance AlgebraicGeometry.Scheme.instIsStableUnderSupQcPrecoverage : qcPrecoverage.IsStableUnderSup

theorem AlgebraicGeometry.Scheme.precoverage_le_qcPrecoverage_of_isOpenMap {P : CategoryTheory.MorphismProperty Scheme} (hP : P ≤ fun (x x_1 : Scheme) (f : x ⟶ x_1) => IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f.base)) : precoverage P ≤ qcPrecoverage

If P implies being an open map, the by P induced precoverage is coarser than the quasi-compact precoverage.

theorem AlgebraicGeometry.Scheme.zariskiPrecoverage_le_qcPrecoverage : zariskiPrecoverage ≤ qcPrecoverage