Documentation

Mathlib.Algebra.Module.Submodule.Bilinear

Images of pairs of submodules under bilinear maps #

This file provides Submodule.map₂, which is later used to implement Submodule.mul.

Main results #

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

Map a pair of submodules under a bilinear map.

This is the submodule version of Set.image2.

Equations
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 mp, nq, (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) :
    @[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) :
    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₂) :
    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₂) :
    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) :
    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) :
    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) :
    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 : xp, yq, (B x) y = 0) :