Commit 2023-11-13 21:35 2fed2bb8

View on Github →

refactor(Algebra): Define the center appropriately for non-associative algebras (#6996) For a sensible theory, we require that the centre of an algebra is closed under multiplication. The definition currently in Mathlib works for associative algebras, but not non-associative algebras. This PR uses the definition from Cabrera García and Rodríguez Palacios, which works for any multiplication (addition) and which coincides with the current definition in the associative case. I did consider whether the centralizer should also be re-defined in terms of operator commutation, but this still results in a centralizer which is not closed under multiplication in the non-associative case. I have therefore retained the current definition, but changed centralizer_eq_top_iff_subset and centralizer_univ to only work in the associative case.

Estimated changes

modified theorem Set.smul_mem_center
modified theorem Set.star_mem_center
modified theorem Subgroup.mem_center_iff
modified theorem Submonoid.mem_center_iff
added structure IsAddCentral
added structure IsMulCentral
modified def Set.center
modified theorem Set.center_eq_univ
modified theorem Set.intCast_mem_center
modified theorem Set.inv_mem_center
modified theorem Set.mem_center_iff
modified theorem Set.mul_mem_center
modified theorem Set.natCast_mem_center
modified theorem Set.one_mem_center
modified theorem Set.zero_mem_center
modified theorem Subsemigroup.mem_center_iff
modified theorem Set.centralizer_univ
modified def Subsemiring.center
modified theorem Subsemiring.coe_center