Proposition. Composition and field multiplication [fdip-0011]
✍️source

  • October 20, 2026

Let \(R\) be a commutative unital ring. For \(R\)-modules \(M,N,P\), use \(\operatorname {Hom}_R(M,N)\) for additive, scalar-preserving maps. Thus linearity fixes \(\sigma =\operatorname {id}_R\). Given \(A\in \operatorname {Hom}_R(M,N)\) and \(B\in \operatorname {Hom}_R(N,P)\), write \[BA=B\circ A:M\to P.\] Composition is associative and \(R\)-bilinear where the types match. In particular, the endomorphisms \(\operatorname {End}_R(M)=\operatorname {Hom}_R(M,M)\) form an associative unital \(R\)-algebra, with unit \(I_M\) and central scalar map \(r\mapsto rI_M\).

On the vertex-field module, pointwise products are the multiplication operators. The map \(f\mapsto M_f\) is an injective \(R\)-algebra homomorphism into \(\operatorname {End}_R(\mathcal F_R(V))\). The proof evaluates those algebra laws. Example [fdip-00AP] exhibits endomorphisms that do not commute.

Proof. 

  • October 20, 2026

Pointwise addition and scalar multiplication make \(\operatorname {Hom}_R(M,N)\) a module: the linearity equations are preserved by both operations. If \(A,B\) are composable, then \(BA(rx+y)=B(rAx+Ay)=rBAx+BAy\), so \(BA\) is linear. For a third composable map \(C\), \((CB)A(x)=C(B(Ax))=C(BA)(x)\). The identity map is a two-sided unit. For composable maps with common source and target, \[\begin {aligned} B(A+A')(x)&=B(Ax)+B(A'x),\\ (B+B')A(x)&=B(Ax)+B'(Ax),\\ B(rA)(x)&=rB(Ax),\qquad (rB)A(x)=rB(Ax). \end {aligned}\] These prove distributivity and bilinearity. For an endomorphism \(A\), \((rI)A(x)=rAx=A(rx)=A(rI)(x)\), proving centrality of the scalar map; its unit, addition and product laws follow immediately by evaluation.

Pointwise multiplication makes \(M_f\) linear. Evaluating the 4 identities \[M_{f+g}=M_f+M_g,\quad M_{rf}=rM_f,\quad M_{fg}=M_fM_g,\quad M_1=I\] on a field proves them using the ring laws. If \(M_f=M_g\), applying both maps to the constant field \(1\) yields \(f=g\); this also holds when \(V\) is empty or \(R\) is the zero ring.

The Hom-module and algebra conventions are [stacks2017stacks, Section 10.10; Section 22.2], Tags 0581 and 09JF; the field multiplication assertions are the direct calculation above. Mathlib's Module.End.mul_eq_comp and Module.End.mul_apply give this right-factor-first product. These declarations do not assert that arbitrary maps with different endpoints form one algebra, or that a formal generator presentation is faithful.