English
For W, φ ∈ (M/W)^*, and x ∈ M, the equivalence sends φ to an element whose action on x is φ(x).
Русский
Для W, φ ∈ (M/W)^*, и x ∈ M, отображение эквивалентности отправляет φ на элемент, действующий на x как φ(x).
LaTeX
$$$dualQuotEquivDualAnnihilator(W)(\varphi) (x) = \varphi(x)$$$
Lean4
/-- Equivalence $(M/W)^* \cong \operatorname{ann}(W)$. That is, there is a one-to-one
correspondence between the dual of `M ⧸ W` and those elements of the dual of `M` that
vanish on `W`.
The inverse of this is `Submodule.dualCopairing`. -/
def dualQuotEquivDualAnnihilator (W : Submodule R M) : Module.Dual R (M ⧸ W) ≃ₗ[R] W.dualAnnihilator :=
LinearEquiv.ofLinear
(W.mkQ.dualMap.codRestrict W.dualAnnihilator fun φ =>
W.range_dualMap_mkQ_eq ▸ LinearMap.mem_range_self W.mkQ.dualMap φ)
W.dualCopairing (by ext; rfl) (by ext; rfl)
