Structures · Geometry

AlgebraicGeometry.LocallyQuasiFinite

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 fibers (via f.isDiscrete_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_finite_preimage_singleton: If f is of finite type, this is equivalent to f having finite fibers.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Shape

One type argument · adds quasiFinite_appLE