English
Two R-algebra morphisms out of A[ε] are equal if they agree on the image of A and on the ε-multiples of A.
Русский
Два R-алгебраоднозначных отображения из A[ε] равны, если они согласны на изображении A и на множителях ε от A.
LaTeX
$$$\text{If } f,g: A[ε] \to B \text{ are } R\text{-algebra morphisms, then } f=g \text{ provided } f|_{A} = g|_{A} \text{ and } f(εa) = g(εa) \text{ for all } a \in A.$$$
Lean4
/-- For two `R`-algebra morphisms out of `A[ε]` to agree, it suffices for them to agree on the
elements of `A` and the `A`-multiples of `ε`. -/
@[ext 1100]
nonrec theorem algHom_ext' ⦃f g : A[ε] →ₐ[R] B⦄ (hinl : f.comp (inlAlgHom _ _ _) = g.comp (inlAlgHom _ _ _))
(hinr :
f.toLinearMap ∘ₗ (LinearMap.toSpanSingleton A A[ε] ε).restrictScalars R =
g.toLinearMap ∘ₗ (LinearMap.toSpanSingleton A A[ε] ε).restrictScalars R) :
f = g :=
algHom_ext' hinl
(by
ext a
change f (inr a) = g (inr a)
simpa only [inr_eq_smul_eps] using DFunLike.congr_fun hinr a)
