Theorems · Inductive type · algebraic geometry

AlgebraicGeometry.LocallyQuasiFinite

{X Y : AlgebraicGeometry.Scheme} → (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 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

Cited by

29 results in Mathlib

Foundations

Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound