Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Cover.Over.mk.noConfusion

{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} →
              {P_1 : Sort u_2} →
                {«over» : autoParam ((j : 𝒰.I₀) → (𝒰.X j).Over S) AlgebraicGeometry.Scheme.Cover.Over.over._autoParam} →
                  {isOver_map :
                      autoParam (∀ (j : 𝒰.I₀), AlgebraicGeometry.Scheme.Hom.IsOver (𝒰.f j) S)
                        AlgebraicGeometry.Scheme.Cover.Over.isOver_map._autoParam} →
                    {over' :
                        autoParam ((j : 𝒰.I₀) → (𝒰.X j).Over S) AlgebraicGeometry.Scheme.Cover.Over.over._autoParam} →
                      {isOver_map' :
                          autoParam (∀ (j : 𝒰.I₀), AlgebraicGeometry.Scheme.Hom.IsOver (𝒰.f j) S)
                            AlgebraicGeometry.Scheme.Cover.Over.isOver_map._autoParam} →
                        { «over» := «over», isOver_map := isOver_map } =
                            { «over» := over', isOver_map := isOver_map' } →
                          («over» ≍ over' → P_1) → P_1

Defined in

Mathlib.AlgebraicGeometry.Cover.Over

Cited by

0 results in Mathlib

Foundations

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