English
An Extensionality principle: two algebra homomorphisms from the direct sum are equal if they agree on all the generators coming from the inclusions of each summand.
Русский
Принцип экстенсиональности: два гомоморфизма от прямой суммы равны, если они совпадают на включениях каждого слагаемого.
LaTeX
$$$\\forall f,g: (\\bigoplus_i A_i) \\to_R B,\\; (\\forall i,x, f(of_i\\, x)=g(of_i\\, x))\\Rightarrow f=g$$$
Lean4
/-- Two `AlgHom`s out of a direct sum are equal if they agree on the generators.
See note [partially-applied ext lemmas]. -/
@[ext]
theorem algHom_ext' ⦃f g : (⨁ i, A i) →ₐ[R] B⦄
(h : ∀ i, f.toLinearMap.comp (lof _ _ A i) = g.toLinearMap.comp (lof _ _ A i)) : f = g :=
AlgHom.toLinearMap_injective <| DirectSum.linearMap_ext _ h
