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 theirset.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}
[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 R P
Map a pair of submodules under a bilinear map.
This is the submodule version of set.image2.
Equations
- submodule.map₂ f p q = ⨆ (s : ↥p), submodule.map (⇑f ↑s) q
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) :
⇑(⇑f m) n ∈ submodule.map₂ f p 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} :
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) :
submodule.map₂ f p ⊥ = ⊥
@[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) :
submodule.map₂ f ⊥ q = ⊥
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₂) :
submodule.map₂ f p₁ q ≤ submodule.map₂ f p₂ q
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₂) :
submodule.map₂ f p q₁ ≤ submodule.map₂ f p 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₂_flip
{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.flip q p = submodule.map₂ f 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)
theorem
submodule.map₂_span_singleton_eq_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) :
submodule.map₂ f (submodule.span R {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}
[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)
(n : N) :
submodule.map₂ f s (submodule.span R {n}) = submodule.map (⇑(f.flip) n) s