Documentation

Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

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) :

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

Instances

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] :

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) :

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

Equations

Instances For

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}