Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Cover.toPresieveOver

{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {S : AlgebraicGeometry.Scheme} →
    [inst : P.IsStableUnderBaseChange] →
      {X : CategoryTheory.Over S} →
        (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X.left) →
          [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] → CategoryTheory.Presieve X

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

Defined in

Mathlib.AlgebraicGeometry.Sites.Small

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlgebraicGeometry.Scheme.Cover.Over