English
For an essentially finite type morphism f, there is a finite set F ⊆ S of essential generators that suffices to determine maps out of S together with the base map f.
Русский
Для гомоморфизма f, являющегося существенно конечного типа, существует конечное множество F ⊆ S подназваний правильных генераторов, которое достаточно для определения отображений из S вместе с базовым отображением f.
LaTeX
$$$\text{hf}: f\!:\! R \to S\text{ is EssFiniteType} \;\Rightarrow\; \exists F = hf.finset \subseteq S,\; \text{Finite}(F) \,\land \, \forall g_1,g_2: S\to T,\; (g_1\circ f = g_2\circ f) \land (\forall x\in F,\; g_1(x)=g_2(x)) \Rightarrow g_1=g_2.$$$
Lean4
/-- A choice of "essential generators" for a ring hom essentially of finite type.
See `Algebra.EssFiniteType.ext`. -/
noncomputable def finset (hf : f.EssFiniteType) : Finset S :=
letI := f.toAlgebra
haveI : Algebra.EssFiniteType R S := hf
Algebra.EssFiniteType.finset R S
