map₂_span_singleton_eq_map_flip

English

Let R be a commutative semiring and M, N, P be modules over R. For a bilinear map f: M × N → P and a submodule S ⊆ M and a vector n ∈ N, the image of S × span{n} under f equals the image of S under the linear map m ↦ f(m, n). In symbols: f(S × span{n}) = { f(m, n) : m ∈ S }.

Русский

Пусть R — коммутативное полуребро, M, N, P — модули над R. Для билинейного отображения f: M × N → P и подмодуля S ⊆ M и вектора n ∈ N образ S × span{n} при помощи f совпадает с образом S под линейным отображением m ↦ f(m, n). Формально: f(S × span{n}) = { f(m, n) : m ∈ S }.

LaTeX

$$$F(S, \\langle n \\rangle) = F_n[S], \\quad F_n(m) = F(m,n).$$$

Lean4

theorem map₂_span_singleton_eq_map_flip (f : M →ₗ[R] N →ₗ[R] P) (s : Submodule R M) (n : N) :
    map₂ f s (span R { n }) = map (f.flip n) s := by rw [← map₂_span_singleton_eq_map, map₂_flip]

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