Commit 2024-08-15 08:47 58d407ba

feat: add the WithCStarModule type synonym (#15763) It is often the case that we want to construct a CStarModule instance on a type that is already endowed with a norm, and it has a different norm which makes it into a CStarModule. For this reason, we create a type synonym WithCStarModule which is endowed with the requisite CStarModule instance. We also introduce the scoped notation C⋆ᵐᵒᵈ for this type synonym. The common use cases are, when A is a C⋆-algebra:

• A itself over A
• E × F where E and F are CStarModules over A
• Π i, E i where E i is a CStarModule over A and i : ι with ι a Fintype
• E where E is an InnerProductSpace over ℂ The WithCStarModule synonym is of vital importance, especially because the CStarModule class marks A as an outParam. Indeed, we want to infer A from the type of E, but, as with modules, a type E can be a CStarModule over different C⋆-algebras. For example, note that if A is a C⋆-algebra, then so is A × A, and therefore we may consider both A and A × A as CStarModules over themselves, respectively. However, we may also consider A × A as a CStarModule over A. However, by utilizing the type synonym, these actually correspond to different types, namely:
• A as a CStarModule over A corresponds to C⋆ᵐᵒᵈ A
• A × A as a CStarModule over A × A corresponds to C⋆ᵐᵒᵈ (A × A)
• A × A as a CStarModule over A corresponds to C⋆ᵐᵒᵈ (C⋆ᵐᵒᵈ A × C⋆ᵐᵒᵈ A)