dualRestrict_ker_eq_dualAnnihilator

English

For W ⊆ M and f: N →_R M, the image of W.dualAnnihilator under f.dualMap is contained in (W.comap f).dualAnnihilator.

Русский

Для W ⊆ M и отображения f: N →_R M образ W.dualAnnihilator под действием f.dualMap содержится в (W.comap f).dualAnnihilator.

LaTeX

$$W.dualAnnihilator.map f.dualMap ≤ (W.comap f).dualAnnihilator.$$

Lean4

/-- That $\operatorname{ker}(\iota^* : V^* \to W^*) = \operatorname{ann}(W)$.
This is the definition of the dual annihilator of the submodule $W$. -/
theorem dualRestrict_ker_eq_dualAnnihilator (W : Submodule R M) : LinearMap.ker W.dualRestrict = W.dualAnnihilator :=
  rfl

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