Images of pairs of submodules under bilinear maps #
This file provides Submodule.map₂, which is later used to implement Submodule.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.NAry.
Please keep them in sync.
def
Submodule.map₂
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid 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
Instances For
theorem
Submodule.apply_mem_map₂
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid 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}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid 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 ∈ p, ∀ 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}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid 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 (fun (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}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid 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}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid 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}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
{f : M →ₗ[R] N →ₗ[R] P}
{p₁ : Submodule R M}
{p₂ : Submodule R M}
{q₁ : Submodule R N}
{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}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
{f : M →ₗ[R] N →ₗ[R] P}
{p₁ : Submodule R M}
{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}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
{f : M →ₗ[R] N →ₗ[R] P}
{p : Submodule R M}
{q₁ : Submodule R N}
{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}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
(f : M →ₗ[R] N →ₗ[R] P)
(p : Submodule R M)
(q₁ : Submodule R N)
(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}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
(f : M →ₗ[R] N →ₗ[R] P)
(p₁ : Submodule R M)
(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}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid 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 (fun (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}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid 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 (fun (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}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid 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₂_iSup_left
{ι : Sort uι}
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid 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₂_iSup_right
{ι : Sort uι}
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid 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}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid 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}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid 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