Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Cover.qculift

{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {S : AlgebraicGeometry.Scheme} →
    (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S) →
      [AlgebraicGeometry.QuasiCompactCover 𝒰.toPreZeroHypercover] →
        AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.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.

Defined in

Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Cited by

0 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.QuasiCompactCover