Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Cover.Over.noConfusion

{P : Sort u_2} →
  {S : AlgebraicGeometry.Scheme} →
    {P_1 : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
      {inst : P_1.IsStableUnderBaseChange} →
        {inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P_1} →
          {X : AlgebraicGeometry.Scheme} →
            {inst_2 : X.Over S} →
              {𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P_1) X} →
                {t : 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'} →
                                {t' : AlgebraicGeometry.Scheme.Cover.Over S' 𝒰'} →
                                  S = S' →
                                    P_1 = P' →
                                      inst ≍ inst' →
                                        inst_1 ≍ inst'_1 →
                                          X = X' →
                                            inst_2 ≍ inst'_2 →
                                              𝒰 ≍ 𝒰' →
                                                t ≍ t' → AlgebraicGeometry.Scheme.Cover.Over.noConfusionType P t t'

Defined in

Mathlib.AlgebraicGeometry.Cover.Over

Cited by

0 results in Mathlib

Foundations

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