Morphisms of finite type #
A morphism of schemes f : X ⟶ Y is locally of finite type if for each affine U ⊆ Y and
V ⊆ f ⁻¹' U, The induced map Γ(Y, U) ⟶ Γ(X, V) is of finite type.
A morphism of schemes is of finite type if it is both locally of finite type and quasi-compact.
We show that these properties are local, and are stable under compositions and base change.
A morphism of schemes f : X ⟶ Y is locally of finite type if for each affine U ⊆ Y and
V ⊆ f ⁻¹' U, The induced map Γ(Y, U) ⟶ Γ(X, V) is of finite type.
- finiteType_of_affine_subset : ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U), RingHom.FiniteType (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)
Instances
theorem
AlgebraicGeometry.locallyOfFiniteType_iff
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
:
AlgebraicGeometry.LocallyOfFiniteType f ↔ ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U),
RingHom.FiniteType (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)
instance
AlgebraicGeometry.instHasRingHomPropertyLocallyOfFiniteTypeFiniteType :
AlgebraicGeometry.HasRingHomProperty @AlgebraicGeometry.LocallyOfFiniteType
fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.FiniteType
@[instance 900]
instance
AlgebraicGeometry.locallyOfFiniteType_of_isOpenImmersion
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
[AlgebraicGeometry.IsOpenImmersion f]
:
Equations
- ⋯ = ⋯
instance
AlgebraicGeometry.locallyOfFiniteType_comp
{X Y Z : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[hf : AlgebraicGeometry.LocallyOfFiniteType f]
[hg : AlgebraicGeometry.LocallyOfFiniteType g]
:
Equations
- ⋯ = ⋯
theorem
AlgebraicGeometry.locallyOfFiniteType_of_comp
{X Y Z : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[AlgebraicGeometry.LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp f g)]
: