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 ⇑f) : 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

theorem AlgebraicGeometry.Scheme.Hom.singleton_mem_qcPrecoverage {X Y : Scheme} (f : X ⟶ Y) [Surjective f] [QuasiCompact f] : CategoryTheory.Presieve.singleton f ∈ qcPrecoverage.coverings Y

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.propQCPrecoverage (P : CategoryTheory.MorphismProperty Scheme) : CategoryTheory.Precoverage Scheme

The qc-precoverage of a scheme wrt. to a morphism property P is the precoverage given by quasi-compact covers satisfying P.

Equations

• AlgebraicGeometry.Scheme.propQCPrecoverage P = AlgebraicGeometry.Scheme.qcPrecoverage ⊓ AlgebraicGeometry.Scheme.precoverage P

theorem AlgebraicGeometry.Scheme.propQCPrecoverage_le_precoverage {P : CategoryTheory.MorphismProperty Scheme} : propQCPrecoverage P ≤ precoverage P

instance AlgebraicGeometry.Scheme.instQuasiCompactCover {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} (𝒰 : Cover (propQCPrecoverage P) S) : QuasiCompactCover 𝒰.toPreZeroHypercover

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Cover.forgetQc {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} (𝒰 : Cover (propQCPrecoverage P) S) : Cover (precoverage P) S

Forget being quasi-compact.

Equations

• 𝒰.forgetQc = { toPreZeroHypercover := 𝒰.toPreZeroHypercover, mem₀ := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.forgetQc_toPreZeroHypercover {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} (𝒰 : Cover (propQCPrecoverage P) S) : 𝒰.forgetQc.toPreZeroHypercover = 𝒰.toPreZeroHypercover

instance AlgebraicGeometry.Scheme.instQuasiCompactCoverForgetQc {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} (𝒰 : Cover (propQCPrecoverage P) S) : QuasiCompactCover 𝒰.forgetQc.toPreZeroHypercover

def AlgebraicGeometry.Scheme.Cover.ofQuasiCompactCover {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} (𝒰 : Cover (precoverage P) S) [qc : QuasiCompactCover 𝒰.toPreZeroHypercover] : Cover (propQCPrecoverage P) S

Construct a cover in the P-qc topology from a quasi-compact cover in the P-topology.

Equations

• 𝒰.ofQuasiCompactCover = { toPreZeroHypercover := 𝒰.toPreZeroHypercover, mem₀ := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.ofQuasiCompactCover_toPreZeroHypercover {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} (𝒰 : Cover (precoverage P) S) [qc : QuasiCompactCover 𝒰.toPreZeroHypercover] : 𝒰.ofQuasiCompactCover.toPreZeroHypercover = 𝒰.toPreZeroHypercover

noncomputable def AlgebraicGeometry.Scheme.Cover.qculift {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} (𝒰 : Cover (precoverage P) S) [QuasiCompactCover 𝒰.toPreZeroHypercover] : Cover (precoverage P) S

Lift a quasi-compact P-cover of a u-scheme in an arbitrary universe to universe u. This is again quasi-compact.

Equations

• 𝒰.qculift = { toPreZeroHypercover := 𝒰.ulift.sum (AlgebraicGeometry.QuasiCompactCover.ulift 𝒰.toPreZeroHypercover), mem₀ := ⋯ }

instance AlgebraicGeometry.Scheme.instQuasiCompactCoverQculift {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} (𝒰 : Cover (precoverage P) S) [QuasiCompactCover 𝒰.toPreZeroHypercover] : QuasiCompactCover 𝒰.qculift.toPreZeroHypercover

instance AlgebraicGeometry.Scheme.instSmallPropQCPrecoverage {P : CategoryTheory.MorphismProperty Scheme} : (propQCPrecoverage P).Small

theorem AlgebraicGeometry.Scheme.mem_propQCPrecoverage_iff_exists_quasiCompactCover {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} {R : CategoryTheory.Presieve S} : R ∈ (propQCPrecoverage P).coverings S ↔ ∃ (𝒰 : Cover (precoverage P) S), QuasiCompactCover 𝒰.toPreZeroHypercover ∧ R = 𝒰.presieve₀

theorem AlgebraicGeometry.Scheme.Hom.singleton_mem_propQCPrecoverage {P : CategoryTheory.MorphismProperty Scheme} {X Y : Scheme} {f : X ⟶ Y} (hf : P f) [Surjective f] [QuasiCompact f] : CategoryTheory.Presieve.singleton f ∈ (propQCPrecoverage P).coverings Y

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.propQCTopology (P : CategoryTheory.MorphismProperty Scheme) : CategoryTheory.GrothendieckTopology Scheme

The P-qc-topology on the category of schemes wrt. to a morphism property P is the topology generated by quasi-compact covers satisfying P.

Equations

• AlgebraicGeometry.Scheme.propQCTopology P = (AlgebraicGeometry.Scheme.propQCPrecoverage P).toGrothendieck

theorem AlgebraicGeometry.Scheme.Hom.generate_singleton_mem_propQCTopology {P : CategoryTheory.MorphismProperty Scheme} {X Y : Scheme} (f : X ⟶ Y) (hf : P f) [Surjective f] [QuasiCompact f] : CategoryTheory.Sieve.generate (CategoryTheory.Presieve.singleton f) ∈ (propQCTopology P) Y

@[simp]

theorem AlgebraicGeometry.Scheme.Cover.mem_propQCTopology {P : CategoryTheory.MorphismProperty Scheme} {S : Scheme} (𝒰 : Cover (precoverage P) S) [QuasiCompactCover 𝒰.toPreZeroHypercover] : CategoryTheory.Sieve.ofArrows 𝒰.X 𝒰.f ∈ (propQCTopology P) S