Morphisms of finite presentation #
A morphism of schemes f : X ⟶ Y is locally of finite presentation if for each affine U ⊆ Y and
V ⊆ f ⁻¹' U, The induced map Γ(Y, U) ⟶ Γ(X, V) is of finite presentation.
A morphism of schemes is of finite presentation if it is both locally of finite presentation and quasi-compact. We do not provide a separate declaration for this, instead simply assume both conditions.
We show that these properties are local, and are stable under compositions.
A morphism of schemes f : X ⟶ Y is locally of finite presentation if for each affine U ⊆ Y
and V ⊆ f ⁻¹' U, The induced map Γ(Y, U) ⟶ Γ(X, V) is of finite presentation.
- finitePresentation_of_affine_subset : ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U), RingHom.FinitePresentation (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)
Instances
theorem
AlgebraicGeometry.locallyOfFinitePresentation_iff
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
:
AlgebraicGeometry.LocallyOfFinitePresentation f ↔ ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U),
RingHom.FinitePresentation (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)
instance
AlgebraicGeometry.instHasRingHomPropertyLocallyOfFinitePresentationFinitePresentation :
AlgebraicGeometry.HasRingHomProperty @AlgebraicGeometry.LocallyOfFinitePresentation
fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.FinitePresentation
@[instance 900]
instance
AlgebraicGeometry.locallyOfFinitePresentation_of_isOpenImmersion
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
[AlgebraicGeometry.IsOpenImmersion f]
:
Equations
- ⋯ = ⋯
instance
AlgebraicGeometry.locallyOfFinitePresentation_comp
{X Y Z : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[hf : AlgebraicGeometry.LocallyOfFinitePresentation f]
[hg : AlgebraicGeometry.LocallyOfFinitePresentation g]
:
Equations
- ⋯ = ⋯