Theorems · Theorem · algebraic geometry

AlgebraicGeometry.QuasiCompactCover.of_isOpenMap

∀ {S : AlgebraicGeometry.Scheme} {K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme}
  {𝒰 : AlgebraicGeometry.Scheme.Cover K S} [AlgebraicGeometry.Scheme.JointlySurjective K],
  (∀ (i : 𝒰.I₀), IsOpenMap ⇑(𝒰.f i)) → AlgebraicGeometry.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.

Defined in

Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Cited by

1 results in Mathlib

Foundations

Depth 147 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AlgebraicGeometry.Scheme.JointlySurjective