Site defined by a morphism property #
Given a multiplicative morphism property P that is stable under base change, we define the
associated (pre)topology on the category of schemes, where coverings are given
by jointly surjective families of morphisms satisfying P.
TODO #
- Define the small site on
Over P Q X.
The pretopology on the category of schemes defined by covering families where the components
satisfy P.
The coverings are defined via existence of a P-cover. This is convenient in practice, as one
directly has the cover available. For a pretopology generating the same Grothendieck topology, see
AlgebraicGeometry.Scheme.grothendieckTopology_eq_inf.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Grothendieck topology on the category of schemes induced by the pretopology defined by
P-covers.
Equations
Instances For
The pretopology on the category of schemes defined by jointly surjective families.
Note: The assumption IsJointlySurjectivePreserving ⊤ is mathematically unneeded, and only here
to reduce imports. To satisfy it, use AlgebraicGeometry.Scheme.isJointlySurjectivePreserving.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Grothendieck topology defined by P-covers agrees with the Grothendieck
topology induced by the intersection of the pretopology of surjective families with
the pretopology defined by P.
Note: Because of size issues, this does not hold on the level of pretopologies: A presieve
in the intersection can have up to Type (u + 1) many components, while in the definition
of AlgebraicGeometry.Scheme.pretopology we only allow Type u many components.