Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Cover.Over.noConfusionType

Sort u_2 →
  {S : AlgebraicGeometry.Scheme} →
    {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
      [inst : P.IsStableUnderBaseChange] →
        [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] →
          {X : AlgebraicGeometry.Scheme} →
            [inst_2 : X.Over S] →
              {𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X} →
                AlgebraicGeometry.Scheme.Cover.Over S 𝒰 →
                  {S' : AlgebraicGeometry.Scheme} →
                    {P' : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
                      [inst' : P'.IsStableUnderBaseChange] →
                        [inst'_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P'] →
                          {X' : AlgebraicGeometry.Scheme} →
                            [inst'_2 : X'.Over S'] →
                              {𝒰' : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P') X'} →
                                AlgebraicGeometry.Scheme.Cover.Over S' 𝒰' → Sort u_2

Defined in

Mathlib.AlgebraicGeometry.Cover.Over

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlgebraicGeometry.Scheme.IsJointlySurjectivePreservingAlgebraicGeometry.Scheme.OverCategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlgebraicGeometry.Scheme.IsJointlySurjectivePreservingAlgebraicGeometry.Scheme.Over