range_smulRight_apply_of_surjective

English

If f: M →ₗ[R] R is surjective, then for any x ∈ M₁, the range of the map f.smulRight x equals span_R{ x }.

Русский

Если f: M →ₗ[R] R сюръективно, то для любого x ∈ M₁ образ f.smulRight x равен подмодулю span_R{ x }.

LaTeX

$$$ \mathrm{range}(f \smulRight x) = \operatorname{span}_R \{ x \}$$$

Lean4

theorem range_smulRight_apply_of_surjective [Semiring R] [Module R M] [Module R M₁] {f : M →ₗ[R] R}
    (hf : Function.Surjective f) (x : M₁) : range (f.smulRight x) = Submodule.span R { x } :=
  Submodule.ext fun z ↦ by
    simp_rw [mem_range, smulRight_apply, Submodule.mem_span_singleton]
    refine ⟨fun ⟨w, hw⟩ ↦ ⟨f w, hw ▸ rfl⟩, fun ⟨w, hw⟩ ↦ ?_⟩
    obtain ⟨y, rfl⟩ := hf w
    exact ⟨y, hw⟩

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