English
The direct sum of algebras over an index set carries a natural algebra structure, with the embedding maps as algebra homomorphisms and the product defined componentwise via the graded algebra structure.
Русский
Прямая сумма алгебр по индексу имеет естественную алгебраическую структуру; вложения являются гомоморфизмами алгебр, а произведение определяется по компонентам через градуированную структуру.
LaTeX
$$$\\text{DirectSum}\\;\\text{GAlgebra} \\;R\\;A\\;\\Rightarrow\\; \\text{Algebra }R(\\bigoplus_i A_i)$$$
Lean4
instance : Algebra R (⨁ i, A i)
where
algebraMap :=
{ toFun := (DirectSum.of A 0).comp GAlgebra.toFun
map_zero' := AddMonoidHom.map_zero _
map_add' := AddMonoidHom.map_add _
map_one' := DFunLike.congr_arg (DirectSum.of A 0) GAlgebra.map_one
map_mul' a
b := by
simp only [AddMonoidHom.comp_apply]
rw [of_mul_of]
apply DFinsupp.single_eq_of_sigma_eq (GAlgebra.map_mul a b) }
commutes' r
x := by
change AddMonoidHom.mul (DirectSum.of _ _ _) x = AddMonoidHom.mul.flip (DirectSum.of _ _ _) x
apply DFunLike.congr_fun _ x
ext i xi : 2
dsimp only [AddMonoidHom.comp_apply, AddMonoidHom.mul_apply, AddMonoidHom.flip_apply]
rw [of_mul_of, of_mul_of]
apply DFinsupp.single_eq_of_sigma_eq (GAlgebra.commutes r ⟨i, xi⟩)
smul_def' r
x := by
change DistribMulAction.toAddMonoidHom _ r x = AddMonoidHom.mul (DirectSum.of _ _ _) x
apply DFunLike.congr_fun _ x
ext i xi : 2
dsimp only [AddMonoidHom.comp_apply, DistribMulAction.toAddMonoidHom_apply, AddMonoidHom.mul_apply]
rw [DirectSum.of_mul_of, ← of_smul]
apply DFinsupp.single_eq_of_sigma_eq (GAlgebra.smul_def r ⟨i, xi⟩)
