Generalizing `Module.Dual`

Stream: mathlib4

[Monica Omar]

At the moment docs#Module.Dual uses CommSemiring, but I think it would be better if we had this for Semiring. It would be useful to have things in terms of Dual R M instead of M →ₗ[R] R.

Is there any objections to changing this to use Semiring?

[Yaël Dillies]

That change seems pretty agreeable to me

[Monica Omar]

I've opened #31289 for this :)

[Kenny Lau]

note that this is a right R-module i think?

[Kenny Lau]

the formula is Hom : A-B-Mod x A-C-Mod -> B-C-Mod

[Kenny Lau]

with M : R-Nat-Mod and R : R-R-Mod

[Robin Carlier]

Usually, in non-symmetric monoidal categories (such as modules over a non-commutative (semi)-ring <- it's only monoidal if we do bimodules) non-commutative settings you want to distinguish between left and right (weak) duals. If we generalize, the docstrings should perhaps add which direction it is the dual of (I always get confused by the directions here... this might be relevant as the natural setting for this is by thinking of everything as bimodules I believe, though we need to ignore the "projective" part in the accepted answer.)

[Monica Omar]

@Anne Baanen , to answer your question in the PR.
Here is an example of what motivated this: I wanted to add that given a nonzero element x in a vector space (by vector space I mean a module over a semiring), there exists a dual f such that f x is nonzero.
(See here: https://github.com/leanprover-community/mathlib4/pull/28100/files#r2494755205.)
Which is the linear map version of docs#SeparatingDual.exists_ne_zero.

Also, note that docs#StrongDual uses Semiring.

[Kevin Buzzard]

But it's not true that given a random nonzero module over a random semiring that there even exists a nonzero map from the module to the semiring, let alone one that does not vanish on a given nonzero element. What exactly is the statement what you want to add?

[Monica Omar]

Right, I forgot to say that it's "free". Here's the full statement:

theorem exists_dual_ne_zero (R : Type*) {M : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
    [Free R M] {x : M} (hx : x ≠ 0) : ∃ f : M →ₗ[R] R, f x ≠ 0 :=

[Kevin Buzzard]

Aah yeah, then you're fine. I am assuming that generalizing Dual to the noncommutative case will not stop us adding the R-module instance when R is commutative? Will probably be worth benchmarking afterwards to see if any chaos has been caused by this change.

[Monica Omar]

Don't see why not. Just benched it, let's see.

[Aaron Liu]

Kevin Buzzard said:

Aah yeah, then you're fine. I am assuming that generalizing Dual to the noncommutative case will not stop us adding the R-module instance when R is commutative? Will probably be worth benchmarking afterwards to see if any chaos has been caused by this change.

Worried about possible diamonds

[Monica Omar]

what kind of diamonds?

[Eric Wieser]

I don't see any diamonds risk here

[Eric Wieser]

I think the only risk is the one @Anne Baanen calls out about this representing a choice to have Dual mean "left dual" (and this being surprising), but indeed it seems we already made this choice for docs#StrongDual so may as well be consistent for now

[Kevin Buzzard]

"left dual" is only a thing when there are both left and right actions, right? I didn't understand this objection.

[Monica Omar]

Should we change all forms of M →ₗ[R] R to Dual R M?
For example, there's docs#Module.Basis.coord and docs#Module.Basis.sumCoords (and a lot more).