Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving.exists_preimage_snd_triplet_of_prop

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

Defined in

Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Cited by

0 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.Scheme.IsJointlySurjectivePreservingCategoryTheory.Limits.HasPullback