quotDualCoannihilatorToDual — Mathlib

English

For W ⊆ M, the map quotDualCoannihilatorToDual sends a coset to evaluation on W, giving a functional on W.

Русский

Для W ⊆ M отображение quotDualCoannihilatorToDual отправляет косет на функционал на W, то есть вычисление на W.

LaTeX

$$$W.quotDualCoannihilatorToDual (\overline{m}) w = w(m)$$$

Lean4

/-- The pairing between a submodule `W` of a dual module `Dual R M` and the quotient of
`M` by the coannihilator of `W`, which is always nondegenerate. -/
def quotDualCoannihilatorToDual (W : Submodule R (Dual R M)) : M ⧸ W.dualCoannihilator →ₗ[R] Dual R W :=
  liftQ _ (flip <| Submodule.subtype _) le_rfl

Похожие утверждения