English
Let f,g be S→T algebra homomorphisms; if they agree on a finite generating set of S over R, then f=g.
Русский
Пусть f,g — алгебра-гомоморфизмы S→T; если они совпадают на конечном базисе S над R, то f=g.
LaTeX
$$$\forall f,g: S \to_{R} T,\; (\forall s\in \text{finset } R S, f(s)=g(s)) \Rightarrow f=g$$$
Lean4
theorem algHom_ext [EssFiniteType R S] (f g : S →ₐ[R] T) (H : ∀ s ∈ finset R S, f s = g s) : f = g :=
by
suffices f.toRingHom = g.toRingHom by ext; exact RingHom.congr_fun this _
apply IsLocalization.ringHom_ext (EssFiniteType.submonoid R S)
suffices f.comp (IsScalarTower.toAlgHom R _ S) = g.comp (IsScalarTower.toAlgHom R _ S) by ext;
exact AlgHom.congr_fun this _
apply AlgHom.ext_of_adjoin_eq_top (s := {x | x.1 ∈ finset R S})
· exact adjoin_mem_finset R S
· rintro ⟨x, hx⟩ hx'; exact H x hx'
