Constructors for properties of morphisms between schemes #
This file provides some constructors to obtain morphism properties of schemes from other morphism properties:
AffineTargetMorphismProperty.diagonal
: Given an affine target morphism propertyP
,P.diagonal f
holds ifP (pullback.mapDesc f₁ f₂ f)
holds for two affine open immersionsf₁
andf₂
.MorphismProperty.topologically
: Given a propertyP
of maps of topological spaces,(topologically P) f
holds ifP
holds for the underlying continuous map off
.
Also provides API for showing the standard locality and stability properties for these types of properties.
The AffineTargetMorphismProperty
associated to (targetAffineLocally P).diagonal
.
See diagonal_targetAffineLocally_eq_targetAffineLocally
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
topologically P
holds for a morphism if the underlying topological map satisfies P
.
Equations
- AlgebraicGeometry.MorphismProperty.topologically P f = P ⇑f.val.base
Instances For
If a property of maps of topological spaces is stable under composition, the induced morphism property of schemes is stable under composition.
If a property of maps of topological spaces is satisfied by all homeomorphisms, every isomorphism of schemes satisfies the induced property.
If a property of maps of topological spaces is satisfied by homeomorphisms and is stable under composition, the induced property on schemes respects isomorphisms.
To check that a topologically defined morphism property is local at the target, we may check the corresponding properties on topological spaces.
Alias of AlgebraicGeometry.diagonal_targetAffineLocally_of_openCover
.
Alias of AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_of_targetAffineLocally
.
Alias of AlgebraicGeometry.universally_isLocalAtTarget_of_morphismRestrict
.