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.
theorem
AlgebraicGeometry.locallyOfFiniteType_iff
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
:
AlgebraicGeometry.LocallyOfFiniteType f ↔ ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.val.base).obj ↑U),
RingHom.FiniteType (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)
class
AlgebraicGeometry.LocallyOfFiniteType
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
:
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.val.base).obj ↑U), RingHom.FiniteType (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)
Instances
theorem
AlgebraicGeometry.LocallyOfFiniteType.finiteType_of_affine_subset
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
{f : X ⟶ Y}
[self : AlgebraicGeometry.LocallyOfFiniteType f]
(U : ↑Y.affineOpens)
(V : ↑X.affineOpens)
(e : ↑V ≤ (TopologicalSpace.Opens.map f.val.base).obj ↑U)
:
RingHom.FiniteType (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)
@[instance 900]
instance
AlgebraicGeometry.locallyOfFiniteType_of_isOpenImmersion
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
[AlgebraicGeometry.IsOpenImmersion f]
:
Equations
- ⋯ = ⋯
instance
AlgebraicGeometry.locallyOfFiniteType_comp
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
{Z : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[hf : AlgebraicGeometry.LocallyOfFiniteType f]
[hg : AlgebraicGeometry.LocallyOfFiniteType g]
:
Equations
- ⋯ = ⋯
theorem
AlgebraicGeometry.locallyOfFiniteType_of_comp
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
{Z : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[hf : AlgebraicGeometry.LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp f g)]
:
theorem
AlgebraicGeometry.LocallyOfFiniteType.affine_openCover_iff
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(𝒰 : Y.OpenCover)
[∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)]
(𝒰' : (i : (𝒰.pullbackCover f).J) → ((𝒰.pullbackCover f).obj i).OpenCover)
[∀ (i : (𝒰.pullbackCover f).J) (j : (𝒰' i).J), AlgebraicGeometry.IsAffine ((𝒰' i).obj j)]
:
AlgebraicGeometry.LocallyOfFiniteType f ↔ ∀ (i : (𝒰.pullbackCover f).J) (j : (𝒰' i).J),
RingHom.FiniteType
(AlgebraicGeometry.Scheme.Γ.map
(CategoryTheory.CategoryStruct.comp ((𝒰' i).map j) CategoryTheory.Limits.pullback.snd).op)
theorem
AlgebraicGeometry.LocallyOfFiniteType.source_openCover_iff
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(𝒰 : X.OpenCover)
:
AlgebraicGeometry.LocallyOfFiniteType f ↔ ∀ (i : 𝒰.J), AlgebraicGeometry.LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp (𝒰.map i) f)
theorem
AlgebraicGeometry.LocallyOfFiniteType.openCover_iff
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(𝒰 : Y.OpenCover)
:
AlgebraicGeometry.LocallyOfFiniteType f ↔ ∀ (i : 𝒰.J), AlgebraicGeometry.LocallyOfFiniteType CategoryTheory.Limits.pullback.snd