English
The graded multiplication map is bilinear in each argument, i.e., it respects addition and scalar multiplication in each input variable.
Русский
Градуированное умножение билинеарно по каждому аргументу: сохраняет сложение и скалярное умножение в каждом входном аргументе.
LaTeX
$$$\\forall i,j, a,a'\\in A_i, b,b'\\in A_j, r\\in R:\\; gMul(a+a')(b)=gMul(a,b)+gMul(a',b),\\; gMul(a)(b+b')=gMul(a,b)+gMul(a,b').$$$
Lean4
/-- A direct sum of copies of an `Algebra` inherits the algebra structure. -/
@[simps]
instance directSumGAlgebra {R A : Type*} [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] :
DirectSum.GAlgebra R fun _ : ι => A
where
toFun := (algebraMap R A).toAddMonoidHom
map_one := (algebraMap R A).map_one
map_mul a b := Sigma.ext (zero_add _).symm (heq_of_eq <| (algebraMap R A).map_mul a b)
commutes := fun _ ⟨_, _⟩ => Sigma.ext ((zero_add _).trans (add_zero _).symm) (heq_of_eq <| Algebra.commutes _ _)
smul_def := fun _ ⟨_, _⟩ => Sigma.ext (zero_add _).symm (heq_of_eq <| Algebra.smul_def _ _)
