Morphisms of finite type #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
@[class]
structure
algebraic_geometry.locally_of_finite_type
{X Y : algebraic_geometry.Scheme}
(f : X ⟶ Y) :
Prop
- finite_type_of_affine_subset : ∀ (U : ↥(Y.affine_opens)) (V : ↥(X.affine_opens)) (e : V.val ≤ (topological_space.opens.map f.val.base).obj U.val), ring_hom.finite_type (algebraic_geometry.Scheme.hom.app_le 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 of this typeclass
theorem
algebraic_geometry.locally_of_finite_type_iff
{X Y : algebraic_geometry.Scheme}
(f : X ⟶ Y) :
algebraic_geometry.locally_of_finite_type f ↔ ∀ (U : ↥(Y.affine_opens)) (V : ↥(X.affine_opens)) (e : V.val ≤ (topological_space.opens.map f.val.base).obj U.val), ring_hom.finite_type (algebraic_geometry.Scheme.hom.app_le f e)
@[protected, instance]
@[protected, instance]
def
algebraic_geometry.locally_of_finite_type_comp
{X Y Z : algebraic_geometry.Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[hf : algebraic_geometry.locally_of_finite_type f]
[hg : algebraic_geometry.locally_of_finite_type g] :
theorem
algebraic_geometry.locally_of_finite_type_of_comp
{X Y Z : algebraic_geometry.Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[hf : algebraic_geometry.locally_of_finite_type (f ≫ g)] :
theorem
algebraic_geometry.locally_of_finite_type.affine_open_cover_iff
{X Y : algebraic_geometry.Scheme}
(f : X ⟶ Y)
(𝒰 : Y.open_cover)
[∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)]
(𝒰' : Π (i : (𝒰.pullback_cover f).J), ((𝒰.pullback_cover f).obj i).open_cover)
[∀ (i : (𝒰.pullback_cover f).J) (j : (𝒰' i).J), algebraic_geometry.is_affine ((𝒰' i).obj j)] :
algebraic_geometry.locally_of_finite_type f ↔ ∀ (i : (𝒰.pullback_cover f).J) (j : (𝒰' i).J), ring_hom.finite_type (algebraic_geometry.Scheme.Γ.map ((𝒰' i).map j ≫ category_theory.limits.pullback.snd).op)
theorem
algebraic_geometry.locally_of_finite_type.source_open_cover_iff
{X Y : algebraic_geometry.Scheme}
(f : X ⟶ Y)
(𝒰 : X.open_cover) :
algebraic_geometry.locally_of_finite_type f ↔ ∀ (i : 𝒰.J), algebraic_geometry.locally_of_finite_type (𝒰.map i ≫ f)
theorem
algebraic_geometry.locally_of_finite_type.open_cover_iff
{X Y : algebraic_geometry.Scheme}
(f : X ⟶ Y)
(𝒰 : Y.open_cover) :