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 their Set.image2.

Notes

This file is quite similar to the n-ary section of Mathlib/Data/Set/Basic.lean and to Mathlib/Order/Filter/NAry.lean. Please keep them in sync.

TODO

Generalize this file to semilinear maps.

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

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 ∈ 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} : 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) : map₂ f (span R s) (span R t) = 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) : 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) : 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₁ p₂ : Submodule R M} {q₁ q₂ : Submodule R N} (hp : p₁ ≤ p₂) (hq : q₁ ≤ q₂) : map₂ f p₁ q₁ ≤ 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₁ p₂ : Submodule R M} {q : Submodule R N} (h : p₁ ≤ p₂) : map₂ f p₁ q ≤ 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₁ q₂ : Submodule R N} (h : q₁ ≤ q₂) : map₂ f p q₁ ≤ 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₁ q₂ : Submodule R N) : map₂ f p (q₁ ⊔ q₂) = map₂ f p q₁ ⊔ 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₁ p₂ : Submodule R M) (q : Submodule R N) : map₂ f (p₁ ⊔ p₂) q = map₂ f p₁ q ⊔ 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 ⊆ ↑(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) : map₂ f p q = 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) : map₂ f.flip q p = 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) : map₂ f (⨆ (i : ι), s i) t = ⨆ (i : ι), 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) : map₂ f s (⨆ (i : ι), t i) = ⨆ (i : ι), 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) : map₂ f (R ∙ m) = 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) : map₂ f s (R ∙ n) = map (f.flip n) s

theorem Submodule.map_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] {P₂ : Type u_7} [AddCommMonoid P₂] [Module R P₂] (f : P →ₗ[R] P₂) (g : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N) : map f (map₂ g p q) = map₂ (g.compr₂ f) p q

theorem Submodule.map₂_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] {N₂ : Type u_6} [AddCommMonoid N₂] [Module R N₂] (f : M →ₗ[R] N₂ →ₗ[R] P) (g : N →ₗ[R] N₂) (p : Submodule R M) (q : Submodule R N) : map₂ f p (map g q) = map₂ (f.compl₂ g) p q

theorem Submodule.map₂_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] {M₂ : Type u_5} [AddCommMonoid M₂] [Module R M₂] (f : M₂ →ₗ[R] N →ₗ[R] P) (g : M →ₗ[R] M₂) (p : Submodule R M) (q : Submodule R N) : map₂ f (map g p) q = map₂ (f ∘ₗ g) p q

theorem Submodule.map₂_map_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] {M₂ : Type u_5} {N₂ : Type u_6} [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M₂] [Module R N₂] (f : M₂ →ₗ[R] N₂ →ₗ[R] P) (g : M →ₗ[R] M₂) (h : N →ₗ[R] N₂) (p : Submodule R M) (q : Submodule R N) : map₂ f (map g p) (map h q) = map₂ (f.compl₁₂ g h) p q