range_dualMap_dual_eq_span_singleton

English

For f ∈ Dual R M1, range(f.dualMap) equals the span of f, i.e., range(f^*) = R · f.

Русский

Для f ∈ Dual R M1 образ(f.dualMap) равен линейной оболочке f, то есть range(f^*) = R · f.

LaTeX

$$$$ \\operatorname{range}(f^{\\ast}) = R \\cdot f. $$$$

Lean4

@[simp]
theorem range_dualMap_dual_eq_span_singleton (f : Dual R M₁) : range f.dualMap = R ∙ f :=
  by
  ext m
  rw [Submodule.mem_span_singleton]
  refine ⟨fun ⟨r, hr⟩ ↦ ⟨r 1, ?_⟩, fun ⟨r, hr⟩ ↦ ⟨r • LinearMap.id, ?_⟩⟩
  · ext; simp [dualMap_apply', ← hr]
  · ext; simp [dualMap_apply', ← hr]

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