Tensor naturality of exterior-algebra generators

The inclusion of generators into an exterior algebra commutes with algebra homomorphisms on the right tensor factor. This lets tensor constructions on generators pass through changes of the coefficient algebra, in particular the comultiplication and counit of a bialgebra.

theorem TauCeti.ExteriorAlgebra.map_id_rTensor_ι {R : Type u_1} {M : Type u_2} {H : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [Semiring H] [Algebra R H] {K : Type u_4} [Semiring K] [Algebra R K] (φ : H →ₐ[R] K) (z : TensorProduct R M H) : (Algebra.TensorProduct.map (AlgHom.id R (ExteriorAlgebra R M)) φ) ((LinearMap.rTensor H (ExteriorAlgebra.ι R)) z) = (LinearMap.rTensor K (ExteriorAlgebra.ι R)) ((LinearMap.lTensor M φ.toLinearMap) z)

An algebra homomorphism on the right tensor factor commutes with the inclusion of exterior-algebra generators.