map — Mathlib

English

The additive submonoid of p.map f coincides with the image of the additive submonoid p.toAddSubmonoid under f.

Русский

Аддитивная подмоноида p.map f совпадает с изображением аддитивной подмножины p под действием f.

LaTeX

$$p.\\text{map} f \\;\\text{toAddSubmonoid} = p.\\text{toAddSubmonoid}.map f$$

Lean4

/-- The pushforward of a submodule `p ⊆ M` by `f : M → M₂` -/
def map (f : F) (p : Submodule R M) : Submodule R₂ M₂ :=
  { p.toAddSubmonoid.map f with
    carrier := f '' p
    smul_mem' := by
      rintro c x ⟨y, hy, rfl⟩
      obtain ⟨a, rfl⟩ := σ₁₂.surjective c
      exact ⟨_, p.smul_mem a hy, map_smulₛₗ f _ _⟩ }

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