[Merged by Bors] - refactor(linear_algebra/sesquilinear_form): Use similar definition as used in bilinear_map

[mcdoll]

Define sesquilinear forms as M →ₗ[R] M →ₛₗ[I] R.

---

[mcdoll]

While the definition is for general noncommutative rings, it is basically useless due to https://leanprover-community.github.io/mathlib_docs/algebra/star/module.html#todo

The easiest way would be to restrict the definition to commutative (semi)rings for now and generalize it later.

[hrmacbeth]

@mcdoll Sorry I didn't see this when you first submitted it (feel free to ping me on future PRs). I wonder, what do you think of redoing both bilinear_form and sesquilinear_form together? Then you won't need to define is_ortho (etc) separately for sesquilinear and bilinear forms -- you can give a uniform treatment at the level of semibilinear forms.

Also, when sesquilinear_form was written, we didn't yet have star_ring; it'd be great if your refactor could also do the work of switch over to that structure (rather than the current form with a separate R and involution I).

[mcdoll]

You are totally right about using star_ring.

In the end, we should not need both bilinear_form and sesquilinear_form, but there are quite a lot of files depending on bilinear_form, so I went with refactoring sesquilinear_form first.
I thought it might be best to split the whole thing into several PRs: first rewrite sesquilinear_form, then copy all the features from bilinear_form to sesquilinear_form and finally refactoring the structures that are depend on bilinear_form. If we do everything in on go, we might have to deal with merge conflicts, the PR would be extremely long and we have to be very careful that we don't forget features.

About the old version of sesquilinear_form: should I move it into deprecated/ or just delete it?

[mcdoll]

@hrmacbeth (do you get notified automatically by new comments once you replied in a PR?) there might be a reason not to combine it with star_ring, if we define sesquilinear forms as B : M →ₗ[R] M →ₗ⋆[R] R, then we have the issue that bilinear forms are no longer (by definition) a special case of sesquilinear forms, of course there is the theorem that shows that every commutative ring admits a trivial star, but if I understand it correctly Lean cannot use that to deduce that B : M →ₗ[R] M →ₗ[R] R is a of the form above.

[hrmacbeth]

Yes, I do get notified automatically! To your points:

• your point about star_ring is a good one. I think we can get around that by writing something like local attribute [instance] star_ring_of_comm in files when we are working with bilinear forms. But I don't know how unwieldy this would be. My own thought would be, let's try it out!

Regarding the plan for the refactor: Are you planning to do
(A) a switch from separate linear and sesquilinear to semilinear, with linear and sesquilinear as special cases, or
(B) a switch from the current definition with an ad-hoc structure to using M →ₗ[R] M →ₗ[I] R (or appropriate semilinear variants)
or both of these? And if both, which one would you like to accomplish first? (I'd suggest doing them separately.)

If (B) I will think a little more about what the plan should be, but if (A) is your priority, I can make a proposal from my own experience (see #9539 for example). Here is a sequence of PRs which each do "only one change at once":

1. Introduce a notation for the old-fashioned bilin_form R M, perhaps something like M ˣ²→ₗ R (we can brainstorm) and switch to this throughout the library.
2. Change the definition def bilin_form (R : Type*) (M : Type*) ... := to a semilinear version, def bilin_form {R S T : Type*} ... (σ : R →* S) (τ : R →* T) (M : Type*) ... :=, but keep the notation referring to the old (linear, not semilinear) version. This means that all lemmas, definitions, etc in the rest of the library are still about the old version, so very little breaks.
3. At your leisure, in future PRs, go through and generalize the lemmas you're especially interested in to semilinear versions.

Regarding deprecating vs deleting: delete. It's saved in the GitHub version history so can always be brought back.

[mcdoll]

I wanted to do (A) and (B) together. For sesquilinear_form I did that already and for bilinear_form it is more work, but I think it is the same work as changing from the structure to B : M →ₗ[R] M →ₗ[R] R. I would assume that generalizing most of the things from bilinear_form to semibilinear forms is only a matter of changing the definition and putting in the ring homomorphism in the correct places. In any case if there is something that is not straightforward to generalize it is also possible to leave that for later.

[ocfnash]

Hi @mcdoll thanks for this proposal and sorry the review process has dragged on for so long.

I am in favour of your approach but I am concerned about introducing a divergence between the definitions of bilin_form and sesq_form. I appreciate your ultimate goal is to unify them but I'm a bit concerned about the possibility that it might turn out to be more work / take more time than expected to change bilin_form.

I note that you have already sketched out a plan of action, namely:

• first rewrite sesquilinear_form,
• then copy all the features from bilinear_form to sesquilinear_form and,
• finally refactoring the structures that are depend on bilinear_form

This looks like quite a lot of work but if you have the appetite I believe it would work. Are you still interesting in doing all this?

[mcdoll]

I agree that it will be quite a bit of work, but I think that it is better if we do this sooner than later otherwise it will get even worse. I would like to do that, but I will most likely need some help when it comes to matrix and later the inner_product stuff.

[ocfnash]

@mcdoll OK great, thanks for taking this on. Let's go for it!

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests