Documentation

Mathlib.AlgebraicGeometry.Morphisms.FiniteType

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.

class AlgebraicGeometry.LocallyOfFiniteType {X Y : 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_appLE {U : Y.Opens} : IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FiniteType

Instances

theorem AlgebraicGeometry.locallyOfFiniteType_iff {X Y : Scheme} (f : X ⟶ Y) :

LocallyOfFiniteType f ↔ ∀ {U : Y.Opens}, IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FiniteType

theorem AlgebraicGeometry.Scheme.Hom.finiteType_appLE {X Y : Scheme} (f : X ⟶ Y) [self : LocallyOfFiniteType f] {U : Y.Opens} :

IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (appLE f U V e)).FiniteType

Alias of AlgebraicGeometry.LocallyOfFiniteType.finiteType_appLE.

@[deprecated AlgebraicGeometry.Scheme.Hom.finiteType_appLE (since := "2026-01-20")]

theorem AlgebraicGeometry.LocallyOfFiniteType.finiteType_of_affine_subset {X Y : Scheme} (f : X ⟶ Y) [self : LocallyOfFiniteType f] {U : Y.Opens} :

IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FiniteType

Alias of AlgebraicGeometry.LocallyOfFiniteType.finiteType_appLE.

Alias of AlgebraicGeometry.LocallyOfFiniteType.finiteType_appLE.

instance AlgebraicGeometry.instHasRingHomPropertyLocallyOfFiniteTypeFiniteType :

HasRingHomProperty @LocallyOfFiniteType fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.FiniteType

@[instance 900]

instance AlgebraicGeometry.locallyOfFiniteType_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] :

LocallyOfFiniteType f

instance AlgebraicGeometry.instIsStableUnderCompositionSchemeLocallyOfFiniteType :

CategoryTheory.MorphismProperty.IsStableUnderComposition @LocallyOfFiniteType

instance AlgebraicGeometry.locallyOfFiniteType_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [hf : LocallyOfFiniteType f] [hg : LocallyOfFiniteType g] :

LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp f g)

theorem AlgebraicGeometry.locallyOfFiniteType_of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp f g)] :

LocallyOfFiniteType f

instance AlgebraicGeometry.instIsMultiplicativeSchemeLocallyOfFiniteType :

CategoryTheory.MorphismProperty.IsMultiplicative @LocallyOfFiniteType

instance AlgebraicGeometry.locallyOfFiniteType_isStableUnderBaseChange :

CategoryTheory.MorphismProperty.IsStableUnderBaseChange @LocallyOfFiniteType

instance AlgebraicGeometry.instLocallyOfFiniteTypeFstScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [LocallyOfFiniteType g] :

LocallyOfFiniteType (CategoryTheory.Limits.pullback.fst f g)

instance AlgebraicGeometry.instLocallyOfFiniteTypeSndScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [LocallyOfFiniteType f] :

LocallyOfFiniteType (CategoryTheory.Limits.pullback.snd f g)

instance AlgebraicGeometry.instLocallyOfFiniteTypeMorphismRestrict {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) [LocallyOfFiniteType f] :

LocallyOfFiniteType (f ∣_ V)

instance AlgebraicGeometry.instLocallyOfFiniteTypeResLE {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens) (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) [LocallyOfFiniteType f] :

LocallyOfFiniteType (Scheme.Hom.resLE f V U e)

theorem AlgebraicGeometry.LocallyOfFiniteType.stalkMap {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] (x : ↥X) :

(CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).EssFiniteType

instance AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfOfIsJacobsonRing {R : Type u_1} [CommRing R] [IsJacobsonRing R] :

JacobsonSpace ↥(Spec { carrier := R, commRing := inst✝ })

instance AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfIsJacobsonRingCarrier {R : CommRingCat} [IsJacobsonRing ↑R] :

JacobsonSpace ↥(Spec R)

theorem AlgebraicGeometry.LocallyOfFiniteType.jacobsonSpace {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace ↥Y] :

JacobsonSpace ↥X