Mathlib.Algebra.Module.Submodule.Bilinear

Submodule.map₂ definition

(f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N) : Submodule R P

Full source

/-- Map a pair of submodules under a bilinear map.

This is the submodule version of `Set.image2`. -/
def map₂ (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N) : Submodule R P :=
  ⨆ s : p, q.map (f s)

Image of submodules under a bilinear map

Informal description

Given a bilinear map $f \colon M \to N \to P$ over a semiring $R$, and submodules $p \subseteq M$ and $q \subseteq N$, the submodule $\mathrm{map}_2(f, p, q) \subseteq P$ is defined as the supremum of the images of $q$ under the linear maps $f(s)$ for each $s \in p$. In other words, it is the smallest submodule of $P$ containing all elements of the form $f(m, n)$ where $m \in p$ and $n \in q$.

Submodule.apply_mem_map₂ theorem

 (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

Full source

theorem apply_mem_map₂ (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 :=
  (le_iSup _ ⟨m, hm⟩ : _ ≤ map₂ f p q) ⟨n, hn, by rfl⟩

Image of Bilinear Map on Submodules Lies in Mapped Submodule

Informal description

Let $R$ be a semiring, and let $M$, $N$, and $P$ be modules over $R$. Given a bilinear map $f \colon M \to N \to P$, submodules $p \subseteq M$ and $q \subseteq N$, and elements $m \in p$ and $n \in q$, the image $f(m, n)$ belongs to the submodule $\mathrm{map}_2(f, p, q) \subseteq P$.

Submodule.map₂_le theorem

 {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

Full source

theorem map₂_le {f : M →ₗ[R] N →ₗ[R] P} {p : Submodule R M} {q : Submodule R N}
    {r : Submodule R P} : map₂map₂ f p q ≤ r ↔ ∀ m ∈ p, ∀ n ∈ q, f m n ∈ r :=
  ⟨fun H _m hm _n hn => H <| apply_mem_map₂ _ hm hn, fun H =>
    iSup_le fun ⟨m, hm⟩ => map_le_iff_le_comap.2 fun n hn => H m hm n hn⟩

Characterization of Submodule Containment for Bilinear Map Images

Informal description

Let $R$ be a semiring, and let $M$, $N$, and $P$ be $R$-modules. Given a bilinear map $f \colon M \to N \to P$, submodules $p \subseteq M$, $q \subseteq N$, and $r \subseteq P$, the submodule $\mathrm{map}_2(f, p, q)$ is contained in $r$ if and only if for all $m \in p$ and $n \in q$, the image $f(m, n)$ belongs to $r$.

Submodule.map₂_span_span theorem

 (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 n => f m n) s t)

Full source

theorem map₂_span_span (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 n => f m n) s t) := by
  apply le_antisymm
  · rw [map₂_le]
    apply @span_induction R M _ _ _ s
    on_goal 1 =>
      intro a ha
      apply @span_induction R N _ _ _ t
      · intro b hb
        exact subset_span ⟨_, ‹_›, _, ‹_›, rfl⟩
    all_goals
      intros
      simp only [*, add_mem, smul_mem, zero_mem, map_zero, map_add,
        LinearMap.zero_apply, LinearMap.add_apply, LinearMap.smul_apply, map_smul]
  · rw [span_le, image2_subset_iff]
    intro a ha b hb
    exact apply_mem_map₂ _ (subset_span ha) (subset_span hb)

Image of Spans under Bilinear Map Equals Span of Pairwise Images

Informal description

Let $R$ be a semiring, and let $M$, $N$, and $P$ be $R$-modules. Given a bilinear map $f \colon M \to N \to P$ and subsets $s \subseteq M$, $t \subseteq N$, the image of the spans $\operatorname{span}_R s$ and $\operatorname{span}_R t$ under $f$ is equal to the span of the set $\{f(m, n) \mid m \in s, n \in t\}$. In other words: \[ \mathrm{map}_2(f, \operatorname{span}_R s, \operatorname{span}_R t) = \operatorname{span}_R \{f(m, n) \mid m \in s, n \in t\}. \]

Submodule.map₂_bot_right theorem

(f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) : map₂ f p ⊥ = ⊥

Full source

@[simp]
theorem map₂_bot_right (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) : map₂ f p ⊥ = ⊥ :=
  eq_bot_iff.2 <|
    map₂_le.2 fun m _hm n hn => by
      rw [Submodule.mem_bot] at hn
      rw [hn, LinearMap.map_zero]; simp only [mem_bot]

Image of Submodule and Zero Submodule under Bilinear Map is Zero

Informal description

Let $R$ be a semiring, $M$, $N$, and $P$ be $R$-modules, and $f \colon M \to N \to P$ be a bilinear map. For any submodule $p \subseteq M$, the image of $p$ and the zero submodule $\{0\} \subseteq N$ under $f$ is the zero submodule $\{0\} \subseteq P$, i.e., $\mathrm{map}_2(f, p, \{0\}) = \{0\}$.

Submodule.map₂_bot_left theorem

(f : M →ₗ[R] N →ₗ[R] P) (q : Submodule R N) : map₂ f ⊥ q = ⊥

Full source

@[simp]
theorem map₂_bot_left (f : M →ₗ[R] N →ₗ[R] P) (q : Submodule R N) : map₂ f ⊥ q = ⊥ :=
  eq_bot_iff.2 <|
    map₂_le.2 fun m hm n _ => by
      rw [Submodule.mem_bot] at hm ⊢
      rw [hm, LinearMap.map_zero₂]

Bilinear Map Image of Zero Submodule is Zero Submodule (Left Case)

Informal description

Let $R$ be a semiring, and let $M$, $N$, and $P$ be $R$-modules. For any bilinear map $f \colon M \to N \to P$ and any submodule $q \subseteq N$, the image of the zero submodule $\{0\} \subseteq M$ and $q$ under $f$ is the zero submodule $\{0\} \subseteq P$, i.e., $\mathrm{map}_2(f, \{0\}, q) = \{0\}$.

Submodule.map₂_le_map₂ theorem

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

Full source

@[gcongr, mono]
theorem map₂_le_map₂ {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₂ :=
  map₂_le.2 fun _m hm _n hn => apply_mem_map₂ _ (hp hm) (hq hn)

Monotonicity of Bilinear Map Image with Respect to Submodule Inclusion

Informal description

Let $R$ be a semiring, and let $M$, $N$, and $P$ be $R$-modules. Given a bilinear map $f \colon M \to N \to P$, and submodules $p_1 \subseteq p_2 \subseteq M$ and $q_1 \subseteq q_2 \subseteq N$, the image submodule $\mathrm{map}_2(f, p_1, q_1)$ is contained in $\mathrm{map}_2(f, p_2, q_2)$.

Submodule.map₂_le_map₂_left theorem

 {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

Full source

theorem map₂_le_map₂_left {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 :=
  map₂_le_map₂ h (le_refl q)

Left Monotonicity of Bilinear Map Image with Respect to Submodule Inclusion

Informal description

Let $R$ be a semiring, and let $M$, $N$, and $P$ be $R$-modules. Given a bilinear map $f \colon M \to N \to P$, submodules $p_1 \subseteq p_2 \subseteq M$, and a submodule $q \subseteq N$, the image submodule $\mathrm{map}_2(f, p_1, q)$ is contained in $\mathrm{map}_2(f, p_2, q)$.

Submodule.map₂_le_map₂_right theorem

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

Full source

theorem map₂_le_map₂_right {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₂ :=
  map₂_le_map₂ (le_refl p) h

Right Monotonicity of Bilinear Map Image with Respect to Submodule Inclusion

Informal description

Let $R$ be a semiring, and let $M$, $N$, and $P$ be $R$-modules. Given a bilinear map $f \colon M \to N \to P$, a submodule $p \subseteq M$, and submodules $q_1 \subseteq q_2 \subseteq N$, the image submodule $\mathrm{map}_2(f, p, q_1)$ is contained in $\mathrm{map}_2(f, p, q_2)$.

Submodule.map₂_sup_right theorem

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

Full source

theorem map₂_sup_right (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q₁ q₂ : Submodule R N) :
    map₂ f p (q₁ ⊔ q₂) = map₂map₂ f p q₁ ⊔ map₂ f p q₂ :=
  le_antisymm
    (map₂_le.2 fun _m hm _np hnp =>
      let ⟨_n, hn, _p, hp, hnp⟩ := mem_sup.1 hnp
      mem_sup.2 ⟨_, apply_mem_map₂ _ hm hn, _, apply_mem_map₂ _ hm hp, hnp ▸ (map_add _ _ _).symm⟩)
    (sup_le (map₂_le_map₂_right le_sup_left) (map₂_le_map₂_right le_sup_right))

Right Supremum Preservation under Bilinear Map on Submodules

Informal description

Let $R$ be a semiring, and let $M$, $N$, and $P$ be $R$-modules. Given a bilinear map $f \colon M \to N \to P$, a submodule $p \subseteq M$, and submodules $q_1, q_2 \subseteq N$, the image of $p$ and the supremum $q_1 \sqcup q_2$ under $f$ is equal to the supremum of the images of $p$ with $q_1$ and $p$ with $q_2$ under $f$. That is, \[ \mathrm{map}_2(f, p, q_1 \sqcup q_2) = \mathrm{map}_2(f, p, q_1) \sqcup \mathrm{map}_2(f, p, q_2). \]

Submodule.map₂_sup_left theorem

 (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

Full source

theorem map₂_sup_left (f : M →ₗ[R] N →ₗ[R] P) (p₁ p₂ : Submodule R M) (q : Submodule R N) :
    map₂ f (p₁ ⊔ p₂) q = map₂map₂ f p₁ q ⊔ map₂ f p₂ q :=
  le_antisymm
    (map₂_le.2 fun _mn hmn _p hp =>
      let ⟨_m, hm, _n, hn, hmn⟩ := mem_sup.1 hmn
      mem_sup.2
        ⟨_, apply_mem_map₂ _ hm hp, _, apply_mem_map₂ _ hn hp,
          hmn ▸ (LinearMap.map_add₂ _ _ _ _).symm⟩)
    (sup_le (map₂_le_map₂_left le_sup_left) (map₂_le_map₂_left le_sup_right))

Left Supremum Preservation under Bilinear Map Image

Informal description

Let $R$ be a semiring, and let $M$, $N$, and $P$ be $R$-modules. Given a bilinear map $f \colon M \to N \to P$ and submodules $p_1, p_2 \subseteq M$ and $q \subseteq N$, the image of the supremum $p_1 \sqcup p_2$ under $f$ with $q$ equals the supremum of the images of $p_1$ and $p_2$ under $f$ with $q$. That is: \[ \mathrm{map}_2(f, p_1 \sqcup p_2, q) = \mathrm{map}_2(f, p_1, q) \sqcup \mathrm{map}_2(f, p_2, q). \]

Submodule.image2_subset_map₂ theorem

 (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N) :
  Set.image2 (fun m n => f m n) (↑p : Set M) (↑q : Set N) ⊆ (↑(map₂ f p q) : Set P)

Full source

theorem image2_subset_map₂ (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N) :
    Set.image2Set.image2 (fun m n => f m n) (↑p : Set M) (↑q : Set N) ⊆ (↑(map₂ f p q) : Set P) := by
  rintro _ ⟨i, hi, j, hj, rfl⟩
  exact apply_mem_map₂ _ hi hj

Image of Bilinear Map on Submodules is Contained in Mapped Submodule

Informal description

Let $R$ be a semiring, and let $M$, $N$, and $P$ be $R$-modules. Given a bilinear map $f \colon M \to N \to P$ and submodules $p \subseteq M$, $q \subseteq N$, the image set $\{f(m, n) \mid m \in p, n \in q\}$ is contained in the submodule $\mathrm{map}_2(f, p, q) \subseteq P$.

Submodule.map₂_eq_span_image2 theorem

 (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N) :
  map₂ f p q = span R (Set.image2 (fun m n => f m n) (p : Set M) (q : Set N))

Full source

theorem map₂_eq_span_image2 (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N) :
    map₂ f p q = span R (Set.image2 (fun m n => f m n) (p : Set M) (q : Set N)) := by
  rw [← map₂_span_span, span_eq, span_eq]

Image of Submodules under Bilinear Map Equals Span of Pairwise Images

Informal description

Let $R$ be a semiring, and let $M$, $N$, and $P$ be $R$-modules. Given a bilinear map $f \colon M \to N \to P$ and submodules $p \subseteq M$, $q \subseteq N$, the image of $p$ and $q$ under $f$ is equal to the span of the set $\{f(m, n) \mid m \in p, n \in q\}$. In other words: \[ \mathrm{map}_2(f, p, q) = \operatorname{span}_R \{f(m, n) \mid m \in p, n \in q\}. \]

Submodule.map₂_flip theorem

(f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N) : map₂ f.flip q p = map₂ f p q

Full source

theorem map₂_flip (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N) :
    map₂ f.flip q p = map₂ f p q := by
  rw [map₂_eq_span_image2, map₂_eq_span_image2, Set.image2_swap]
  rfl

Image of Submodules under Flipped Bilinear Map Equals Original Image

Informal description

Let $R$ be a semiring, and let $M$, $N$, and $P$ be $R$-modules. Given a bilinear map $f \colon M \to N \to P$ and submodules $p \subseteq M$, $q \subseteq N$, the image of $q$ and $p$ under the flipped bilinear map $f.flip$ equals the image of $p$ and $q$ under $f$. That is: \[ \mathrm{map}_2(f.flip, q, p) = \mathrm{map}_2(f, p, q). \]

Submodule.map₂_iSup_left theorem

 (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

Full source

theorem map₂_iSup_left (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 := by
  suffices map₂ f (⨆ i, span R (s i : Set M)) (span R t) = ⨆ i, map₂ f (span R (s i)) (span R t) by
    simpa only [span_eq] using this
  simp_rw [map₂_span_span, ← span_iUnion, map₂_span_span, Set.image2_iUnion_left]

Bilinear Image of Supremum of Submodules Equals Supremum of Bilinear Images (Left Argument)

Informal description

Let $R$ be a semiring, and let $M$, $N$, and $P$ be $R$-modules. Given a bilinear map $f \colon M \to N \to P$, a family of submodules $\{s_i\}_{i \in \iota}$ of $M$, and a submodule $t$ of $N$, the image of the supremum $\bigsqcup_i s_i$ and $t$ under $f$ equals the supremum of the images $f(s_i, t)$ for all $i \in \iota$. In symbols: \[ \mathrm{map}_2(f, \bigsqcup_i s_i, t) = \bigsqcup_i \mathrm{map}_2(f, s_i, t). \]

Submodule.map₂_iSup_right theorem

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

Full source

theorem map₂_iSup_right (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) := by
  suffices map₂ f (span R s) (⨆ i, span R (t i : Set N)) = ⨆ i, map₂ f (span R s) (span R (t i)) by
    simpa only [span_eq] using this
  simp_rw [map₂_span_span, ← span_iUnion, map₂_span_span, Set.image2_iUnion_right]

Bilinear Image of Supremum Equals Supremum of Bilinear Images (Right Argument)

Informal description

Let $R$ be a semiring, and let $M$, $N$, and $P$ be $R$-modules. Given a bilinear map $f \colon M \to N \to P$, a submodule $s \subseteq M$, and a family of submodules $\{t_i\}_{i \in \iota}$ of $N$, the image of $s$ and the supremum $\bigsqcup_i t_i$ under $f$ equals the supremum of the images $f(s, t_i)$ for all $i \in \iota$. In symbols: \[ \mathrm{map}_2(f, s, \bigsqcup_i t_i) = \bigsqcup_i \mathrm{map}_2(f, s, t_i). \]

Submodule.map₂_span_singleton_eq_map theorem

(f : M →ₗ[R] N →ₗ[R] P) (m : M) : map₂ f (span R { m }) = map (f m)

Full source

theorem map₂_span_singleton_eq_map (f : M →ₗ[R] N →ₗ[R] P) (m : M) :
    map₂ f (span R {m}) = map (f m) := by
  funext s
  rw [← span_eq s, map₂_span_span, image2_singleton_left, map_span]

Bilinear image of a span of a singleton equals image under the corresponding linear map

Informal description

Let $R$ be a semiring, and let $M$, $N$, and $P$ be $R$-modules. Given a bilinear map $f \colon M \to N \to P$ and an element $m \in M$, the image of the span $\operatorname{span}_R \{m\}$ and any submodule $q \subseteq N$ under $f$ is equal to the image of $q$ under the linear map $f(m) \colon N \to P$. In other words: \[ \mathrm{map}_2(f, \operatorname{span}_R \{m\}, q) = f(m)(q). \]

Submodule.map₂_span_singleton_eq_map_flip theorem

(f : M →ₗ[R] N →ₗ[R] P) (s : Submodule R M) (n : N) : map₂ f s (span R { n }) = map (f.flip n) s

Full source

theorem map₂_span_singleton_eq_map_flip (f : M →ₗ[R] N →ₗ[R] P) (s : Submodule R M) (n : N) :
    map₂ f s (span R {n}) = map (f.flip n) s := by rw [← map₂_span_singleton_eq_map, map₂_flip]

Bilinear image of a span of a singleton equals image under the flipped linear map

Informal description

Let $R$ be a semiring, and let $M$, $N$, and $P$ be $R$-modules. Given a bilinear map $f \colon M \to N \to P$, a submodule $s \subseteq M$, and an element $n \in N$, the image of $s$ and the span $\operatorname{span}_R \{n\}$ under $f$ equals the image of $s$ under the linear map obtained by flipping $f$ and evaluating at $n$. In symbols: \[ \mathrm{map}_2(f, s, \operatorname{span}_R \{n\}) = (f.flip)(n)(s). \]

Mathlib.Algebra.Module.Submodule.Bilinear

Main results

Notes