More typeclass instances for bilinear forms

Stream: mathlib4

[Martin Winter]

For the duality theory of convex cones we will need to carry around some properties of bilinear forms as typeclasses, similar to IsPerfPair. This includes SeparatingLeft, SeparatingRightand Nondegenerate.

I prepared a first draft PR, see #34487.

There are two topics that I would like to discuss before I proceed.

[Martin Winter]

I. Fact

LinealMap.IsPerfPair is a typeclass. The above mentioned properties are not. Hence I need to write [Fact B.SeparatingLeft] all over the place (and yes, this will be a common thing to write). Is this okay? Or should one implement typeclasses? I was given this warning when I first learned of Fact (@Kenny Lau ).

[Martin Winter]

II. Placement

Where to put this code? In the PR draft I put it in LinearAlgebra/SesquilinearForm/Basic. But the code requires Module.Projective (which I added as an import) and also lemmas from LinearAlgebra.Dual.Lemmas (which I cannot import due to an import cycle). This suggests the code should go into LinearAlgebra.Dual.Lemmas. But the code has, on its surface, nothing to do with duality. Consider this lemma:

theorem SeparatingRight.id [Module.Projective R M] : .id.SeparatingRight

I imagine it would be bad for discoverability to put it into duality files?

Note that we develop a topology-free duality theory. Hence we cannot use SeparatingDual etc.