mathlib documentation

algebra.module.submodule.bilinear

Images of pairs of submodules under bilinear maps #

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

Main results #

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} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M →ₗ[R] N →ₗ[R] P) (p : submodule R M) (q : submodule R N) :

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} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M →ₗ[R] N →ₗ[R] P) {m : M} {n : N} {p : submodule R M} {q : submodule R N} (hm : m p) (hn : n q) :
theorem submodule.map₂_le {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] {f : M →ₗ[R] N →ₗ[R] P} {p : submodule R M} {q : submodule R N} {r : submodule R P} :
submodule.map₂ f 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} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M →ₗ[R] N →ₗ[R] P) (s : set M) (t : set N) :
submodule.map₂ f (submodule.span R s) (submodule.span R t) = submodule.span R (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} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M →ₗ[R] N →ₗ[R] P) (p : submodule R M) :
@[simp]
theorem submodule.map₂_bot_left {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M →ₗ[R] N →ₗ[R] P) (q : submodule R N) :
theorem submodule.map₂_le_map₂ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] {f : M →ₗ[R] N →ₗ[R] P} {p₁ p₂ : submodule R M} {q₁ q₂ : submodule R N} (hp : p₁ p₂) (hq : q₁ q₂) :
submodule.map₂ f p₁ q₁ submodule.map₂ f p₂ q₂
theorem submodule.map₂_le_map₂_left {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] {f : M →ₗ[R] N →ₗ[R] P} {p₁ p₂ : submodule R M} {q : submodule R N} (h : p₁ p₂) :
theorem submodule.map₂_le_map₂_right {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] {f : M →ₗ[R] N →ₗ[R] P} {p : submodule R M} {q₁ q₂ : submodule R N} (h : q₁ q₂) :
theorem submodule.map₂_sup_right {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M →ₗ[R] N →ₗ[R] P) (p : submodule R M) (q₁ q₂ : submodule R N) :
submodule.map₂ f p (q₁ q₂) = submodule.map₂ f p q₁ submodule.map₂ f p q₂
theorem submodule.map₂_sup_left {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M →ₗ[R] N →ₗ[R] P) (p₁ p₂ : submodule R M) (q : submodule R N) :
submodule.map₂ f (p₁ p₂) q = submodule.map₂ f p₁ q submodule.map₂ f p₂ q
theorem submodule.image2_subset_map₂ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M →ₗ[R] N →ₗ[R] P) (p : submodule R M) (q : submodule R N) :
set.image2 (λ (m : M) (n : N), (f m) n) p q (submodule.map₂ f p q)
theorem submodule.map₂_eq_span_image2 {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M →ₗ[R] N →ₗ[R] P) (p : submodule R M) (q : submodule R N) :
submodule.map₂ f p q = submodule.span R (set.image2 (λ (m : M) (n : N), (f m) 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} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M →ₗ[R] N →ₗ[R] P) (s : ι → submodule R M) (t : submodule R N) :
submodule.map₂ f (⨆ (i : ι), s i) t = ⨆ (i : ι), submodule.map₂ f (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} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : M →ₗ[R] N →ₗ[R] P) (s : submodule R M) (t : ι → submodule R N) :
submodule.map₂ f s (⨆ (i : ι), t i) = ⨆ (i : ι), submodule.map₂ f s (t i)