Quasi-finite morphisms

We say that a morphism f : X ⟶ Y is locally quasi finite if Γ(Y, U) ⟶ Γ(X, V) is quasi-finite (in the mathlib sense) for every pair of affine opens that f maps one into the other.

This is equivalent to all the fibers f⁻¹(x) having an open cover of κ(x)-finite schemes. Note that this does not require f to be quasi-compact nor locally of finite type.

We prove that this is stable under composition and base change, and is right cancellative.

Main results

• AlgebraicGeometry.LocallyQuasiFinite : The class of locally quasi-finite morphisms.
• AlgebraicGeometry.Scheme.Hom.isDiscrete_preimage_singleton: Locally quasi-finite morphisms have discrete fibers.
• AlgebraicGeometry.Scheme.Hom.finite_preimage_singleton: Quasi-finite morphisms have finite fibers.
• AlgebraicGeometry.locallyQuasiFinite_iff_isFinite_fiber: If f is quasi-compact, then f is locally quasi-finite iff all the fibers f⁻¹(x) are κ(x)-finite.
• AlgebraicGeometry.locallyQuasiFinite_iff_isDiscrete_preimage_singleton: If f is locally of finite type, then f is locally quasi-finite iff f has discrete fibers.
• AlgebraicGeometry.locallyQuasiFinite_iff_finite_preimage_singleton: If f is of finite type, then f is locally quasi-finite iff f has finite fibers.

class AlgebraicGeometry.LocallyQuasiFinite {X Y : Scheme} (f : X ⟶ Y) : Prop

We say that a morphism f : X ⟶ Y is locally quasi finite if Γ(Y, U) ⟶ Γ(X, V) is quasi-finite (in the mathlib sense) for every pair of affine opens that f maps one into the other.

Note that this does not require f to be quasi-compact nor locally of finite type.

Being locally quasi-finite implies that f has discrete and finite fibers (via f.isDiscrete_preimage_singleton and f.finite_preimage_singleton). The converse holds under various scenarios:

• locallyQuasiFinite_iff_isDiscrete_preimage_singleton: If f is quasi-compact, this is equivalent to f ⁻¹ {x} being κ(x)-finite for all x.
• locallyQuasiFinite_iff_isDiscrete_preimage_singleton: If f is locally of finite type, this is equivalent to f having discrete fibers.
• locallyQuasiFinite_iff_isDiscrete_preimage_singleton: If f is locally of finite type, this is equivalent to f having finite fibers.

• quasiFinite_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)).QuasiFinite

theorem AlgebraicGeometry.locallyQuasiFinite_iff {X Y : Scheme} (f : X ⟶ Y) : LocallyQuasiFinite 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)).QuasiFinite

instance AlgebraicGeometry.instHasRingHomPropertyLocallyQuasiFiniteQuasiFinite : HasRingHomProperty @LocallyQuasiFinite fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.QuasiFinite

instance AlgebraicGeometry.instIsStableUnderCompositionSchemeLocallyQuasiFinite : CategoryTheory.MorphismProperty.IsStableUnderComposition @LocallyQuasiFinite

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

@[instance 100]

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

@[instance 100]

instance AlgebraicGeometry.instLocallyQuasiFiniteOfIsImmersion {X Y : Scheme} (f : X ⟶ Y) [IsImmersion f] : LocallyQuasiFinite f

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

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

instance AlgebraicGeometry.instIsMultiplicativeSchemeLocallyQuasiFinite : CategoryTheory.MorphismProperty.IsMultiplicative @LocallyQuasiFinite

instance AlgebraicGeometry.instIsStableUnderBaseChangeSchemeLocallyQuasiFinite : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @LocallyQuasiFinite

instance AlgebraicGeometry.instLocallyQuasiFiniteFstScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [LocallyQuasiFinite g] : LocallyQuasiFinite (CategoryTheory.Limits.pullback.fst f g)

instance AlgebraicGeometry.instLocallyQuasiFiniteSndScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [LocallyQuasiFinite f] : LocallyQuasiFinite (CategoryTheory.Limits.pullback.snd f g)

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

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

instance AlgebraicGeometry.instRespectsSchemeLocallyQuasiFiniteIsOpenImmersion : CategoryTheory.MorphismProperty.Respects (@LocallyQuasiFinite) IsOpenImmersion

theorem AlgebraicGeometry.IsLocallyArtinian.of_locallyQuasiFinite {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] [IsLocallyArtinian Y] : IsLocallyArtinian X

instance AlgebraicGeometry.instIsLocallyArtinianFiberOfLocallyQuasiFinite {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] (y : ↥Y) : IsLocallyArtinian (Scheme.Hom.fiber f y)

theorem AlgebraicGeometry.Scheme.Hom.isDiscrete_preimage_singleton {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] (y : ↥Y) : IsDiscrete (⇑f ⁻¹' {y})

theorem AlgebraicGeometry.Scheme.Hom.isDiscrete_preimage {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] {s : Set ↥Y} (hs : IsDiscrete s) : IsDiscrete (⇑f ⁻¹' s)

instance AlgebraicGeometry.instIsArtinianSchemeFiberOfLocallyQuasiFiniteOfQuasiCompact {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] [QuasiCompact f] (y : ↥Y) : IsArtinianScheme (Scheme.Hom.fiber f y)

theorem AlgebraicGeometry.Scheme.Hom.finite_preimage_singleton {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] [QuasiCompact f] (y : ↥Y) : (⇑f ⁻¹' {y}).Finite

@[deprecated AlgebraicGeometry.Scheme.Hom.finite_preimage_singleton (since := "2026-02-05")]

theorem AlgebraicGeometry.IsFinite.finite_preimage_singleton {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] [QuasiCompact f] (y : ↥Y) : (⇑f ⁻¹' {y}).Finite

Alias of AlgebraicGeometry.Scheme.Hom.finite_preimage_singleton.

theorem AlgebraicGeometry.Scheme.Hom.finite_preimage {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] [QuasiCompact f] {s : Set ↥Y} (hs : s.Finite) : (⇑f ⁻¹' s).Finite

theorem AlgebraicGeometry.Scheme.Hom.tendsto_cofinite_cofinite {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] [QuasiCompact f] : Filter.Tendsto (⇑f) Filter.cofinite Filter.cofinite

theorem AlgebraicGeometry.IsFinite.of_locallyQuasiFinite {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] [QuasiCompact f] [IsLocallyArtinian Y] : IsFinite f

instance AlgebraicGeometry.instIsFiniteFiberToSpecResidueFieldOfLocallyQuasiFiniteOfQuasiCompact {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] [QuasiCompact f] (x : ↥Y) : IsFinite (Scheme.Hom.fiberToSpecResidueField f x)

theorem AlgebraicGeometry.LocallyQuasiFinite.of_fiberToSpecResidueField {X Y : Scheme} (f : X ⟶ Y) (hf : ∀ (x : ↥Y), LocallyQuasiFinite (Scheme.Hom.fiberToSpecResidueField f x)) : LocallyQuasiFinite f

@[deprecated AlgebraicGeometry.LocallyQuasiFinite.of_fiberToSpecResidueField (since := "2026-02-15")]

theorem AlgebraicGeometry.LocallyQuasiFinite.of_isFinite_fiberToSpecResidueField {X Y : Scheme} (f : X ⟶ Y) (hf : ∀ (x : ↥Y), LocallyQuasiFinite (Scheme.Hom.fiberToSpecResidueField f x)) : LocallyQuasiFinite f

Alias of AlgebraicGeometry.LocallyQuasiFinite.of_fiberToSpecResidueField.

theorem AlgebraicGeometry.locallyQuasiFinite_iff_isFinite_fiber {X Y : Scheme} {f : X ⟶ Y} [QuasiCompact f] : LocallyQuasiFinite f ↔ ∀ (x : ↥Y), IsFinite (Scheme.Hom.fiberToSpecResidueField f x)

@[instance 100]

instance AlgebraicGeometry.instLocallyQuasiFiniteOfIsPreimmersion {X Y : Scheme} (f : X ⟶ Y) [IsPreimmersion f] : LocallyQuasiFinite f

theorem AlgebraicGeometry.locallyQuasiFinite_iff_isDiscrete_preimage_singleton {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFiniteType f] : LocallyQuasiFinite f ↔ ∀ (x : ↥Y), IsDiscrete (⇑f ⁻¹' {x})

theorem AlgebraicGeometry.LocallyQuasiFinite.of_finite_preimage_singleton {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] (hf : ∀ (x : ↥Y), (⇑f ⁻¹' {x}).Finite) : LocallyQuasiFinite f

theorem AlgebraicGeometry.locallyQuasiFinite_iff_finite_preimage_singleton {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFiniteType f] [QuasiCompact f] : LocallyQuasiFinite f ↔ ∀ (x : ↥Y), (⇑f ⁻¹' {x}).Finite

theorem AlgebraicGeometry.LocallyQuasiFinite.of_injective {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFiniteType f] (hf : Function.Injective ⇑f) : LocallyQuasiFinite f

@[instance 100]

instance AlgebraicGeometry.instLocallyQuasiFiniteOfLocallyOfFiniteTypeOfUniversallyInjective {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFiniteType f] [UniversallyInjective f] : LocallyQuasiFinite f

def AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) : Prop

A morphism f : X ⟶ Y is quasi-finite at x : X if the stalk map 𝒪_{X, x} ⟶ 𝒪_{Y, f x} is quasi-finite.

Equations

• AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt f x = (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x)).QuasiFinite

theorem AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.quasiFiniteAt {X Y : Scheme} {f : X ⟶ Y} {x : ↥X} (hx : QuasiFiniteAt f x) {V : X.Opens} (hV : IsAffineOpen V) {U : Y.Opens} (hU : IsAffineOpen U) (hVU : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (hxV : x ∈ V.carrier) : (CommRingCat.Hom.hom (appLE f U V hVU)).QuasiFiniteAt (hV.primeIdealOf ⟨x, hxV⟩).asIdeal

theorem AlgebraicGeometry.Scheme.Hom.quasiFiniteAt {X Y : Scheme} (f : X ⟶ Y) [LocallyQuasiFinite f] (x : ↥X) : QuasiFiniteAt f x

theorem AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_comp_iff_of_isOpenImmersion {X Y Z : Scheme} {f : X ⟶ Y} {g : Y ⟶ Z} {x : ↥X} [IsOpenImmersion f] : QuasiFiniteAt (CategoryTheory.CategoryStruct.comp f g) x ↔ QuasiFiniteAt g (f x)

theorem AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_comp_iff {X Y Z : Scheme} {f : X ⟶ Y} {g : Y ⟶ Z} {x : ↥X} [LocallyQuasiFinite g] : QuasiFiniteAt (CategoryTheory.CategoryStruct.comp f g) x ↔ QuasiFiniteAt f x

theorem AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_iff {X Y : Scheme} {f : X ⟶ Y} {x : ↥X} : QuasiFiniteAt f x ↔ LocallyQuasiFinite (CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) f)

theorem AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber {X Y : Scheme} {f : X ⟶ Y} [LocallyOfFiniteType f] {x : ↥X} : QuasiFiniteAt f x ↔ IsOpen {asFiber f x}

theorem AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.isClopen_singleton_asFiber {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] {x : ↥X} (hx : QuasiFiniteAt f x) : IsClopen {asFiber f x}