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.

TODO (@erdOne):

• If f is quasi-compact, then f is locally quasi-finite iff all the fibers f⁻¹(x) are κ(x)-finite.
• If f is locally of finite type, then f is locally quasi-finite iff f has discrete fibers.
• 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.

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.

TODO (@erdOne): prove the following If one assumes quasi-compact, this is equivalent to all the fibers f⁻¹(x) being κ(x)-finite. If one assumes locally of finite type, this is equivalent to f having discrete fibers. If one assumes 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

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)