ker_dualMap_eq_dualCoannihilator_range

English

For a linear map f, the range of its dual map is contained in the dual annihilator of its kernel: range(f.dualMap) ≤ (ker f).dualAnnihilator.

Русский

Для линейного отображения f область образа его дуального отображения вложена в дуальный аннигилятор его ядра: range(f.dualMap) ≤ (ker f).dualAnnihilator.

LaTeX

$$$ \\mathrm{range} \\, f.dualMap \\le (\\ker f).dualAnnihilator $$$

Lean4

theorem ker_dualMap_eq_dualCoannihilator_range (f : M →ₗ[R] M') :
    LinearMap.ker f.dualMap = (range (Dual.eval R M' ∘ₗ f)).dualCoannihilator := by ext x;
  simp [LinearMap.ext_iff (f := dualMap f x)]

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