Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving.exists_preimage_fst_triplet_of_prop

∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  [self : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {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

Defined in

Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Cited by

2 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.Scheme.IsJointlySurjectivePreservingCategoryTheory.Limits.HasPullback