Structures · Geometry

AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving

A morphism property of schemes is said to preserve joint surjectivity, if for any pair of morphisms f : X ⟶ S and g : Y ⟶ S where g satisfies P, any pair of points x : X and y : Y with f x = g y can be lifted to a point of X ×[S] Y. In later files, this will be automatic, since this holds for any morphism g (see AlgebraicGeometry.Scheme.isJointlySurjectivePreserving). But at this early stage in the import tree, we only know it for open immersions.

Defined in

Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Shape

One type argument · adds exists_preimage_fst_triplet_of_prop