redefining `Inner` in `InnerProductSpace 𝕜 𝕜`

Stream: mathlib4

[Jireh Loreaux]

Currently, the definition of InnerProductSpace 𝕜 𝕜 is:

/-- A field `𝕜` satisfying `RCLike` is itself a `𝕜`-inner product space. -/
instance RCLike.innerProductSpace : InnerProductSpace 𝕜 𝕜 where
  inner x y := conj x * y
  norm_sq_eq_inner x := by simp only [inner, conj_mul, ← ofReal_pow, ofReal_re]
  conj_symm x y := by simp only [mul_comm, map_mul, starRingEnd_self_apply]
  add_left x y z := by simp only [add_mul, map_add]
  smul_left x y z := by simp only [mul_assoc, smul_eq_mul, map_mul]

I would like to change the inner field to:

  inner x y := y * conj x

This is, of course, propositionally but not definitionally equal to the original. My reason for wanting this change is as follows. In C⋆-algebra theory, we like to consider an object called a (Hilbert) docs#CStarModule. These are essentially generalizations of InnerProductSpace where the scalars are replaced by a C⋆-algebra. In the literature, we generally consider these as right A-modules (where A is the C⋆-algebra), which is why CStarModule is currently set up with SMul Aᵐᵒᵖ E. However, I realized that we will need both left and right C⋆-modules, which makes me want to just take a SMul A E hypothesis instead.

Now, given any C⋆-algebra A, there is a natural CStarModule A A instance (with a left action) analogous to the InnerProductSpace 𝕜 𝕜 instance where the inner field is defined as inner x y := y * star x. Note that because the multiplication is non-commutative, we need inner to be defined this way in order to get the appropriate behavior with the (pre-existing!) left action of A on itself (i.e., we need ⟪x, a • y⟫ = a • ⟪x, y⟫ for a x y : A).

Herein lies the rub: ℂ is a C⋆-algebra, so it will inherit CStarModule ℂ ℂ and InnerProductSpace ℂ ℂ instances, which will result in a non-defeq diamond for Inner ℂ ℂ.

Does anyone see any problem with this? @Frédéric Dupuis, @Heather Macbeth, @Jon Bannon

[Yaël Dillies]

Oh, I really like the convention with the star on the left because it corresponds to applying the dual map corresponding to x to y

[Jireh Loreaux]

I think that's unaffected? Because that map uses innerSL which, for this specific type, gets redefined.

[Jireh Loreaux]

Also @Anatole Dedecker

[Jon Bannon]

This is a source of controversy in some places because the OA community generally uses a * star b (in Kadison-Ringrose, for example) but physics uses star a * b, so if you have been raised on the former, calculations with the latter can be stumbly, on paper. I've come around to star a * b for precisely the reason you mention, Jireh. In CStarModule-land, everyone uses this convention for the CStarModule valued inner products, which immediately puts it at odds with ordinary inner products in the trivial case where the C* algebra is the complex numbers.

[Jireh Loreaux]

Hold on, I don't think we're talking on the same wavelength.

[Jireh Loreaux]

I don't want to define ⟪x, y⟫ := x * star y, I want to define it as ⟪x, y⟫ := y * star x (as opposed the to current star x * y). My version will still agree with that of current Mathlib propositionally (i.e., conjugate linear in the first variable).

[Jireh Loreaux]

Literally all I want to do is use the fact that multiplication in 𝕜 is commutative.

[Jon Bannon]

OK. So this isn't a change at all. Knee-jerk, I was taken back to several discussions with J. Martin Lindsay in which he vociferously argued for conjugate linearity in the first coordinate. The only problem I can see might be that some people prefer the opposite.

The physicists like conjugate linearity in the first variable (in opposition to the OA traditional approach), and since in the trivial A-A C* module we typically define $\langle a, b \rangle = a^{*}b$ for $a,b \in A$ and develop the whole theory around this, it seemed better to adopt that.

Sorry for the noise!

[Jireh Loreaux]

In Mathlib we've been conjugate linear in the first coordinate since ... forever? I think. But sure, that's a stance we've taken.

[Jon Bannon]

OK. No problem, then. I should probably have checked Mathlib before commenting...or carefully read your question.

[Eric Wieser]

Is it relevant that I was intending to eventually make InnerProductSpace K V (or rather, its parent NormedSpace K V) imply both a left- and right-action by K?

[Jireh Loreaux]

:thinking: I think that's fine?

[Jireh Loreaux]

(deleted)

[Jireh Loreaux]

Oh, I guess it depends on what your definition of the right action is?

[Yaël Dillies]

Jireh Loreaux said:

I don't want to define ⟪x, y⟫ := x * star y, I want to define it as ⟪x, y⟫ := y * star x (as opposed the to current star x * y).

I completely misread this! I am now unsaddened

[Jon Bannon]

(I'm glad you did too, @Yaël Dillies ...I feel a tiny bit less silly, now. :rolling_on_the_floor_laughing: )

[Eric Wieser]

So just to check, we want

⟪x, a • y⟫ = a • ⟪x, y⟫

and not the more symmetric

⟪a •> x, y⟫ = a •> ⟪x, y⟫
⟪x, y <• a⟫ = ⟪x, y⟫ <• a

[Eric Wieser]

(and am I right in saying we currently have the latter?)

[Jireh Loreaux]

No on both counts.

[Jireh Loreaux]

We want ⟪x, a • y⟫ = a • ⟪x, y⟫ (and we have this) and we want ⟪a • x, y⟫ = ⟪x, y⟫ <• (star a).

[Jireh Loreaux]

(and we have these currently propositionally, but not defeq)

[Eric Wieser]

This is all moot without generalizing InnerProductSpace to not need IsROrC, right?

[Jireh Loreaux]

??

[Eric Wieser]

Ah nevermind, I now understand your diamond comment, sorry

[Jireh Loreaux]

When we have a CStarModule Aᵐᵒᵖ E instance, then for x y : E and a : A, we'll get ⟪x, y <• a⟫ = ⟪x, y⟫ <• a, which is what we normally do in C⋆-module theory (i.e., we default to right actions instead of left actions).

[Jireh Loreaux]

Eric Wieser said:

Is it relevant that I was intending to eventually make InnerProductSpace K V (or rather, its parent NormedSpace K V) imply both a left- and right-action by K?

I confused myself about this earlier. I think there is no issue here because the right-module action of a C⋆-algebra on itself gives us a CStarModule Aᵐᵒᵖ A instance which leads to an Inner Aᵐᵒᵖ A instance. So this doesn't conflict with anything in the case of A := ℂ because it's an Inner instance over ℂᵐᵒᵖ not over ℂ.

[Eric Wieser]

Do you have any interest in one-sided CStarModules, or should they also imply compatible left and right actions?

[Jireh Loreaux]

No, they will only be one-sided in general.

[Jireh Loreaux]

But I'll need to, for example, consider C⋆-bimodules, where I have CStarModule A E and CStarModule Bᵐᵒᵖ E along with some compatibility conditions, hence I really do need left and right actions.

[Anatole Dedecker]

A bit late to the discussion, but I agree with Jireh on everything here. It's just a bit sad that ⟪x, a • y⟫ = a • ⟪x, y⟫ looks less good than in the right module setting, but that's just a fact of life.

[Anatole Dedecker]

Eric Wieser said:

Is it relevant that I was intending to eventually make InnerProductSpace K V (or rather, its parent NormedSpace K V) imply both a left- and right-action by K?

I think we should be removing requirements from NormedSpace (e.g allowing more base rings), not adding some. And indeed if we ever want to unify CStarModule and InnerProductSpace (which is not the most urgent thing, but could be nice) that could be annoying I think.

[Eric Wieser]

Anatole Dedecker said:

I think we should be removing requirements from NormedSpace (e.g allowing more base rings), not adding some.

We already have the fully-removed version, it's docs#BoundedSMul

[Eric Wieser]

I went through a spree last year of replacing lots of NormedSpaces in theorems in mathlib with that typeclass, generalizing the ring appropriately

[Anatole Dedecker]

Eric Wieser said:

Anatole Dedecker said:

I think we should be removing requirements from NormedSpace (e.g allowing more base rings), not adding some.

We already have the fully-removed version, it's docs#BoundedSMul

Ah yes, I always forget about this one, sorry. I don't remember, is there a reason not to replace NormedSpace? But I guess this is another subject.

[Jireh Loreaux]

I suspect we never want to unify InnerProductSpace and CStarModule

[Anatole Dedecker]

Is there an obvious reason I'm missing?

[Jireh Loreaux]

several:

1. import hierarchy
2. Can't include \R
3. Many theorems don't generalize so there isn't tons of duplication. And even the ones that do require high-powered results.

[Jireh Loreaux]

Even putting an instance on the product requires nontrivial CFC machinery.

[Anatole Dedecker]

I wasn't advocating for any nontrivial generalization, so I don't think the first two point are that bad (again, just for the definitions). I was mostly thinking of factorizing e.g Cauchy-Schwartz identity, but I was missing the sneaky docs#CStarAlgebra.conjugate_le_norm_smul in the proof.

[Jireh Loreaux]

Yeah, and note also that (at least for now), we don't allow pre-C⋆-modules, but we do allow for pre-inner product spaces.

But what I meant with ℝ is that the ℂ-module structure is baked in as a parameter to docs#CStarModule, so it's impossible to have CStarModule ℝ ℝ. This may need to change at some point, but currently we do this because it would be a royal pain otherwise, as Lean will never be able to figure out whether it should choose ℝ or ℂ. (Indeed, while ⟪x, y⟫_A makes reference to A, there is no mention of the actual scalar ring anywhere.)

[Jireh Loreaux]

Ugh... this is a super annoying change. If anyone wants to lend a hand, it's on branch#j-loreaux/InnerProductSpace-swap-mul.

[Jireh Loreaux]

I think the thing that is perhaps worst about it is that over ℝ it's really surprising (i.e., that ⟪x, y⟫_ℝ := y * x definitionally for x y : ℝ). This comes up in the Fourier Transform stuff a bunch. I guess I'm not sure whether to change some of the definitions (so that they are innerSL.flip, which preserves the order of multiplication, or to fix the proofs).

Likewise, when constructing an inner product on n → 𝕜 from a positive definite matrix M, the definition was ⟪x, y⟫ := dotProduct (star x) (M *ᵥ y), which is pretty natural, but I switched it to dotProduct (M *ᵥ y) (star x) so that when you take the inner product corresponding to the identity you will get the same inner product definitionally as the one on EuclideanSpace 𝕜 n.

[Oliver Nash]

I confess I haven't read this thread carefully but are you saying that we will lose the fact that the following proof is true by definition if we make this change?

import Mathlib

open scoped RealInnerProductSpace

example (x y : ℝ) : ⟪x, y⟫ = x * y := rfl

[Jireh Loreaux]

Yes, it will be ⟪x, y⟫ = y * x := rfl.

[Jireh Loreaux]

I finally got around to finishing this: #22715. Please feel free to comment.

@David Loeffler and @Yaël Dillies in particular I would like your comments on changes in this PR to areas relevant to you.

[David Loeffler]

I think Jireh has done an excellent job of making the change in a way that's minimally invasive for the existing code – the vast majority the changes in Fourier theory, etc, seem to be just changing inner_apply to inner_apply'. So, if it makes life easier for C* algebra stuff, then I certainly have no objection.

[Kim Morrison]

There's a merge conflict now. Otherwise, sounds great!

[Jireh Loreaux]

conflict resolved.

[George Granberry]

Probably not related to the issue I'm having but you're probably familiar with this bit of code. I've been trying to use

rw [inner]

to use the lemma

∀ (w z : ℂ), inner w z = ((starRingEnd ℂ) w * z).re

but for whatever reason i'm always getting

Inner.inner.{u_4, u_5} {𝕜 : Type u_4} {E : Type u_5} [self : Inner 𝕜 E] : E → E → 𝕜

[Aaron Liu]

George Granberry said:

Probably not related to the issue I'm having but you're probably familiar with this bit of code. I've been trying to use

rw [inner]

to use the lemma

∀ (w z : ℂ), inner w z = ((starRingEnd ℂ) w * z).re

but for whatever reason i'm always getting

Inner.inner.{u_4, u_5} {𝕜 : Type u_4} {E : Type u_5} [self : Inner 𝕜 E] : E → E → 𝕜

That lemma is called docs#Complex.inner.

[George Granberry]

Ahhh, thanks so much @Aaron Liu !