Documentation

Mathlib.AlgebraicGeometry.Sites.QuasiCompact

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.

Instances For

@[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.

Instances For

@[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.bot_mem_qcPrecoverage (X : Scheme) [IsEmpty ↥X] :

⊥ ∈ qcPrecoverage.coverings X

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.

Instances For

theorem AlgebraicGeometry.Scheme.propQCPrecoverage_le_precoverage {P : CategoryTheory.MorphismProperty Scheme} :

propQCPrecoverage P ≤ precoverage P

theorem AlgebraicGeometry.Scheme.propQCPrecoverage_monotone :

Monotone propQCPrecoverage

theorem AlgebraicGeometry.Scheme.zariskiPrecoverage_le_propQCPrecoverage {P : CategoryTheory.MorphismProperty Scheme} [P.ContainsIdentities] [IsZariskiLocalAtSource P] :

zariskiPrecoverage ≤ propQCPrecoverage P

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

QuasiCompactCover 𝒰.toPreZeroHypercover

theorem AlgebraicGeometry.Scheme.bot_mem_propQCPrecoverage {P : CategoryTheory.MorphismProperty Scheme} (X : Scheme) [IsEmpty ↥X] :

⊥ ∈ (propQCPrecoverage P).coverings X

@[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.

Instances For

@[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.

Instances For

@[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.

Instances For

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.

Instances For

theorem AlgebraicGeometry.Scheme.bot_mem_propQCTopology {P : CategoryTheory.MorphismProperty Scheme} (X : Scheme) [IsEmpty ↥X] :

⊥ ∈ (propQCTopology P) X

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

theorem AlgebraicGeometry.Scheme.zariskiTopology_le_propQCTopology {P : CategoryTheory.MorphismProperty Scheme} [P.IsMultiplicative] [IsZariskiLocalAtSource P] :

zariskiTopology ≤ propQCTopology P