range_dualMap_eq_dualAnnihilator_ker_of_surjective

English

If f is surjective, the range of its dual map equals the dual annihilator of the kernel: range f.dualMap = ker f.dualAnnihilator.

Русский

Если отображение f сюръективно, образ его дуального отображения равен двойственному аннигилятору ядра: range f.dualMap = ker f.dualAnnihilator.

LaTeX

$$$\operatorname{range} f.dualMap = (\ker f).dualAnnihilator$$$

Lean4

theorem range_dualMap_eq_dualAnnihilator_ker_of_surjective (f : M →ₗ[R] M') (hf : Function.Surjective f) :
    LinearMap.range f.dualMap = (LinearMap.ker f).dualAnnihilator :=
  ((f.quotKerEquivOfSurjective hf).dualMap.range_comp _).trans (LinearMap.ker f).range_dualMap_mkQ_eq

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