English
For W ⊆ M and φ ∈ Module.Dual R M, and x ∈ W, the pairing W.dualPairing (Quotient.mk φ) x equals φ(x).
Русский
Для W ⊆ M и φ ∈ Module.Dual R M, и x ∈ W, паринг W.dualPairing (Quotient.mk φ) x = φ(x).
LaTeX
$$$W.dualPairing (\overline{\varphi}) x = \varphi(x)$$$
Lean4
/-- Given a submodule, restrict to the pairing on `W` by
simultaneously corestricting to `Module.Dual R M ⧸ W.dualAnnihilator`.
This is `Submodule.dualRestrict` factored through the quotient by its kernel (which
is `W.dualAnnihilator` by definition).
See `Subspace.dualPairing_nondegenerate`. -/
def dualPairing (W : Submodule R M) : Module.Dual R M ⧸ W.dualAnnihilator →ₗ[R] W →ₗ[R] R :=
W.dualAnnihilator.liftQ W.dualRestrict le_rfl
