Unifying `Submodule.dual` and `Submodule.orthogonalBilin`

Stream: mathlib4

[Martin Winter]

In #34007 I propose an implementation of Submodule.dual as an analogue of the existing PointedCone.dual. This PR is a bottleneck for the upcoming cone duality theory and needed for polyhedral cones. @Joël Riou pointed out the similarity to Submodule.orthogonalBilin and asked whether these concepts can be unified. I am open for it, but feel not competent in judging how this should be done in detail.

Both "dual" and "orthogonalBilin" are based on a bi(semi)linear pairing B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M but with complementary generality:

• "orthogonalBilin" assumes that M₁ and M₂ are identical.
• "dual" currently assumes an R-bilinear pairing, and M is the base ring R.

Also "dual" takes in a set, whereas "orthogonalBilin" takes in a submodule.

[Martin Winter]

Questions:

1. First and foremost, is it the right move to unify these concept? They are related, but express slightly different intent. Note that there are also dualAnnihilator and dualCoannihilator that are further special cases (see dual_dualCoannihilator in #34007). Should they exist independently?
2. How to unify? I suppose the unification should be build on the maximally general B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M. Do we want "orthogonalBilin" to take in a set as opposed to a submodule?
3. Which terminology should survive? I feel like "orthogonal" is a relation between submodules in the same space. So, should "dual" be the primary terminology? Should "orthogonalBilin" be an optional terminology for when M₁ = M₂?
4. Given that Submodule.dual is a bottleneck for polyhedral cones and that the unifaction seems nontrivial, should it be a priority now?

[Yaël Dillies]

I assume you meant @Joël Riou

[Joël Riou]

I would argue that "dual" is a very confusing terminology, and orthogonal is much better. The word "orthogonal" seems quite standard (in the French speaking undergraduate literature) at least in the case of the pairing between a finite dimensional vector space and its dual. (There are actually two notions of left or right orthogonal, but it may be ok to use only one because the other can be deduced by using the flip.)

[Antoine Chambert-Loir]

Submodule.dual is confusing in three ways: 1) there is docs#Module.Dual for the actual dual of a module ; 2) that notion depends on the choice of a pairing ; 3) in the classical case, it would represent the dual of the quotient module.

[Violeta Hernández]

(deleted)

[Violeta Hernández]

Which terminology should survive? I feel like "orthogonal" is a relation between submodules in the same space. So, should "dual" be the primary terminology?

I agree with this, I've never seen the word "orthogonal" used outside of this context. We already use the word for docs#Module.Dual, and I think we should use the same word here.

[Violeta Hernández]

...oh wait, this takes a bilinear map rather than being the true dual. So yeah, I think we should find another name.

[Violeta Hernández]

This is for convex polytopes, right? Is there a reason we can't just take a dual polytope to live in the dual space?

[Martin Winter]

Antoine Chambert-Loir said:

Submodule.dual is confusing in three ways: 1) there is docs#Module.Dual for the actual dual of a module [...]

I consider this a feature, not a bug: using Dual.eval as a pairing, Submodule.dual would live in Module.Dual. This would be consistent terminology.

If we don't want "dual", I would still hope for a term of comparable length. Statements that contain "orthogonalBilin" more than once (of which there will be plenty) are rather cumbersome to parse. Can we have "ortho"?

[Martin Winter]

While we are at it, I have another question:

5. why do we have a separate BilinForm.orthogonal? The only difference to orthogonalBilin (besides the namespace) seems to be that it takes a bilinear form rather than a bilinear map. It even implements a lot of the same lemmas. Can't we just use orthogonalBilin in place of orthogonal everywhere (and then rename the former to the latter)?

[Martin Winter]

Violeta Hernández said:

This is for convex polytopes, right? Is there a reason we can't just take a dual polytope to live in the dual space?

For convex cones at this time, but convex polytopes eventually.

Note that defining the dual with respect to a general pairing is not a feature of my PR but is already the case for PointedCone.dual. I am merely consistent with it.
We had a discussion here where I also opposed the pairing in dual. What convinced me eventually is that the following two common use cases are covered very easily:

• ideally the dual of the dual lives in the same space as the original cone. We can get from the dual cone back using the pairing B.flip. This is especially important in infinite dimensions where a module is not isomorphic to its double dual.
• in Euclidean spaces we can choose a pairing that gives us the dual in the same space again.

[Violeta Hernández]

Justus Springer said:

It's true we don't gain any generality in a mathematical sense. After all, for any pair of vector spaces $N$ and $M$ with a perfect pairing, we have $M \cong N^*$. But we gain flexibility in Lean, as it might happen that $M$ is not definitionally equal to $N^*$. If we only allow the "canonical" dual, we would then have to carry around the isomorphism all the time, as in the example with the double dual Yael mentions.

Well, this convinces me.