map_smul'' — Mathlib

English

For an ideal I, a submodule N, and a linear map f, we have map f (I • N) = I • (map f N).

Русский

Для идеала I, подподмодуля N и линейного отображения f выполняется map f (I • N) = I • (map f N).

LaTeX

$$$\\mathrm{map}\, f\\,(I \\cdot N) = I \\cdot (\\mathrm{map}\, f\\ N)$$$

Lean4

@[simp]
theorem map_smul'' (f : M →ₗ[R] M') : (I • N).map f = I • N.map f :=
  le_antisymm
      (map_le_iff_le_comap.2 <|
        smul_le.2 fun r hr n hn =>
          show f (r • n) ∈ I • N.map f from (f.map_smul r n).symm ▸ smul_mem_smul hr (mem_map_of_mem hn)) <|
    smul_le.2 fun r hr _ hn =>
      let ⟨p, hp, hfp⟩ := mem_map.1 hn
      hfp ▸ f.map_smul r p ▸ mem_map_of_mem (smul_mem_smul hr hp)

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