Theorems · Definition · algebraic geometry

AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.recOn

{P : AlgebraicGeometry.AffineTargetMorphismProperty} →
  {motive : P.IsLocal → Sort u} →
    (t : P.IsLocal) →
      ((respectsIso : P.toProperty.RespectsIso) →
          (to_basicOpen :
              ∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y)
                (r : ↑(Y.presheaf.obj (Opposite.op ⊤))), P f → P (f ∣_ Y.basicOpen r)) →
            (of_basicOpenCover :
                ∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y)
                  (s : Finset ↑(Y.presheaf.obj (Opposite.op ⊤))),
                  Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P (f ∣_ Y.basicOpen ↑r)) → P f) →
              motive ⋯) →
        motive t

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Basic

Cited by

0 results in Mathlib

Foundations

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