Commit 2025-03-30 16:02 ea841e87

View on Github →

refactor: default to left modules for CStarModule (#22967) When CStarModule was introduced, the hypotheses assumed a right action of the C⋆-algebra A on the module E (i.e., a SMul Aᵐᵒᵖ E instance). On the one hand, this is consistent with the literature (which also defaults to right-actions), but on the other hand, it will cause problems in the future. In particular, we will need to consider C⋆-bimodules, but if we default to right actions, then to get a left C⋆-module structure we would need a SMul (Aᵐᵒᵖ)ᵐᵒᵖ E instance. In this PR we switch so that the default for CStarModules are left-actions, consistent with the rest of Mathlib. In addition, we remove the outParam condition on A in the CStarModule class. Indeed, we may need to consider C⋆-modules over multiple C⋆-algebras simultaneously (the canonical example is A and its unitization A⁺¹, which arises frequently). This necessitates a change to the type synonym WithCStarModule so that A is an explicit parameter. In addition, the variable A is now explicit in a few declarations which otherwise only mention terms of E and their norms (e.g., CStarModule.norm_sq_eq).

Estimated changes

Modified Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean

modified theorem CStarMatrix.inner_toCLM_conjTranspose_left

modified theorem CStarMatrix.inner_toCLM_conjTranspose_right

modified theorem CStarMatrix.mul_entry_mul_eq_inner_toCLM

deleted theorem CStarMatrix.normedSpaceCore:

added theorem CStarMatrix.normedSpaceCore

modified def CStarMatrix.toCLM

modified def CStarMatrix.toCLMNonUnitalAlgHom

modified theorem CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM

modified theorem CStarMatrix.toCLM_apply

modified theorem CStarMatrix.toCLM_apply_eq_sum

modified theorem CStarMatrix.toCLM_apply_single

modified theorem CStarMatrix.toCLM_apply_single_apply

Modified Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean

modified theorem WithCStarModule.inner_def

modified theorem WithCStarModule.inner_single_left

modified theorem WithCStarModule.inner_single_right

modified theorem WithCStarModule.max_le_prod_norm

modified theorem WithCStarModule.norm_apply_le_norm

modified theorem WithCStarModule.norm_equiv_le_norm_pi

modified theorem WithCStarModule.norm_equiv_le_norm_prod

modified theorem WithCStarModule.pi_inner

modified theorem WithCStarModule.pi_norm

modified theorem WithCStarModule.pi_norm_le_sum_norm

modified theorem WithCStarModule.pi_norm_sq

modified theorem WithCStarModule.prod_inner

modified theorem WithCStarModule.prod_norm

modified theorem WithCStarModule.prod_norm_le_norm_add

modified theorem WithCStarModule.prod_norm_sq

Modified Mathlib/Analysis/CStarAlgebra/Module/Defs.lean

modified theorem CStarModule.inner_mul_inner_swap_le

modified theorem CStarModule.inner_op_smul_left

modified theorem CStarModule.norm_sq_eq

Modified Mathlib/Analysis/CStarAlgebra/Module/Synonym.lean

modified def WithCStarModule.addEquiv

modified def WithCStarModule.equiv

modified def WithCStarModule.equivL

modified theorem WithCStarModule.equiv_add

modified theorem WithCStarModule.equiv_fst

modified theorem WithCStarModule.equiv_neg

modified theorem WithCStarModule.equiv_pi_apply

modified theorem WithCStarModule.equiv_smul

modified theorem WithCStarModule.equiv_snd

modified theorem WithCStarModule.equiv_sub

modified theorem WithCStarModule.equiv_symm_fst

modified theorem WithCStarModule.equiv_symm_neg

modified theorem WithCStarModule.equiv_symm_smul

modified theorem WithCStarModule.equiv_symm_snd

modified theorem WithCStarModule.equiv_symm_zero

modified theorem WithCStarModule.equiv_zero

modified def WithCStarModule.linearEquiv

modified def WithCStarModule.uniformEquiv

modified theorem WithCStarModule.zero_apply

modified theorem WithCStarModule.zero_fst

modified theorem WithCStarModule.zero_snd

modified def WithCStarModule