Next steps for BilinForm

Stream: mathlib4

[Christopher Hoskin]

I've been working on https://github.com/leanprover-community/mathlib4/issues/10553

With the following PRs merged

• https://github.com/leanprover-community/mathlib4/pull/11032
• https://github.com/leanprover-community/mathlib4/pull/11057
• https://github.com/leanprover-community/mathlib4/pull/11078

I think we'd be quite close to being able to deprecate / remove the BilinForm structure.

Regarding #11032, @Eric Wieser asks: https://github.com/leanprover-community/mathlib4/pull/11032#issuecomment-1970146663

Does anything use the old BilinForm files in this PR after this change? I'd be tempted to update them in place to be about LinearMap.BilinForm, so as to keep the history of the file, like we did with the TensorProduct file.

I think this could work for LinearAlgebra/BilinearForm/DualLattice. I'm less sure what to do about LinearAlgebra/BilinearForm/Properties because several of the concepts in that file not touched by #11032 (e.g. IsRefl, IsAlt, IsSymm) already have equivalents in LinearAlgebra/SesquilinearForm. (Not quite the same as commutativity of the semi-ring is required there, also some results are missing e.g. IsAlt.add, IsAlt.smul, IsAlt.neg and IsAlt.sub.)

Any opinions on how we should proceed?

Thanks.

Christopher

[Christopher Hoskin]

This is what I've come up with.

[Eric Wieser]

One split that looks tempting; I think we should change docs#BilinForm to require CommSemiring R first, as that will collect together all the typeclass changes from that PR

[Eric Wieser]

(ah, which we have already as branch#bilinear-form-commutative)

[Christopher Hoskin]

@Eric Wieser I've opened https://github.com/leanprover-community/mathlib4/pull/11280

[Moritz Doll]

@Eric Wieser @Christopher Hoskin , what are your thoughts on marking everything in the BilinForm folder as deprecated with links to new version. I think we are at a point now where we really don't want to have any new usage of BilinForm and also want to see that all theorems have a counterpart in the new structure.

[Christopher Hoskin]

Moritz Doll said:

want to see that all theorems have a counterpart in the new structure.

If https://github.com/leanprover-community/mathlib4/pull/11280 gets approved/merged, then I was thinking that the next step would be to open PRs like https://github.com/leanprover-community/mathlib4/pull/9485 and then see what was left.

@Moritz Doll What is your view of the approach in https://github.com/leanprover-community/mathlib4/pull/11280 ?

[Moritz Doll]

I think it is good, I didn't have the time to have a proper look at it, but this is definitively the thing to do

[Frédéric Marbach]

Hi. For a project described here (prove that all derivations of a finite dimensional semisimple Lie algebra are inner), I need the lemma restrict_nondegenerate_of_isCompl_orthogonal, which, up to my understanding, was only stated using the old definition of bilinear forms. I pushed #12015 to transfer this statement to the new definition of bilinear forms. I had to put it in a separate file to avoid a dependency cycle. Could any of you take a look or share thoughts about this? Thanks

[Christopher Hoskin]

@Frédéric Marbach In the short term, I think the next step is to merge https://github.com/leanprover-community/mathlib4/pull/11278 which will keep all of the existing _root_. BilinForm results but built on top of LinearMap.BilinForm. There'll then be some clean up and consolidation to do.

[Frédéric Marbach]

Oh, indeed it looks great and we wouldn't need my modifications. Do you know why #11278 is not merged yet? Is there anything in the way?

[Kevin Buzzard]

Probably just because it changes a lot of files, and is several hundred lines long.

[Christopher Hoskin]

Possibly @Eric Wieser has been taking a well deserved Easter break - or has been otherwise occupied.

[Kevin Buzzard]

Given the 200+ page PhD thesis that landed in my inbox recently, I know he's been very occupied :-)

[Oliver Nash]

Rumour has it, he also has a day job.

[Frédéric Marbach]

Thanks for preparing this PR and merging!

It seems that there are two definitions of the restriction of a bilinear form to a subspace:

• Submodule.restrictBilinear
• BilinForm.restrict

I am running into an issue because two lemmas I need use respectively each of these.

I can prepare a commit to delete one of these definitions and align everything on the remaining one. Which one do you want to keep? Both are used in a small number of places (~5 references each). I would probably lean towards keeping BilinForm.restrict because writing B.restrict W feels more natural to me than W.restrict B, but I don't have much experience!

[Eric Wieser]

It looks like the docs have not yet rebuilt with the latest change

[Frédéric Marbach]

Well, I linked the docs but both are still in the source code too on the master branch.

[Eric Wieser]

Well, thanks for making me notice; the docs builds stop every 60 days, and the last such stop was three days ago! I've set them going again for the next two months :)

[Eric Wieser]

And actually, we have three of these definitions, not two!

[Eric Wieser]

docs#LinearMap.domRestrict₁₂ is the other one

[Frédéric Marbach]

Yes. But this last one is for general bi-semi-linear maps M → N → P, while the previous two were really specific to bilinear forms M → M → R.

I am ready to implement whatever option you think is best concerning these 2/3 definitions.

In the same way that BilinForm is defined as an abbreviation, could we keep one abbreviation for the restriction of a bilinear form to a subspace? B.restrict W feels better to me than B.domRestrict₁₂ W W.

[Eric Wieser]

Submodule.restrictBilinear should definitely go, we can think about the other two later

[Eric Wieser]

Changing the BilinForm one to an abbrev sounds good to me

[Frédéric Marbach]

It is here: #12045. I ran into some unexpected weird problems with flip (for which I have no explanation). I think I found an OK solution after a lot of fiddling. The try-and-test was quite painful because of long compile times (probably messing with files quite low in the hierarchy).

[Christopher Hoskin]

I've opened a PR to deprecate a some of the definitions and results which are essentially just the identity following the migration: https://github.com/leanprover-community/mathlib4/pull/12078

[Christopher Hoskin]

More deprecations: https://github.com/leanprover-community/mathlib4/pull/12112

What is the rule / convention for how long a result remains in Mathlib before being removed after deprecation?

[Frédéric Marbach]

I would indeed very much like to read a page about how the mathlib community approaches versioning/deprecation with respect to third parties.

Christopher Hoskin said:

What is the rule / convention for how long a result remains in Mathlib before being removed after deprecation?

[Eric Wieser]

I don't think we really have a policy yet

[Yaël Dillies]

I have been removing deprecated lemmas that were on my way for other things. Those were deprecated since they were ported over a year ago.

[Michael Rothgang]

Eric Wieser said:

I don't think we really have a policy yet

@Frédéric Marbach think this would be a good conversation to start. My wild guess/impression is that one year is presumably uncontroversial, and something between three and six months could be a likely outcome.

[Kim Morrison]

I'd prefer we land in the 3-6 months range. It would be helpful if there's a consistent method for including a date in the deprecated attribute.

[Damiano Testa]

Btw, #10864 is a wrapper around @[deprecate] alias that makes the date part of the syntax. If you think that it may be useful, feel free to suggest modifications!

[Christopher Hoskin]

I'm inclined to close without merging this PR unless anyone thinks it's still useful?

[Michael Rothgang]

Damiano Testa said:

Btw, #10864 is a wrapper around @[deprecate] alias that makes the date part of the syntax. If you think that it may be useful, feel free to suggest modifications!

Since @deprecate in Lean 4.8 allows including a date (in the since field), I think it's easier to just standardise on that.