Site defined by a morphism property #
Given a multiplicative morphism property P that is stable under base change, we define the
associated precoverage on the category of schemes, where coverings are given
by jointly surjective families of morphisms satisfying P.
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.
- exists_preimage_fst_triplet_of_prop {X Y S : Scheme} {f : X ⟶ S} {g : Y ⟶ S} [CategoryTheory.Limits.HasPullback f g] (hg : P g) (x : ↥X) (y : ↥Y) (h : (CategoryTheory.ConcreteCategory.hom f.base) x = (CategoryTheory.ConcreteCategory.hom g.base) y) : ∃ (a : ↥(CategoryTheory.Limits.pullback f g)), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g).base) a = x
Instances
The precoverage on Scheme of jointly surjective families.
Equations
Instances For
The precoverage on Scheme induced by P is given by jointly surjective families of
P-morphisms.
Equations
Instances For
The Zariski precoverage on the category of schemes is the precoverage defined by jointly surjective families of open immersions.