weak version of PerfectPairing for infinite rank

Stream: Is there code for X?

[Scott Carnahan]

Do we have a name for a bilinear map that has trivial left and right kernels? E.g.,

import Mathlib.LinearAlgebra.Dual

open Function Module

variable (R M N : Type*) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]

/-- A quasi-perfect pairing of two (left) modules over a commutative ring. -/
structure QuasiPerfectPairing :=
  toLin : M →ₗ[R] N →ₗ[R] R
  injectiveLeft : Injective toLin
  injectiveRight : Injective toLin.flip

[Moritz Doll]

docs#LinearMap.Nondegenerate

[Scott Carnahan]

Thank you, that is a perfect answer to the question that I asked. Your answer made me realize that I actually want an additional saturation condition, namely that the left and right cokernels are R-torsion-free. (sorry, I don't know how to spell this: torsion R (cokernel toLin) = ⊥ maybe?). Basically, I am looking for something that specializes to a perfect pairing in the finite rank case.

[Oliver Nash]

This might be what you want:

import Mathlib.LinearAlgebra.Dual
import Mathlib.Algebra.Module.Torsion

open Function Module

variable (R M N : Type*) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]

/-- A quasi-perfect pairing of two (left) modules over a commutative ring. -/
structure QuasiPerfectPairing :=
  toLin : M →ₗ[R] N →ₗ[R] R
  injectiveLeft : Injective toLin
  injectiveRight : Injective toLin.flip

open Submodule

variable (P : QuasiPerfectPairing R M N)

#check torsion R (Dual R N ⧸ LinearMap.range P.toLin) = ⊥
#check torsion R (Dual R M ⧸ LinearMap.range P.toLin.flip) = ⊥

-- Also bear in mind:
#check Submodule.noZeroSMulDivisors_iff_torsion_eq_bot

[Scott Carnahan]

Thank you! I think this is what I want:

structure QuasiPerfectPairing :=
  toLin : M →ₗ[R] N →ₗ[R] R
  injectiveLeft : Injective toLin
  injectiveRight : Injective toLin.flip
  saturatedLeft : NoZeroSMulDivisors R (Dual R N ⧸ LinearMap.range toLin)
  saturatedRight : NoZeroSMulDivisors R (Dual R M ⧸ LinearMap.range toLin.flip)

I'll see if I can prove anything about it.