range_dualMap_eq_dualAnnihilator_ker

English

For a linear map f: V1 → V2 between finite-dimensional vector spaces over K, the range of the dual map f.dualMap is precisely the dual annihilator of ker f; i.e., range(f.dualMap) = (ker f)⊥.

Русский

Для линейного отображения f: V1 → V2 между конечномерными пространстваами над K образ дуального отображения f.dualMap совпадает с дуальным аннигилятором ядра: range(f.dualMap) = (ker f)⊥.

LaTeX

$$$\\operatorname{range}(f^{\\ast}) = (\\ker f)^{\\perp}$$$

Lean4

theorem range_dualMap_eq_dualAnnihilator_ker (f : V₁ →ₗ[K] V₂) :
    LinearMap.range f.dualMap = (LinearMap.ker f).dualAnnihilator :=
  range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective f <|
    dualMap_surjective_of_injective (range f).injective_subtype

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