Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving.recOn

{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {motive : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P → Sort u_1} →
    (t : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P) →
      ((exists_preimage_fst_triplet_of_prop :
            ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} [inst : CategoryTheory.Limits.HasPullback f g],
              P g → ∀ (x : ↥X) (y : ↥Y), f x = g y → ∃ a, (CategoryTheory.Limits.pullback.fst f g) a = x) →
          motive ⋯) →
        motive t

Defined in

Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Cited by

0 results in Mathlib

Foundations

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