Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp

{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] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰] →
                    [AlgebraicGeometry.Scheme.Hom.IsOver f S] →
                      {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
                        [Q.HasOfPostcompProperty Q] →
                          [Q.IsStableUnderBaseChange] →
                            [Q.IsStableUnderComposition] →
                              Q (X ↘ S) →
                                Q (W ↘ S) →
                                  (∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)) →
                                    AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) W

The pullback of a cover of S-schemes with Q along a morphism of S-schemes. This is not definitionally equal to AlgebraicGeometry.Scheme.Cover.pullbackCover, as here we take the pullback in Q.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.IsOverCategoryTheory.MorphismProperty.HasOfPostcompPropertyCategoryTheory.MorphismProperty.IsStableUnderBaseChangeCategoryTheory.MorphismProperty.IsStableUnderComposition