Pairings between cyclic spans

A bilinear pairing whose value on two generators is a unit identifies the span of the first generator with the dual of the span of the second. The ambient modules may be different, and the coefficient ring need only be a commutative semiring.

theorem LinearMap.compl₁₂_span_singleton_bijective_of_isUnit {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (B : M →ₗ[R] N →ₗ[R] R) (x : M) (y : N) (hxy : IsUnit ((B x) y)) : Function.Bijective ⇑(B.compl₁₂ (R ∙ x).subtype (R ∙ y).subtype)

A unit generator pairing makes the pairing between the two cyclic spans bijective onto the dual of the right span.