English
A ring homomorphism f: R → S is essentially of finite type if it factors as a localization map followed by a finite-type morphism; equivalently, there exists an intermediate ring A and maps R → A → S with the first map a localization and the second of finite type, such that f = (A → S) ∘ (R → A).
Русский
Кольцевое гомоморфизм f: R → S называется существенно конечного типа, если он раскладывается на локализацию R → A и гомоморфизм A → S конечного типа так, что f = (A → S) ∘ (R → A).
LaTeX
$$$ \operatorname{EssFiniteType}(f) \iff \exists A\, \exists l: R\to A\, ( \operatorname{IsLocalization}(l) \land \exists g: A\to S\, \operatorname{FiniteType}(g) \land f = g \circ l ). $$$
Lean4
/-- A ring hom is essentially of finite type if it is the composition of a localization map
and a ring hom of finite type. See `Algebra.EssFiniteType`. -/
@[algebraize Algebra.EssFiniteType]
def EssFiniteType (f : R →+* S) : Prop :=
letI := f.toAlgebra
Algebra.EssFiniteType R S
