Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Cover.Over.casesOn

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

Defined in

Mathlib.AlgebraicGeometry.Cover.Over

Cited by

0 results in Mathlib

Foundations

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

Assumes

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