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