The left regular module and its tensor powers detect linear and tensor identities

Claim 1: $1_A$ is a two-sided identity of the regular module, so $a=a\cdot 1_A$ and $b=b\cdot 1_A$ by [F1]; conversely $a\cdot 1_A=b\cdot 1_A$ is $a=b$.

Claim 2: for $a\in A$ the map $A^{\times n}\to A^{\otimes n}$, $(a_1,\dots ,a_n)\mapsto (a{a}_1)\otimes a_2\otimes \cdots \otimes a_n$, is $R$-multilinear, so it induces an $R$-linear map ${\lambda }_a:A^{\otimes n}\to A^{\otimes n}$ with ${\lambda }_a(a_1\otimes \cdots \otimes a_n)=(a{a}_1)\otimes a_2\otimes \cdots \otimes a_n$ by [F2]. On elementary tensors ${\lambda }_a{\lambda }_b={\lambda }_{ab}$, ${\lambda }_{a+b}={\lambda }_a+{\lambda }_b$ and ${\lambda }_{1_A}=\mathrm{id}$, and since elementary tensors span [F2], these identities extend to all of $A^{\otimes n}$, so $a\cdot z:={\lambda }_a(z)$ makes $A^{\otimes n}$ a left $A$-module [F1]. The $n$-fold multiplication $a_1\otimes \cdots \otimes a_n\mapsto a_1{a}_2\cdots a_n$ is the $R$-linear map $\mu :A^{\otimes n}\to A$ induced by the $R$-multilinear product [F1, F2], and $\mu ({\lambda }_a(z))=a\mu (z)$ for elementary tensors and hence for all $z$ by linearity. If $a\cdot z=b\cdot z$ for all $z$, then in particular ${\lambda }_a(1_A^{\otimes n})={\lambda }_b(1_A^{\otimes n})$, that is $a\otimes 1_A^{\otimes (n-1)}=b\otimes 1_A^{\otimes (n-1)}$; applying $\mu$ gives $a\cdot 1_A=b\cdot 1_A$, and $a\cdot 1_A=a$ while $b\cdot 1_A=b$ by [F1], so $a=b$: the single element $1_A^{\otimes n}$ detects equality. The right-handed statement is the mirror computation with ${\rho }_a(a_1\otimes \cdots \otimes a_n)=a_1\otimes \cdots \otimes (a_{n}a)$.

Claim 3: by [F2] the $R$-multilinear map $f$ induces the unique $R$-linear map $\bar{f}:A^{\otimes n}\to M$ with $\bar{f}(a_1\otimes \cdots \otimes a_n)=f(a_1,\dots ,a_n)$, and likewise for $g$; if $f=g$ as functions then $\bar{f}$ and $\bar{g}$ agree on every elementary tensor, hence on the whole tensor power, so $\bar{f}=\bar{g}$. Conversely, if $\bar{f}=\bar{g}$, then for every tuple $f(a_1,\dots ,a_n)=\bar{f}(a_1\otimes \cdots \otimes a_n)=\bar{g}(a_1\otimes \cdots \otimes a_n)=g(a_1,\dots ,a_n)$, so the multilinear maps agree on all tuples and the induced maps agree on all pure tensors.

Claim 4: the quotient map $\pi :A\to A\mathrm{/}I$ is a surjective $R$-algebra homomorphism, and ${\pi }^{\otimes n}:=\pi \otimes \cdots \otimes \pi :A^{\otimes n}\to (A\mathrm{/}I{)}^{\otimes n}$ is surjective by iterated [F3]; it sends an elementary tensor $a_1\otimes \cdots \otimes a_n$ to $\pi (a_1)\otimes \cdots \otimes \pi (a_n)$. If $\bar{\phi }:(A\mathrm{/}I{)}^{\otimes n}\to Q$ is an $R$-linear map out of the quotient tensor power, then to check an identity between two such maps on images of pure tensors of $A$ one must first know that each map is well defined on the quotient, equivalently, any proposed map $\phi :A^{\otimes n}\to Q$ must annihilate $\ker ({\pi }^{\otimes n})$, so that $\phi =\bar{\phi }\circ {\pi }^{\otimes n}$ for a well-defined map $\bar{\phi }$; that is the descent obligation, and surjectivity of ${\pi }^{\otimes n}$ alone equips no map out of $A^{\otimes n}$ with a well-defined value on a class. For ring-level descent the quotient universal property [F4] is the tool: a homomorphism killing $I$ factors uniquely through $\pi$.

Collecting: step 1.1 proves claim 1, step 1.2 proves both the module structure and the detection statement of claim 2 together with its right-handed mirror, step 1.3 proves both directions of claim 3, and step 1.4 records the descent warning of claim 4.