Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-02 00:16 9264b15e

View on Github →

feat(algebra/algebra/bilinear): make algebra.lmul to apply to non-unital (non-assoc) algebras (#15310) Multiplication in an algebra is a bilinear map. Previously, this was called algebra.lmul ("l" for "linear") and what was actually constructed was an algebra homomorphism A →ₐ[R] (End R A), where A is an R-algebra. As a result, this object (and the derived linear maps algebra.lmul_left and algebra.lmul_right, and others) only exists when A is a unital R-algebra. Of course, when A is a non-unital (even non-associative) algebra, this bilinear map A →ₗ[R] A →ₗ[R] A still exists, but it can't be upgraded to an algebra homomorphism as above. When A is associative, it can be upgraded to non-unital algebra homomorphism. In this PR, we define all three of these multiplication maps as linear_map.mul, non_unital_alg_hom.lmul and algebra.lmul, along with appropriate simp lemmas stating that the underlying functions coincide. All existing lemmas about the maps are preserved, but each in the correct generality. In so doing, we also move most the results and definitions in this file into the linear_map namespace (which is also why we call the simplest map linear_map.mul instead of linear_map.lmul as the l in the latter would be redundant).

Estimated changes

deleted def algebra.lmul'
deleted theorem algebra.lmul'_apply
modified def algebra.lmul
deleted theorem algebra.lmul_apply
deleted theorem algebra.lmul_injective
deleted def algebra.lmul_left
deleted theorem algebra.lmul_left_apply
deleted theorem algebra.lmul_left_mul
deleted theorem algebra.lmul_left_one
deleted def algebra.lmul_right
deleted theorem algebra.lmul_right_apply
deleted theorem algebra.lmul_right_mul
deleted theorem algebra.lmul_right_one
deleted theorem algebra.pow_lmul_left
deleted theorem algebra.pow_lmul_right
added def linear_map.mul'
added theorem linear_map.mul'_apply
added def linear_map.mul
added theorem linear_map.mul_apply'