[Merged by Bors] - feat: define reflexive modules and prove basics of perfect pairings

[ocfnash]

---

[j-loreaux]

@ocfnash It would be really cool if we could generalize the statement of IsReflexive so that it is also applicable to Banach spaces (or LCTVSs more generally), but (a) I don't immediately see how to do that, and (b) it's not absolutely necessary, especially not for this PR. However, I'm mentioning it in case you see an immediately obvious idea.

Maybe something like this, but it's not fully fleshed out:

class IsSemireflexive {R M : Type _} [Semiring R] [AddCommMonoid M] [Module R M]
    {D : Type _ → Type _ → Type _} [AddCommMonoid (D R (D R M))] [Module R (D R (D R M))]
    (dual_eval : M →ₗ[R] D R (D R M)) : Prop where
  bijective_dual_eval' := Function.Bijective dual_eval

Note that, in functional analysis, the condition you provided for IsReflexive is called "semi-reflexive" (i.e., bijectivity of the double dual map, using the strong dual), and "reflexive" is used to mean this map is an isomorphism (for Banach spaces, these conditions are equivalent). Maybe this warrants a rename, but perhaps not if it's going to be focused solely on the algebraic dual.

[ocfnash]

@j-loreaux Thanks for the remarks, I like the idea but I don't see an easy way to implement it (I had actually thought a bit about this while making this PR).

For me the issue is that I don't see an easy way to abstract over the type of dual we're talking about.

For example, the type D : Type _ → Type _ → Type _ in your sketch won't work because D would also need to take various typeclass parameters. For example, the type of Module.Dual is:

(R : Type u_1) → (M : Type u_2) → [CommSemiring R] → [AddCommMonoid M] → [Module R M] → Type (max u_2 u_1)

I expect we could unify things using our category theory library but I don't think it would be worth it.

I think it is better just to have separate theories for this purely algebraic concept (which is called reflexive) and the analytic versions (with lemmas connecting them in, say, finite dimensions). This is also what we do elsewhere, e.g., we have purely algebraic tensor products.

[eric-wieser]

bors d+

I gave up on ULift because I think we're missing some machinery, and it's not interesting enough to bother with here.

[bors]

✌️ ocfnash can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ocfnash]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style