mathlib3documentation

algebra.module.submodule.bilinear

Images of pairs of submodules under bilinear maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides submodule.map₂, which is later used to implement submodule.has_mul.

Main results #

• submodule.map₂_eq_span_image2: the image of two submodules under a bilinear map is the span of their set.image2.

Notes #

This file is quite similar to the n-ary section of data.set.basic and to order.filter.n_ary. Please keep them in sync.

def submodule.map₂ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] (f : M →ₗ[R] N →ₗ[R] P) (p : M) (q : N) :
P

Map a pair of submodules under a bilinear map.

This is the submodule version of set.image2.

Equations
theorem submodule.apply_mem_map₂ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] (f : M →ₗ[R] N →ₗ[R] P) {m : M} {n : N} {p : M} {q : N} (hm : m p) (hn : n q) :
(f m) n q
theorem submodule.map₂_le {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] {f : M →ₗ[R] N →ₗ[R] P} {p : M} {q : N} {r : P} :
q r (m : M), m p (n : N), n q (f m) n r
theorem submodule.map₂_span_span (R : Type u_1) {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] (f : M →ₗ[R] N →ₗ[R] P) (s : set M) (t : set N) :
s) t) = (set.image2 (λ (m : M) (n : N), (f m) n) s t)
@[simp]
theorem submodule.map₂_bot_right {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] (f : M →ₗ[R] N →ₗ[R] P) (p : M) :
@[simp]
theorem submodule.map₂_bot_left {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] (f : M →ₗ[R] N →ₗ[R] P) (q : N) :
q =
theorem submodule.map₂_le_map₂ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] {f : M →ₗ[R] N →ₗ[R] P} {p₁ p₂ : M} {q₁ q₂ : N} (hp : p₁ p₂) (hq : q₁ q₂) :
p₁ q₁ p₂ q₂
theorem submodule.map₂_le_map₂_left {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] {f : M →ₗ[R] N →ₗ[R] P} {p₁ p₂ : M} {q : N} (h : p₁ p₂) :
p₁ q p₂ q
theorem submodule.map₂_le_map₂_right {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] {f : M →ₗ[R] N →ₗ[R] P} {p : M} {q₁ q₂ : N} (h : q₁ q₂) :
q₁ q₂
theorem submodule.map₂_sup_right {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] (f : M →ₗ[R] N →ₗ[R] P) (p : M) (q₁ q₂ : N) :
(q₁ q₂) = q₁ q₂
theorem submodule.map₂_sup_left {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] (f : M →ₗ[R] N →ₗ[R] P) (p₁ p₂ : M) (q : N) :
(p₁ p₂) q = p₁ q p₂ q
theorem submodule.image2_subset_map₂ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] (f : M →ₗ[R] N →ₗ[R] P) (p : M) (q : N) :
set.image2 (λ (m : M) (n : N), (f m) n) p q p q)
theorem submodule.map₂_eq_span_image2 {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] (f : M →ₗ[R] N →ₗ[R] P) (p : M) (q : N) :
q = (set.image2 (λ (m : M) (n : N), (f m) n) p q)
theorem submodule.map₂_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] (f : M →ₗ[R] N →ₗ[R] P) (p : M) (q : N) :
p = q
theorem submodule.map₂_supr_left {ι : Sort uι} {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] (f : M →ₗ[R] N →ₗ[R] P) (s : ι M) (t : N) :
( (i : ι), s i) t = (i : ι), (s i) t
theorem submodule.map₂_supr_right {ι : Sort uι} {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] (f : M →ₗ[R] N →ₗ[R] P) (s : M) (t : ι N) :
( (i : ι), t i) = (i : ι), (t i)
theorem submodule.map₂_span_singleton_eq_map {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) :
{m}) = submodule.map (f m)
theorem submodule.map₂_span_singleton_eq_map_flip {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ M] [ N] [ P] (f : M →ₗ[R] N →ₗ[R] P) (s : M) (n : N) :
{n}) = submodule.map ((f.flip) n) s