Finite morphisms of schemes

A morphism of schemes f : X ⟶ Y is finite if the preimage of an arbitrary affine open subset of Y is affine and the induced ring map is finite.

It is equivalent to ask only that Y is covered by affine opens whose preimage is affine and the induced ring map is finite.

Also see AlgebraicGeometry.IsFinite.finite_preimage_singleton in Mathlib/AlgebraicGeometry/Fiber.lean for the fact that finite morphisms have finite fibers.

class AlgebraicGeometry.IsFinite {X Y : Scheme} (f : X ⟶ Y) extends AlgebraicGeometry.IsAffineHom f : Prop

A morphism of schemes X ⟶ Y is finite if the preimage of any affine open subset of Y is affine and the induced ring hom is finite.

• isAffine_preimage (U : Y.Opens) : IsAffineOpen U → IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)
• finite_app (U : Y.Opens) (hU : IsAffineOpen U) : (CommRingCat.Hom.hom (Scheme.Hom.app f U)).Finite

theorem AlgebraicGeometry.isFinite_iff {X Y : Scheme} (f : X ⟶ Y) : IsFinite f ↔ IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → (CommRingCat.Hom.hom (Scheme.Hom.app f U)).Finite

theorem AlgebraicGeometry.Scheme.Hom.finite_app {X Y : Scheme} (f : X ⟶ Y) [self : IsFinite f] (U : Y.Opens) (hU : IsAffineOpen U) : (CommRingCat.Hom.hom (app f U)).Finite

Alias of AlgebraicGeometry.IsFinite.finite_app.

instance AlgebraicGeometry.IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop : HasAffineProperty @IsFinite fun (X x : Scheme) (f : X ⟶ x) (x_1 : IsAffine x) => IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite

instance AlgebraicGeometry.IsFinite.instIsStableUnderCompositionScheme : CategoryTheory.MorphismProperty.IsStableUnderComposition @IsFinite

instance AlgebraicGeometry.IsFinite.instIsStableUnderBaseChangeScheme : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @IsFinite

instance AlgebraicGeometry.IsFinite.instContainsIdentitiesScheme : CategoryTheory.MorphismProperty.ContainsIdentities @IsFinite

instance AlgebraicGeometry.IsFinite.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @IsFinite

@[simp]

theorem AlgebraicGeometry.IsFinite.SpecMap_iff {R S : CommRingCat} (f : R ⟶ S) : IsFinite (Spec.map f) ↔ (CommRingCat.Hom.hom f).Finite

@[instance 900]

instance AlgebraicGeometry.IsFinite.instOfIsIsoScheme {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : IsFinite f

instance AlgebraicGeometry.IsFinite.instCompScheme {X Y : Scheme} (f : X ⟶ Y) {Z : Scheme} (g : Y ⟶ Z) [IsFinite f] [IsFinite g] : IsFinite (CategoryTheory.CategoryStruct.comp f g)

instance AlgebraicGeometry.IsFinite.instFstScheme {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [IsFinite g] : IsFinite (CategoryTheory.Limits.pullback.fst f g)

instance AlgebraicGeometry.IsFinite.instSndScheme {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [IsFinite f] : IsFinite (CategoryTheory.Limits.pullback.snd f g)

instance AlgebraicGeometry.IsFinite.instMorphismRestrict {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) [IsFinite f] : IsFinite (f ∣_ V)

theorem AlgebraicGeometry.IsFinite.iff_isIntegralHom_and_locallyOfFiniteType {X Y : Scheme} (f : X ⟶ Y) : IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f

theorem AlgebraicGeometry.IsFinite.eq_inf : @IsFinite = @IsIntegralHom ⊓ @LocallyOfFiniteType

@[instance 900]

instance AlgebraicGeometry.IsFinite.instIsIntegralHom {X Y : Scheme} (f : X ⟶ Y) [IsFinite f] : IsIntegralHom f

@[instance 900]

instance AlgebraicGeometry.IsFinite.instLocallyOfFiniteType {X Y : Scheme} (f : X ⟶ Y) [IsFinite f] : LocallyOfFiniteType f

theorem AlgebraicGeometry.IsClosedImmersion.iff_isFinite_and_mono {X Y : Scheme} (f : X ⟶ Y) : IsClosedImmersion f ↔ IsFinite f ∧ CategoryTheory.Mono f

theorem AlgebraicGeometry.IsClosedImmersion.eq_isFinite_inf_mono : @IsClosedImmersion = @IsFinite ⊓ CategoryTheory.MorphismProperty.monomorphisms Scheme

@[instance 900]

instance AlgebraicGeometry.IsFinite.instOfIsClosedImmersion {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] : IsFinite f

instance AlgebraicGeometry.IsFinite.instHasOfPostcompPropertySchemeIsSeparated : CategoryTheory.MorphismProperty.HasOfPostcompProperty @IsFinite @IsSeparated

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

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

instance AlgebraicGeometry.IsFinite.instDescScheme {U V X : Scheme} (f : U ⟶ X) (g : V ⟶ X) [IsFinite f] [IsFinite g] : IsFinite (CategoryTheory.Limits.coprod.desc f g)

theorem AlgebraicGeometry.Scheme.Hom.finite_appTop {X Y : Scheme} (f : X ⟶ Y) [IsAffine Y] [IsFinite f] : (CommRingCat.Hom.hom (appTop f)).Finite

theorem AlgebraicGeometry.isFinite_iff_locallyOfFiniteType_of_jacobsonSpace {X Y : Scheme} {f : X ⟶ Y} [Subsingleton ↥X] [IsReduced X] [JacobsonSpace ↥Y] : IsFinite f ↔ LocallyOfFiniteType f

If X is a Jacobson scheme and k is a field, Spec(k) ⟶ X is finite iff it is (locally) of finite type. (The statement is more general to allow the empty scheme as well)

theorem AlgebraicGeometry.Scheme.Hom.closedPoints_subset_preimage_closedPoints {X Y : Scheme} (f : X ⟶ Y) [JacobsonSpace ↥Y] [LocallyOfFiniteType f] : closedPoints ↥X ⊆ ⇑f ⁻¹' closedPoints ↥Y

Stacks Tag 01TB ((1) => (3))

@[deprecated AlgebraicGeometry.Scheme.Hom.closedPoints_subset_preimage_closedPoints (since := "2026-09-17")]

theorem AlgebraicGeometry.Scheme.Hom.closePoints_subset_preimage_closedPoints {X Y : Scheme} (f : X ⟶ Y) [JacobsonSpace ↥Y] [LocallyOfFiniteType f] : closedPoints ↥X ⊆ ⇑f ⁻¹' closedPoints ↥Y

Alias of AlgebraicGeometry.Scheme.Hom.closedPoints_subset_preimage_closedPoints.

---

Stacks Tag 01TB ((1) => (3))

theorem AlgebraicGeometry.isClosed_singleton_iff_locallyOfFiniteType {X : Scheme} [JacobsonSpace ↥X] {x : ↥X} : IsClosed {x} ↔ LocallyOfFiniteType (X.fromSpecResidueField x)

Stacks Tag 01TB ((1) => (2))