Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Cover.pullbackCoverOver

{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  (S : AlgebraicGeometry.Scheme) →
    [inst : P.IsStableUnderBaseChange] →
      [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] →
        {X W : AlgebraicGeometry.Scheme} →
          (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
            (f : W ⟶ X) →
              [inst_2 : W.Over S] →
                [inst_3 : X.Over S] →
                  [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] →
                    [AlgebraicGeometry.Scheme.Hom.IsOver f S] →
                      AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) W

The pullback of a cover of S-schemes along a morphism of S-schemes. This is not definitionally equal to AlgebraicGeometry.Scheme.Cover.pullback₁, as here we take the pullback in Over S, whose underlying scheme is only isomorphic but not equal to the pullback in Scheme.

Defined in

Mathlib.AlgebraicGeometry.Cover.Over

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlgebraicGeometry.Scheme.IsJointlySurjectivePreservingAlgebraicGeometry.Scheme.OverAlgebraicGeometry.Scheme.OverAlgebraicGeometry.Scheme.Cover.OverAlgebraicGeometry.Scheme.Hom.IsOver