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 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

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₂ (LinearMap.flip f) 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 ((LinearMap.flip f) n) s

theorem LinearMap.ker_restrictBilinear_eq_of_codisjoint {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} (hpq : Codisjoint p q) {B : LinearMap.BilinForm R M} (hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0) : LinearMap.ker (Submodule.restrictBilinear p B) = Submodule.comap (Submodule.subtype p) (LinearMap.ker B)