Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Cover.toPresieveOverProp

{P Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {S : AlgebraicGeometry.Scheme} →
    [inst : P.IsStableUnderBaseChange] →
      {X : Q.Over ⊤ S} →
        (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X.left) →
          [inst_1 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰] → (∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)) → CategoryTheory.Presieve X

The presieve defined by a P-cover of S-schemes with Q.

Defined in

Mathlib.AlgebraicGeometry.Sites.Small

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlgebraicGeometry.Scheme.Cover.Over