Square-zero linear maps with coefficients in a commutative algebra

Let f : M →ₗ[R] B be a linear map into an R-algebra all of whose values square to zero, and let H be a commutative R-algebra. Then the extension f.rTensor H : M ⊗[R] H → B ⊗[R] H again has square-zero values. Commutativity of H is essential: the cross terms of (∑ f mᵢ ⊗ hᵢ) ^ 2 cancel in pairs because f mᵢ * f mⱼ = -(f mⱼ * f mᵢ) while hᵢ * hⱼ = hⱼ * hᵢ.

This is exactly the hypothesis of ExteriorAlgebra.lift, so a linear map M →ₗ[R] M' ⊗[R] H with coefficients in H followed by ExteriorAlgebra.ι extends to an algebra homomorphism ExteriorAlgebra R M →ₐ[R] ExteriorAlgebra R M' ⊗[R] H. The coaction of the exterior algebra of a comodule over a commutative bialgebra is built this way.

Main results

• TauCeti.rTensor_mul_add_mul_swap_eq_zero: tensor-extended values anticommute.
• TauCeti.rTensor_mul_self_eq_zero: square-zero values persist after tensoring with a commutative algebra on the right.

theorem TauCeti.rTensor_mul_add_mul_swap_eq_zero {R : Type u_1} {M : Type u_2} {B : Type u_3} {H : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring B] [Algebra R B] [CommSemiring H] [Algebra R H] {f : M →ₗ[R] B} (hf : ∀ (m : M), f m * f m = 0) (x y : TensorProduct R M H) : (LinearMap.rTensor H f) x * (LinearMap.rTensor H f) y + (LinearMap.rTensor H f) y * (LinearMap.rTensor H f) x = 0

The cross terms of the square of a sum vanish: values of f.rTensor H anticommute.

theorem TauCeti.rTensor_mul_self_eq_zero {R : Type u_1} {M : Type u_2} {B : Type u_3} {H : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring B] [Algebra R B] [CommSemiring H] [Algebra R H] {f : M →ₗ[R] B} (hf : ∀ (m : M), f m * f m = 0) (x : TensorProduct R M H) : (LinearMap.rTensor H f) x * (LinearMap.rTensor H f) x = 0

If every value of f squares to zero, so does every value of f.rTensor H for a commutative algebra H.