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₂
.AffineTargetMorphismProperty.of
: Given a morphism propertyP
of schemes, this is the restriction ofP
to morphisms with affine target. IfP
is local at the target, we have(toAffineTargetMorphismProperty P).targetAffineLocally = P
(seeMorphismProperty.targetAffineLocally_toAffineTargetMorphismProperty_eq_of_isLocalAtTarget
).MorphismProperty.topologically
: Given a propertyP
of maps of topological spaces,(topologically P) f
holds ifP
holds for the underlying continuous map off
.MorphismProperty.stalkwise
: Given a propertyP
of ring homs,(stalkwise P) f
holds ifP
holds for all stalk maps.
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
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
topologically P
holds for a morphism if the underlying topological map satisfies P
.
Equations
- AlgebraicGeometry.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.
stalkwise P
holds for a morphism if all stalks satisfy P
.
Equations
- AlgebraicGeometry.stalkwise P f = ∀ (x_1 : ↑↑x✝.toPresheafedSpace), P (AlgebraicGeometry.Scheme.Hom.stalkMap f x_1)
Instances For
If P
respects isos, then stalkwise P
respects isos.
If P
respects isos, then stalkwise P
is local at the target.
If P
is local at the target, to show that P
is stable under base change, it suffices to
check this for base change along a morphism of affine schemes.
Alias of AlgebraicGeometry.HasAffineProperty.diagonal_of_openCover
.
Alias of AlgebraicGeometry.HasAffineProperty.diagonal_of_diagonal_of_isPullback
.