English
The graded multiplication is encoded as a bilinear linear map: for fixed indices i,j there is a linear map A_i → A_j → A_{i+j} implementing the product a·b.
Русский
Градуированное умножение задаётся билинейным линейным отображением: для фиксированных индексов i,j имеется линейное отображение A_i → A_j → A_{i+j}, реализующее произведение a·b.
LaTeX
$$$gMulLHom^{i j}: A_i \\to_\\!R (A_j \\to_\\!R A_{i+j})$, с $gMulLHom(a)(b)=\\, GradedMonoid.GMul.mul(a,b)$$$
Lean4
/-- The piecewise multiplication from the `Mul` instance, as a bundled linear map.
This is the graded version of `LinearMap.mul`, and the linear version of `DirectSum.gMulHom` -/
@[simps]
def gMulLHom {i j} : A i →ₗ[R] A j →ₗ[R] A (i + j)
where
toFun
a :=
{ toFun := fun b => GradedMonoid.GMul.mul a b
map_smul' := fun r x => by injection (smul_comm r (GradedMonoid.mk _ a) (GradedMonoid.mk _ x)).symm
map_add' := GNonUnitalNonAssocSemiring.mul_add _ }
map_smul' r x := LinearMap.ext fun y => by injection smul_assoc r (GradedMonoid.mk _ x) (GradedMonoid.mk _ y)
map_add' _ _ := LinearMap.ext fun _ => GNonUnitalNonAssocSemiring.add_mul _ _ _
