Intrinsic star

Stream: mathlib4

[Monica Omar]

So a few months ago I introduced docs#LinearMap.intrinsicStar (star operation on linear maps where star f = star ∘ f ∘ star) which is scoped to IntrinsicStar, this is mathematically distinct from the adjoint star (docs#LinearMap.instStarId, which is a global instance).
Now this is fine for linear maps on non-Hilbert spaces, and for non-endomorphisms. However, say we want to talk about both stars, on a specific Hilbert space which also has a star instance, then we have a problem. My thought in this case is to use star for the intrinsic star and adjoint for the adjoint star, however, how do we know if the star will actually mean what we want it to mean, and what if we want to use results that apply to both?

A similar problem also arises with docs#LinearMap.convMul (the convolutive product on linear maps), which is scoped to ConvolutiveProduct (cc @Yaël Dillies).
What if we want to talk about both @IsStarProjection _ LinearMap.convMul LinearMap.intrinsicStar and @IsStarProjection _ Module.End.instMul LinearMap.instStarId (which we will want to)?
Another example of this conflict: In #34119, I'm adding a result that says what the linear map of the adjacency matrix of docs#SimpleGraph.completeGraph looks like, i.e., ((completeGraph n).adjMatrix R').toLin' = 1 - .id where 1 here is the convolutive one docs#LinearMap.convOne. But in the PR I had to deinstance all the global instances on the composition product ring to make sure we pick the right * and 1. But what if we want to talk about both? What if we needed to talk about both rings?

The current suggestions are:

• local/scoped instance (it is scoped now, local wouldn't solve these problems either)
• using notation/separate definition for the intrinsic star that doesn't use star, but then we wouldn't be able to use IsSelfAdjoint etc
• a type synonym, but this sounds painful for one use case

Does anyone have any thoughts on this?

(cc @Jireh Loreaux, @Oliver Nash)

[Eric Wieser]

I'm glad that docs#LinearMap.convMul didn't become a global instance, but I think it's still quite confusing that lemmas in doc-gen about this convolutional multiplication don't make it clear that a non-standard multiplication is being used

[Eric Wieser]

(In particular seeing 1 - .id and having to remember that 1 is not in this case the identity map any more seems unpleasant)

[Jireh Loreaux]

The way we've been dealing with this so far in the Star situation is that we always useintrinsicStar in the name of the declaration. I think this is less of an issue overall because people who work in this area are used to seeing a star and thinking of both senses of the operation. Admittedly, they don't overlap that much (which is what makes it tolerable on paper), but they do still overlap in certain settings.

[Monica Omar]

And we've been using convMul and convOne in the names of the declarations for the ConvolutionProduct.

The intrinsic star and the convolutive product are both leaf files now, so now is the best time to agree on a change, before things get more complicated and troublesome.

I think the type synonym is the only one that would solve all the problems (but obviously comes with the annoying hurdle of using and implementing the type synonym).
However, I think we can use a single type synonym for both the intrinsic star and the convolutive product, since they can form a star algebra together under the right circumstances.

[Yury G. Kudryashov]

Should we introduce type synonyms instead?

[Monica Omar]

I think so. But let's see what Yaël says about this, since they authored the convolutive product.

[Monica Omar]

I think the other question would be about the name of the synonym. We wouldn't want it to be long, but would also need it to be informative, which is difficult.
toIntrinsicStarConvolutiveProduct is just too long and messy
toConv might be confusing?
I don't know

[Monica Omar]

Can we deinstance global instances for specific types?
For example, say toConvRing is a type synonym. Then I want to disable docs#Module.End.instMul (and the rest) for toConvRing A →ₗ[R] toConvRing A. Is that possible?

[Yury G. Kudryashov]

My suggestion was to put a type synonym on LinearMap ..

[Yury G. Kudryashov]

Something like def ConvEnd R A := A →ₗ[R] A

[Yury G. Kudryashov]

This comes at a cost (you need to transfer the instances that should still apply, define an Equiv to the underlying type, and make sure that the API doesn't abuse defeq), but AFAIK we don't have a better way to deal with conflicting instances.

[Jireh Loreaux]

Having thought about it further, I am also inclined towards the type synonym.

[Monica Omar]

Yeah, the definitions will look messy with the conjugation, but all in all, it will be fine. And at least this way they can be global instances too.

[Eric Wieser]

Perhaps better to go straight to

structure ConvEnd R A : Type where ofEnd :: toEnd : Module.End R A

[Monica Omar]

Alright, done with this: #34945
Just need to rename all the lemmas to match the new statements (which I'll do in a follow-up PR to reduce diff, etc).
Basically copied the same implementation for docs#WithLp.

[Eric Wieser]

Good thought on also wanting the matrix version