Unifying duality for submodules and cones

Stream: mathlib4

[Martin Winter]

There is an implementation of dual for PointedCone based on a pairing p like this

def PointedCone.dual (s : Set M) : PointedCone R N where
  carrier := {y | ∀ ⦃x⦄, x ∈ s → 0 ≤ p x y}
  ...

I implemented an analogous duality for submodules like this

def Submodule.dual : Submodule R N where
  carrier := {y | ∀ ⦃x⦄, x ∈ s → 0 = p x y}
  ...

I then needed to reprove most lemmas from cone duality (about 20, but numbers rising). Both definitions could be unified as follows

variable {S R M N : Type*}
  [CommSemiring S]
  [CommSemiring R] [Algebra S R]
  [AddCommMonoid M] [Module R M]
  [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower S R N]
  (C : Submodule S R) (p : M →ₗ[R] N →ₗ[R] R)

def Dual.dual (s : Set M) : Submodule S N where
  carrier := {y | ∀ ⦃x⦄, x ∈ s → p x y ∈ C}
  ...

and I checked that all basic lemmas can still be proven in this context.
The previous definitions one obtains as follows

abbrev Submodule.dual := Dual.dual (⊥ : Submodule R R) p
abbrev PointedCone.dual := Dual.dual (PointedCone.positive R R) p

I am not certain how one would structure this in mathlib to make this maximally easy to use and extend. Ideally one has the following features:

• The general Dual.dual is not used directly when working within the submodule or cone context. Ideally it is hidden in some namespace (as I have done here), or uses some other name like dual'.
• The general duality lemmas are implemented using theDual.dual. They are not hidden but are intended to be used directly from the specialized contexts.
• For Submodule and PointedCone only the abbrevs shown above need to be implemented, but all the lemmas need not to be reproven. The general duality lemmas should be usable without friction.
• The statements of the general duality lemmas are still easily readable and are not obfuscated by the name or namespace we end up using for the general Dual.dual.

What's the best way to achieve all of this?

[Martin Winter]

For example, I ran into the following problem:

Suppose that the goal contains Submodule.dual p (span R s). Then rw [dual_span] should be able to rewrite this part of the goal. And it does so if I use an implementation of dual_span written in terms of Submodule.dual. But if I define

abbrev Submodule.dual := Dual.dual (⊥ : Submodule R R) p

and use a dual_span written in terms of Dual.dual, then rw [dual_span] cannot find the expression in the goal, even though Submodule.dual is an abbrev of Dual.dual.

Is there anything one can do about it? Or does this indicate that unifying the two duality concepts wont work?

[Artie Khovanov]

I personally avoid abbrev in Mathlib. It is not transparent enough for most purposes. For instance, Ideal R is an abbrev for Submodule R R, but most of the Submodule API is duplicated for Ideal anyway.

Also, do you want PointedCone.dual to have type PointedCone, or Submodule?

[Martin Winter]

Also, do you want PointedCone.dual to have type PointedCone, or Submodule?

PointedCone, which is defined as a Submodule over the non-negative scalars. And the definition of Dual.dual that I propose would produce this sort of submodule. I was hoping this is enough to make the automation work. You seem skeptical?

[Martin Winter]

For instance, Ideal R is an abbrev for Submodule R R, but most of the Submodule API is duplicated for Ideal anyway.

Do you say it is duplicated because abbrev is not transparent enough to make the autmation work. Or is it a naming reason, e.g. people don't want to call Submodule.something when they work with ideals?

[Artie Khovanov]

The usual pattern for avoiding duplication is to use a typeclass. Something like

class DualMapClass (dual : Set M → Submodule R N) where
  kernel : Submodule S R
  mem_iff (s : Set M) (x : N) : x \in s \iff ...

Or you can make kernel a parameter if you like, to avoid defeq issues.

Then write your lemmas for maps dual satisfying this class, and then register your concrete duals as instances.

[Artie Khovanov]

In this case it feels overkill but maybe it's the right choice!

[Martin Winter]

Interesting. I will consider this.

[Artie Khovanov]

Martin Winter said:

Do you say it is duplicated because abbrev is not transparent enough to make the autmation work. Or is it a naming reason, e.g. people don't want to call Submodule.something when they work with ideals?

Former. It's not just about syntactic equality either - I've found the transparency quite brittle.

[Artie Khovanov]

Martin Winter said:

PointedCone, which is defined as a Submodule over the non-negative scalars.

Oh yeah I forgot about the definition. But yeah it's the abbrev issue again - not syntactically equal.

[Martin Winter]

In this case it feels overkill but maybe it's the right choice!

Maybe. But I wonder: what is mathlib's stance on duplication of code like this? Don't worry too much unless you write it like 5 times?

[Artie Khovanov]

Martin Winter said:

what is mathlib's stance on duplication of code like this?

I'm not a maintainer or anything like that but I'd note that the basic API for substructures - hundreds of lines of code - is duplicated maybe 10-20 times across Mathlib. (This is obviously bad and I have a proposal to fix it but big refactors take time and effort.)

Your level of duplication is both common and tiny compared to the amount of existing tech debt. See also @Yaël Dillies's comments on my positive cone proposal.

[Martin Winter]

Good to know. Thanks!

[Yaël Dillies]

Yes, I find it intellectually satisfying that duality holds in this more general setting, but I doubt the small benefit of saving a few (10s of?) lines is worth the syntactic trouble

[Martin Winter]

It's certainly more than "10s of lines" but I think you are right.