English
Two algebra homomorphisms from a direct sum to B are equal if they agree on the images of all generators coming from the component inclusions.
Русский
Два алгебра-гомоморфи from прямой сумму в B равны, если они совпадают на образах всех генераторов, соответствующих включениям компонент.
LaTeX
$$$\\forall f,g:(\\bigoplus_i A_i)\\to_R B,\\; (\\forall i, f\\circ (lof_i)=g\\circ (lof_i))\\Rightarrow f=g$$$
Lean4
/-- A family of `LinearMap`s preserving `DirectSum.GOne.one` and `DirectSum.GMul.mul`
describes an `AlgHom` on `⨁ i, A i`. This is a stronger version of `DirectSum.toSemiring`.
Of particular interest is the case when `A i` are bundled subobjects, `f` is the family of
coercions such as `Submodule.subtype (A i)`, and the `[GMonoid A]` structure originates from
`DirectSum.GMonoid.ofAddSubmodules`, in which case the proofs about `GOne` and `GMul`
can be discharged by `rfl`. -/
@[simps]
def toAlgebra (f : ∀ i, A i →ₗ[R] B) (hone : f _ GradedMonoid.GOne.one = 1)
(hmul : ∀ {i j} (ai : A i) (aj : A j), f _ (GradedMonoid.GMul.mul ai aj) = f _ ai * f _ aj) : (⨁ i, A i) →ₐ[R] B :=
{
toSemiring (fun i => (f i).toAddMonoidHom) hone
@hmul with
toFun := toSemiring (fun i => (f i).toAddMonoidHom) hone @hmul
commutes' := fun r => by
change toModule R _ _ f (algebraMap R _ r) = _
rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, map_smul, one_def, ← lof_eq_of R,
toModule_lof, hone] }
