Mathlib.LinearAlgebra.BilinearMap

LinearMap.mk₂'ₛₗ definition

 (f : M → N → P) (H1 : ∀ m₁ m₂ n, f (m₁ + m₂) n = f m₁ n + f m₂ n) (H2 : ∀ (c : R) (m n), f (c • m) n = ρ₁₂ c • f m n)
  (H3 : ∀ m n₁ n₂, f m (n₁ + n₂) = f m n₁ + f m n₂) (H4 : ∀ (c : S) (m n), f m (c • n) = σ₁₂ c • f m n) :
  M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P

Full source

/-- Create a bilinear map from a function that is semilinear in each component.
See `mk₂'` and `mk₂` for the linear case. -/
def mk₂'ₛₗ (f : M → N → P) (H1 : ∀ m₁ m₂ n, f (m₁ + m₂) n = f m₁ n + f m₂ n)
    (H2 : ∀ (c : R) (m n), f (c • m) n = ρ₁₂ c • f m n)
    (H3 : ∀ m n₁ n₂, f m (n₁ + n₂) = f m n₁ + f m n₂)
    (H4 : ∀ (c : S) (m n), f m (c • n) = σ₁₂ c • f m n) : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P where
  toFun m :=
    { toFun := f m
      map_add' := H3 m
      map_smul' := fun c => H4 c m }
  map_add' m₁ m₂ := LinearMap.ext <| H1 m₁ m₂
  map_smul' c m := LinearMap.ext <| H2 c m

Constructor for Semilinear Bilinear Maps

Informal description

Given a function $f : M \to N \to P$ that is semilinear in each component, the constructor `LinearMap.mk₂'ₛₗ` creates a bilinear map $M \to_{ρ₁₂} N \to_{σ₁₂} P$. Specifically, for $f$ to be semilinear, it must satisfy the following properties: 1. Additivity in the first argument: $f(m₁ + m₂, n) = f(m₁, n) + f(m₂, n)$ for all $m₁, m₂ \in M$ and $n \in N$. 2. Semilinearity in the first argument: $f(c \cdot m, n) = ρ₁₂(c) \cdot f(m, n)$ for all $c \in R$, $m \in M$, and $n \in N$. 3. Additivity in the second argument: $f(m, n₁ + n₂) = f(m, n₁) + f(m, n₂)$ for all $m \in M$ and $n₁, n₂ \in N$. 4. Semilinearity in the second argument: $f(m, c \cdot n) = σ₁₂(c) \cdot f(m, n)$ for all $c \in S$, $m \in M$, and $n \in N$. Here, $ρ₁₂ : R \to R₂$ and $σ₁₂ : S \to S₂$ are ring homomorphisms, and the resulting bilinear map is semilinear with respect to these homomorphisms.

LinearMap.mk₂'ₛₗ_apply theorem

 (f : M → N → P) {H1 H2 H3 H4} (m : M) (n : N) : (mk₂'ₛₗ ρ₁₂ σ₁₂ f H1 H2 H3 H4 : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) m n = f m n

Full source

@[simp]
theorem mk₂'ₛₗ_apply (f : M → N → P) {H1 H2 H3 H4} (m : M) (n : N) :
    (mk₂'ₛₗ ρ₁₂ σ₁₂ f H1 H2 H3 H4 : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) m n = f m n := rfl

Evaluation of Constructed Semilinear Bilinear Map

Informal description

For any function $f : M \to N \to P$ that is semilinear in both arguments with respect to ring homomorphisms $\rho_{12} : R \to R_2$ and $\sigma_{12} : S \to S_2$, and for any elements $m \in M$ and $n \in N$, the bilinear map constructed via `LinearMap.mk₂'ₛₗ` satisfies $(mk₂'ₛₗ \rho_{12} \sigma_{12} f H1 H2 H3 H4)(m, n) = f(m, n)$.

LinearMap.mk₂' definition

 (f : M → N → Pₗ) (H1 : ∀ m₁ m₂ n, f (m₁ + m₂) n = f m₁ n + f m₂ n) (H2 : ∀ (c : R) (m n), f (c • m) n = c • f m n)
  (H3 : ∀ m n₁ n₂, f m (n₁ + n₂) = f m n₁ + f m n₂) (H4 : ∀ (c : S) (m n), f m (c • n) = c • f m n) : M →ₗ[R] N →ₗ[S] Pₗ

Full source

/-- Create a bilinear map from a function that is linear in each component.
See `mk₂` for the special case where both arguments come from modules over the same ring. -/
def mk₂' (f : M → N → Pₗ) (H1 : ∀ m₁ m₂ n, f (m₁ + m₂) n = f m₁ n + f m₂ n)
    (H2 : ∀ (c : R) (m n), f (c • m) n = c • f m n)
    (H3 : ∀ m n₁ n₂, f m (n₁ + n₂) = f m n₁ + f m n₂)
    (H4 : ∀ (c : S) (m n), f m (c • n) = c • f m n) : M →ₗ[R] N →ₗ[S] Pₗ :=
  mk₂'ₛₗ (RingHom.id R) (RingHom.id S) f H1 H2 H3 H4

Constructor for bilinear maps

Informal description

Given a function $ f : M \to N \to P $ that is linear in each component, the constructor `LinearMap.mk₂'` creates a bilinear map $ M \to_{R} N \to_{S} P $. Specifically, for $ f $ to be bilinear, it must satisfy the following properties: 1. Additivity in the first argument: $ f(m_1 + m_2, n) = f(m_1, n) + f(m_2, n) $ for all $ m_1, m_2 \in M $ and $ n \in N $. 2. Linearity in the first argument: $ f(c \cdot m, n) = c \cdot f(m, n) $ for all $ c \in R $, $ m \in M $, and $ n \in N $. 3. Additivity in the second argument: $ f(m, n_1 + n_2) = f(m, n_1) + f(m, n_2) $ for all $ m \in M $ and $ n_1, n_2 \in N $. 4. Linearity in the second argument: $ f(m, c \cdot n) = c \cdot f(m, n) $ for all $ c \in S $, $ m \in M $, and $ n \in N $. Here, $ R $ and $ S $ are the respective rings over which $ M $ and $ N $ are modules, and $ P $ is a module over both $ R $ and $ S $ with commuting actions.

LinearMap.mk₂'_apply theorem

 (f : M → N → Pₗ) {H1 H2 H3 H4} (m : M) (n : N) : (mk₂' R S f H1 H2 H3 H4 : M →ₗ[R] N →ₗ[S] Pₗ) m n = f m n

Full source

@[simp]
theorem mk₂'_apply (f : M → N → Pₗ) {H1 H2 H3 H4} (m : M) (n : N) :
    (mk₂' R S f H1 H2 H3 H4 : M →ₗ[R] N →ₗ[S] Pₗ) m n = f m n := rfl

Evaluation of Constructed Bilinear Map

Informal description

For any function $f \colon M \to N \to P$ that is bilinear (i.e., linear in each argument), and for any elements $m \in M$ and $n \in N$, the bilinear map constructed via `LinearMap.mk₂'` satisfies $(mk₂'\, R\, S\, f\, H1\, H2\, H3\, H4)(m, n) = f(m, n)$.

LinearMap.ext₂ theorem

{f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (H : ∀ m n, f m n = g m n) : f = g

Full source

theorem ext₂ {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (H : ∀ m n, f m n = g m n) : f = g :=
  LinearMap.ext fun m => LinearMap.ext fun n => H m n

Extensionality of Semilinear Maps in Both Arguments

Informal description

Let $M$, $N$, and $P$ be modules over rings $R$, $S$, $R₂$, and $S₂$ respectively, with ring homomorphisms $\rho_{12} \colon R \to R₂$ and $\sigma_{12} \colon S \to S₂$. For any two semilinear maps $f, g \colon M \to_{[\rho_{12}]} N \to_{[\sigma_{12}]} P$, if $f(m, n) = g(m, n)$ for all $m \in M$ and $n \in N$, then $f = g$.

LinearMap.congr_fun₂ theorem

{f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (h : f = g) (x y) : f x y = g x y

Full source

theorem congr_fun₂ {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (h : f = g) (x y) : f x y = g x y :=
  LinearMap.congr_fun (LinearMap.congr_fun h x) y

Equality of Semilinear Maps Implies Pointwise Equality

Informal description

For any two semilinear maps $ f, g \colon M \to_{[\rho_{12}]} N \to_{[\sigma_{12}]} P $, if $ f = g $, then $ f(x, y) = g(x, y) $ for all $ x \in M $ and $ y \in N $.

LinearMap.ext_iff₂ theorem

{f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} : f = g ↔ ∀ m n, f m n = g m n

Full source

theorem ext_iff₂ {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} : f = g ↔ ∀ m n, f m n = g m n :=
  ⟨congr_fun₂, ext₂⟩

Equivalence of Semilinear Map Equality and Pointwise Equality

Informal description

For any two semilinear maps $ f, g \colon M \to_{[\rho_{12}]} N \to_{[\sigma_{12}]} P $, the maps $ f $ and $ g $ are equal if and only if $ f(m, n) = g(m, n) $ for all $ m \in M $ and $ n \in N $.

LinearMap.flip definition

(f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) : N →ₛₗ[σ₁₂] M →ₛₗ[ρ₁₂] P

Full source

/-- Given a linear map from `M` to linear maps from `N` to `P`, i.e., a bilinear map from `M × N` to
`P`, change the order of variables and get a linear map from `N` to linear maps from `M` to `P`. -/
def flip (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) : N →ₛₗ[σ₁₂] M →ₛₗ[ρ₁₂] P :=
  mk₂'ₛₗ σ₁₂ ρ₁₂ (fun n m => f m n) (fun _ _ m => (f m).map_add _ _)
    (fun _ _  m  => (f m).map_smulₛₗ _ _)
    (fun n m₁ m₂ => by simp only [map_add, add_apply])
    -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 changed `map_smulₛₗ` into `map_smulₛₗ _`.
    -- It looks like we now run out of assignable metavariables.
    (fun c n  m  => by simp only [map_smulₛₗ _, smul_apply])

Flip of a bilinear map

Informal description

Given a bilinear map $f \colon M \to_{[\rho_{12}]} N \to_{[\sigma_{12}]} P$ that is semilinear in both arguments, the function `LinearMap.flip` swaps the order of the arguments, yielding a bilinear map $N \to_{[\sigma_{12}]} M \to_{[\rho_{12}]} P$. Specifically, for any $m \in M$ and $n \in N$, the flipped map satisfies $(f.flip)(n)(m) = f(m)(n)$.

LinearMap.flip_apply theorem

(f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (m : M) (n : N) : flip f n m = f m n

Full source

@[simp]
theorem flip_apply (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (m : M) (n : N) : flip f n m = f m n := rfl

Flip Evaluation of Bilinear Map: $(f.flip)(n)(m) = f(m)(n)$

Informal description

For any bilinear map $f \colon M \to_{[\rho_{12}]} N \to_{[\sigma_{12}]} P$ and any elements $m \in M$, $n \in N$, the flipped map satisfies $(f.flip)(n)(m) = f(m)(n)$.

LinearMap.flip_flip theorem

(f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) : f.flip.flip = f

Full source

@[simp]
theorem flip_flip (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) : f.flip.flip = f :=
  LinearMap.ext₂ fun _x _y => (f.flip.flip_apply _ _).trans (f.flip_apply _ _)

Double Flip of Bilinear Map Returns Original Map

Informal description

Let $M$, $N$, and $P$ be modules over rings $R$, $S$, $R₂$, and $S₂$ respectively, with ring homomorphisms $\rho_{12} \colon R \to R₂$ and $\sigma_{12} \colon S \to S₂$. For any bilinear map $f \colon M \to_{[\rho_{12}]} N \to_{[\sigma_{12}]} P$, flipping the arguments twice returns the original map, i.e., $f.flip.flip = f$.

LinearMap.flip_inj theorem

{f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (H : flip f = flip g) : f = g

Full source

theorem flip_inj {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (H : flip f = flip g) : f = g :=
  ext₂ fun m n => show flip f n m = flip g n m by rw [H]

Injectivity of the Flip Operation on Bilinear Maps

Informal description

Let $M$, $N$, and $P$ be modules over rings $R$, $S$, $R₂$, and $S₂$ respectively, with ring homomorphisms $\rho_{12} \colon R \to R₂$ and $\sigma_{12} \colon S \to S₂$. For any two semilinear maps $f, g \colon M \to_{[\rho_{12}]} N \to_{[\sigma_{12}]} P$, if the flipped maps $f.flip$ and $g.flip$ are equal, then $f = g$.

LinearMap.map_zero₂ theorem

(f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (y) : f 0 y = 0

Full source

theorem map_zero₂ (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (y) : f 0 y = 0 :=
  (flip f y).map_zero

Bilinearity Condition: $f(0, y) = 0$

Informal description

For any bilinear map $f \colon M \to_{[\rho_{12}]} N \to_{[\sigma_{12}]} P$ and any element $y \in N$, the evaluation of $f$ at the zero element of $M$ and $y$ yields the zero element of $P$, i.e., $f(0, y) = 0$.

LinearMap.map_neg₂ theorem

(f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P') (x y) : f (-x) y = -f x y

Full source

theorem map_neg₂ (f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P') (x y) : f (-x) y = -f x y :=
  (flip f y).map_neg _

Negation in First Argument of Bilinear Map

Informal description

For any bilinear map $f \colon M' \to_{[\rho_{12}]} N \to_{[\sigma_{12}]} P'$ that is semilinear in both arguments, and for any elements $x \in M'$ and $y \in N$, the map satisfies the linearity condition in its first argument with respect to negation: $$f(-x, y) = -f(x, y).$$

LinearMap.map_sub₂ theorem

(f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P') (x y z) : f (x - y) z = f x z - f y z

Full source

theorem map_sub₂ (f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P') (x y z) : f (x - y) z = f x z - f y z :=
  (flip f z).map_sub _ _

Subtractivity in First Argument of Bilinear Map

Informal description

For any bilinear map $f \colon M' \to_{[\rho_{12}]} N \to_{[\sigma_{12}]} P'$ that is semilinear in both arguments, and for any elements $x, y \in M'$ and $z \in N$, the map satisfies the linearity condition in its first argument with respect to subtraction: $$f(x - y, z) = f(x, z) - f(y, z).$$

LinearMap.map_add₂ theorem

(f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (x₁ x₂ y) : f (x₁ + x₂) y = f x₁ y + f x₂ y

Full source

theorem map_add₂ (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (x₁ x₂ y) : f (x₁ + x₂) y = f x₁ y + f x₂ y :=
  (flip f y).map_add _ _

Additivity in First Argument of Bilinear Map

Informal description

For any bilinear map $f \colon M \to_{[\rho_{12}]} N \to_{[\sigma_{12}]} P$ that is semilinear in both arguments, and for any elements $x_1, x_2 \in M$ and $y \in N$, the map satisfies the linearity condition in its first argument: $$f(x_1 + x_2, y) = f(x_1, y) + f(x_2, y).$$

LinearMap.map_smul₂ theorem

(f : M₂ →ₗ[R] N₂ →ₛₗ[σ₁₂] P₂) (r : R) (x y) : f (r • x) y = r • f x y

Full source

theorem map_smul₂ (f : M₂ →ₗ[R] N₂ →ₛₗ[σ₁₂] P₂) (r : R) (x y) : f (r • x) y = r • f x y :=
  (flip f y).map_smul _ _

Linearity in First Argument of Bilinear Map

Informal description

Let $M₂$, $N₂$, and $P₂$ be modules over rings $R$ and $S₂$ with a ring homomorphism $\sigma_{12} \colon S \to S₂$. Given a bilinear map $f \colon M₂ \to_{[R]} N₂ \to_{[\sigma_{12}]} P₂$ that is linear in the first argument and semilinear in the second, for any scalar $r \in R$ and elements $x \in M₂$, $y \in N₂$, the map satisfies: \[ f(r \cdot x, y) = r \cdot f(x, y). \]

LinearMap.map_smulₛₗ₂ theorem

(f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (r : R) (x y) : f (r • x) y = ρ₁₂ r • f x y

Full source

theorem map_smulₛₗ₂ (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (r : R) (x y) : f (r • x) y = ρ₁₂ r • f x y :=
  (flip f y).map_smulₛₗ _ _

Semilinearity in First Argument of Bilinear Map

Informal description

For a bilinear map $f \colon M \to_{[\rho_{12}]} N \to_{[\sigma_{12}]} P$ that is semilinear in both arguments, any scalar $r \in R$, and any elements $x \in M$, $y \in N$, the map satisfies the semilinearity condition in its first argument: $$f(r \cdot x, y) = \rho_{12}(r) \cdot f(x, y).$$

LinearMap.map_sum₂ theorem

 {ι : Type*} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (t : Finset ι) (x : ι → M) (y) : f (∑ i ∈ t, x i) y = ∑ i ∈ t, f (x i) y

Full source

theorem map_sum₂ {ι : Type*} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (t : Finset ι) (x : ι → M) (y) :
    f (∑ i ∈ t, x i) y = ∑ i ∈ t, f (x i) y :=
  _root_.map_sum (flip f y) _ _

Linearity of Bilinear Map in First Argument over Finite Sums

Informal description

Let $M$, $N$, and $P$ be modules over rings $R$, $S$, and $R_2$, $S_2$ respectively, with ring homomorphisms $\rho_{12} \colon R \to R_2$ and $\sigma_{12} \colon S \to S_2$. Given a bilinear map $f \colon M \to_{[\rho_{12}]} N \to_{[\sigma_{12}]} P$ that is semilinear in both arguments, a finite index set $I$, a family of elements $(x_i)_{i \in I}$ in $M$, and an element $y \in N$, we have: \[ f\left(\sum_{i \in I} x_i\right) y = \sum_{i \in I} f(x_i) y. \]

LinearMap.domRestrict₂ definition

(f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (q : Submodule S N) : M →ₛₗ[ρ₁₂] q →ₛₗ[σ₁₂] P

Full source

/-- Restricting a bilinear map in the second entry -/
def domRestrict₂ (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (q : Submodule S N) : M →ₛₗ[ρ₁₂] q →ₛₗ[σ₁₂] P where
  toFun m := (f m).domRestrict q
  map_add' m₁ m₂ := LinearMap.ext fun _ => by simp only [map_add, domRestrict_apply, add_apply]
  map_smul' c m :=
    LinearMap.ext fun _ => by simp only [f.map_smulₛₗ, domRestrict_apply, smul_apply]

Restriction of a bilinear map to a submodule in the second argument

Informal description

Given a bilinear map $f \colon M \to N \to P$ that is semilinear in both arguments with respect to ring homomorphisms $\rho_{12} \colon R \to R_2$ and $\sigma_{12} \colon S \to S_2$, and a submodule $q$ of $N$, the function `LinearMap.domRestrict₂` restricts the second argument of $f$ to $q$, producing a new bilinear map $M \to q \to P$ that is semilinear in both arguments with respect to the same ring homomorphisms.

LinearMap.domRestrict₂_apply theorem

 (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (q : Submodule S N) (x : M) (y : q) : f.domRestrict₂ q x y = f x y

Full source

theorem domRestrict₂_apply (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (q : Submodule S N) (x : M) (y : q) :
    f.domRestrict₂ q x y = f x y := rfl

Evaluation of Bilinear Map Restriction in Second Argument

Informal description

Given a bilinear map $f \colon M \to N \to P$ that is semilinear in both arguments with respect to ring homomorphisms $\rho_{12} \colon R \to R_2$ and $\sigma_{12} \colon S \to S_2$, a submodule $q$ of $N$, an element $x \in M$, and an element $y \in q$, the restriction of $f$ to $q$ in the second argument satisfies $(f.domRestrict₂\,q)\,x\,y = f\,x\,y$.

LinearMap.domRestrict₁₂ definition

 (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (p : Submodule R M) (q : Submodule S N) : p →ₛₗ[ρ₁₂] q →ₛₗ[σ₁₂] P

Full source

/-- Restricting a bilinear map in both components -/
def domRestrict₁₂ (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (p : Submodule R M) (q : Submodule S N) :
    p →ₛₗ[ρ₁₂] q →ₛₗ[σ₁₂] P :=
  (f.domRestrict p).domRestrict₂ q

Restriction of a bilinear map to submodules in both arguments

Informal description

Given a bilinear map $f \colon M \to N \to P$ that is semilinear in both arguments with respect to ring homomorphisms $\rho_{12} \colon R \to R_2$ and $\sigma_{12} \colon S \to S_2$, and submodules $p$ of $M$ and $q$ of $N$, the function `LinearMap.domRestrict₁₂` restricts both arguments of $f$ to $p$ and $q$ respectively, producing a new bilinear map $p \to q \to P$ that is semilinear in both arguments with respect to the same ring homomorphisms.

LinearMap.domRestrict₁₂_apply theorem

 (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (p : Submodule R M) (q : Submodule S N) (x : p) (y : q) : f.domRestrict₁₂ p q x y = f x y

Full source

theorem domRestrict₁₂_apply (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (p : Submodule R M) (q : Submodule S N)
    (x : p) (y : q) : f.domRestrict₁₂ p q x y = f x y := rfl

Evaluation of Bilinear Map Restriction in Both Arguments

Informal description

Given a bilinear map $f \colon M \to N \to P$ that is semilinear in both arguments with respect to ring homomorphisms $\rho_{12} \colon R \to R_2$ and $\sigma_{12} \colon S \to S_2$, submodules $p \subseteq M$ and $q \subseteq N$, and elements $x \in p$ and $y \in q$, the restriction of $f$ to $p$ and $q$ satisfies $(f.domRestrict₁₂\,p\,q)\,x\,y = f\,x\,y$.

LinearMap.restrictScalars₁₂ definition

(B : M →ₗ[R] N →ₗ[S] Pₗ) : M →ₗ[R'] N →ₗ[S'] Pₗ

Full source

/-- If `B : M → N → Pₗ` is `R`-`S` bilinear and `R'` and `S'` are compatible scalar multiplications,
then the restriction of scalars is a `R'`-`S'` bilinear map. -/
@[simps!]
def restrictScalars₁₂ (B : M →ₗ[R] N →ₗ[S] Pₗ) : M →ₗ[R'] N →ₗ[S'] Pₗ :=
  LinearMap.mk₂' R' S'
    (B · ·)
    B.map_add₂
    (fun r' m _ ↦ by
      dsimp only
      rw [← smul_one_smul R r' m, map_smul₂, smul_one_smul])
    (fun _ ↦ map_add _)
    (fun _ x ↦ (B x).map_smul_of_tower _)

Restriction of scalars for a bilinear map

Informal description

Given a bilinear map $ B \colon M \to_R N \to_S P $ and compatible scalar multiplications $ R' $ and $ S' $, the function `LinearMap.restrictScalars₁₂` restricts the scalars of $ B $ to produce a new bilinear map $ M \to_{R'} N \to_{S'} P $. This means that the resulting map is linear in both arguments with respect to the new scalar rings $ R' $ and $ S' $, while preserving the original bilinear structure of $ B $.

LinearMap.restrictScalars₁₂_injective theorem

 : Function.Injective (LinearMap.restrictScalars₁₂ R' S' : (M →ₗ[R] N →ₗ[S] Pₗ) → (M →ₗ[R'] N →ₗ[S'] Pₗ))

Full source

theorem restrictScalars₁₂_injective : Function.Injective
    (LinearMap.restrictScalars₁₂ R' S' : (M →ₗ[R] N →ₗ[S] Pₗ) → (M →ₗ[R'] N →ₗ[S'] Pₗ)) :=
  fun _ _ h ↦ ext₂ (congr_fun₂ h :)

Injectivity of Scalar Restriction for Bilinear Maps

Informal description

The function `LinearMap.restrictScalars₁₂ R' S'` that restricts the scalars of a bilinear map from $R$ and $S$ to $R'$ and $S'$ is injective. That is, for any two bilinear maps $B, B' \colon M \to_R N \to_S P$, if $B.\text{restrictScalars₁₂}\,R'\,S' = B'.\text{restrictScalars₁₂}\,R'\,S'$, then $B = B'$.

LinearMap.restrictScalars₁₂_inj theorem

{B B' : M →ₗ[R] N →ₗ[S] Pₗ} : B.restrictScalars₁₂ R' S' = B'.restrictScalars₁₂ R' S' ↔ B = B'

Full source

@[simp]
theorem restrictScalars₁₂_inj {B B' : M →ₗ[R] N →ₗ[S] Pₗ} :
    B.restrictScalars₁₂ R' S' = B'.restrictScalars₁₂ R' S' ↔ B = B' :=
  (restrictScalars₁₂_injective R' S').eq_iff

Equality of Bilinear Maps Under Scalar Restriction: $ B = B' \leftrightarrow B|_{R',S'} = B'|_{R',S'} $

Informal description

For any two bilinear maps $ B, B' \colon M \to_R N \to_S P $, the restriction of scalars to $ R' $ and $ S' $ yields equal maps if and only if the original maps are equal, i.e., \[ B.\text{restrictScalars₁₂}\,R'\,S' = B'.\text{restrictScalars₁₂}\,R'\,S' \leftrightarrow B = B'. \]

LinearMap.mk₂ definition

 (f : M → Nₗ → Pₗ) (H1 : ∀ m₁ m₂ n, f (m₁ + m₂) n = f m₁ n + f m₂ n) (H2 : ∀ (c : R) (m n), f (c • m) n = c • f m n)
  (H3 : ∀ m n₁ n₂, f m (n₁ + n₂) = f m n₁ + f m n₂) (H4 : ∀ (c : R) (m n), f m (c • n) = c • f m n) :
  M →ₗ[R] Nₗ →ₗ[R] Pₗ

Full source

/-- Create a bilinear map from a function that is linear in each component.

This is a shorthand for `mk₂'` for the common case when `R = S`. -/
def mk₂ (f : M → Nₗ → Pₗ) (H1 : ∀ m₁ m₂ n, f (m₁ + m₂) n = f m₁ n + f m₂ n)
    (H2 : ∀ (c : R) (m n), f (c • m) n = c • f m n)
    (H3 : ∀ m n₁ n₂, f m (n₁ + n₂) = f m n₁ + f m n₂)
    (H4 : ∀ (c : R) (m n), f m (c • n) = c • f m n) : M →ₗ[R] Nₗ →ₗ[R] Pₗ :=
  mk₂' R R f H1 H2 H3 H4

Constructor for bilinear maps (equal base ring case)

Informal description

Given a function $ f : M \to N \to P $ that is linear in each component when $ R = S $, the constructor `LinearMap.mk₂` creates a bilinear map $ M \to_{R} N \to_{R} P $. Specifically, for $ f $ to be bilinear, it must satisfy the following properties: 1. Additivity in the first argument: $ f(m_1 + m_2, n) = f(m_1, n) + f(m_2, n) $ for all $ m_1, m_2 \in M $ and $ n \in N $. 2. Linearity in the first argument: $ f(c \cdot m, n) = c \cdot f(m, n) $ for all $ c \in R $, $ m \in M $, and $ n \in N $. 3. Additivity in the second argument: $ f(m, n_1 + n_2) = f(m, n_1) + f(m, n_2) $ for all $ m \in M $ and $ n_1, n_2 \in N $. 4. Linearity in the second argument: $ f(m, c \cdot n) = c \cdot f(m, n) $ for all $ c \in R $, $ m \in M $, and $ n \in N $. Here, $ R $ is the ring over which $ M $, $ N $, and $ P $ are modules.

LinearMap.mk₂_apply theorem

 (f : M → Nₗ → Pₗ) {H1 H2 H3 H4} (m : M) (n : Nₗ) : (mk₂ R f H1 H2 H3 H4 : M →ₗ[R] Nₗ →ₗ[R] Pₗ) m n = f m n

Full source

@[simp]
theorem mk₂_apply (f : M → Nₗ → Pₗ) {H1 H2 H3 H4} (m : M) (n : Nₗ) :
    (mk₂ R f H1 H2 H3 H4 : M →ₗ[R] Nₗ →ₗ[R] Pₗ) m n = f m n := rfl

Evaluation of Constructed Bilinear Map: $(mk₂_R f)(m)(n) = f(m)(n)$

Informal description

Let $M$, $N$, and $P$ be modules over a ring $R$, and let $f : M \to N \to P$ be a function that is bilinear (i.e., linear in each argument). Then for any $m \in M$ and $n \in N$, the bilinear map constructed via `LinearMap.mk₂ R f` satisfies $(mk₂_R f)(m)(n) = f(m)(n)$.

LinearMap.lflip definition

: (M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) →ₗ[R₃] N →ₛₗ[σ₂₃] M →ₛₗ[σ₁₃] P

Full source

/-- Given a linear map from `M` to linear maps from `N` to `P`, i.e., a bilinear map `M → N → P`,
change the order of variables and get a linear map from `N` to linear maps from `M` to `P`. -/
def lflip : (M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) →ₗ[R₃] N →ₛₗ[σ₂₃] M →ₛₗ[σ₁₃] P where
  toFun := flip
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

Linear flip of a bilinear map

Informal description

Given a bilinear map $ f \colon M \to_{[\sigma_{13}]} N \to_{[\sigma_{23}]} P $ that is semilinear in both arguments, the function `LinearMap.lflip` swaps the order of the arguments and produces a linear map from $ N $ to the space of linear maps from $ M $ to $ P $. Specifically, for any $ m \in M $ and $ n \in N $, the flipped map satisfies $ (f.lflip)(n)(m) = f(m)(n) $.

LinearMap.lflip_apply theorem

(m : M) (n : N) : lflip f n m = f m n

Full source

@[simp]
theorem lflip_apply (m : M) (n : N) : lflip f n m = f m n := rfl

Flip Application Identity for Bilinear Maps: $\operatorname{lflip}(f)(n)(m) = f(m)(n)$

Informal description

For any bilinear map $f \colon M \to N \to P$ and elements $m \in M$, $n \in N$, the flipped map $\operatorname{lflip}(f)$ satisfies $\operatorname{lflip}(f)(n)(m) = f(m)(n)$.

LinearMap.lcomp definition

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

Full source

/-- Composing a given linear map `M → N` with a linear map `N → P` as a linear map from
`Nₗ →ₗ[R] Pₗ` to `M →ₗ[R] Pₗ`. -/
def lcomp (f : M →ₗ[R] Nₗ) : (Nₗ →ₗ[R] Pₗ) →ₗ[R] M →ₗ[R] Pₗ :=
  flip <| LinearMap.comp (flip id) f

Precomposition with a linear map

Informal description

Given a linear map $f \colon M \to_{[R]} N$, the function `LinearMap.lcomp` constructs a linear map from the space of linear maps $N \to_{[R]} P$ to the space of linear maps $M \to_{[R]} P$ by precomposition with $f$. Specifically, for any linear map $g \colon N \to_{[R]} P$, the composition $g \circ f$ is a linear map from $M$ to $P$.

LinearMap.lcomp_apply theorem

(f : M →ₗ[R] Nₗ) (g : Nₗ →ₗ[R] Pₗ) (x : M) : lcomp _ _ f g x = g (f x)

Full source

@[simp]
theorem lcomp_apply (f : M →ₗ[R] Nₗ) (g : Nₗ →ₗ[R] Pₗ) (x : M) : lcomp _ _ f g x = g (f x) := rfl

Evaluation of Linear Map Composition: $(g \circ f)(x) = g(f(x))$

Informal description

For any linear maps $f \colon M \to_{[R]} N$ and $g \colon N \to_{[R]} P$, and any element $x \in M$, the evaluation of the composition $g \circ f$ at $x$ equals $g(f(x))$, i.e., $(g \circ f)(x) = g(f(x))$.

LinearMap.lcomp_apply' theorem

(f : M →ₗ[R] Nₗ) (g : Nₗ →ₗ[R] Pₗ) : lcomp R Pₗ f g = g ∘ₗ f

Full source

theorem lcomp_apply' (f : M →ₗ[R] Nₗ) (g : Nₗ →ₗ[R] Pₗ) : lcomp R Pₗ f g = g ∘ₗ f := rfl

Composition of Linear Maps via `lcomp`

Informal description

For any linear maps $f \colon M \to_{[R]} N$ and $g \colon N \to_{[R]} P$, the composition of linear maps `lcomp R P f g` is equal to the linear composition $g \circ f$.

LinearMap.lcompₛₗ definition

(f : M →ₛₗ[σ₁₂] N) : (N →ₛₗ[σ₂₃] P) →ₗ[R₃] M →ₛₗ[σ₁₃] P

Full source

/-- Composing a semilinear map `M → N` and a semilinear map `N → P` to form a semilinear map
`M → P` is itself a linear map. -/
def lcompₛₗ (f : M →ₛₗ[σ₁₂] N) : (N →ₛₗ[σ₂₃] P) →ₗ[R₃] M →ₛₗ[σ₁₃] P :=
  flip <| LinearMap.comp (flip id) f

Linear composition of semilinear maps

Informal description

Given a semilinear map $f \colon M \to_{[\sigma_{12}]} N$, the function `LinearMap.lcompₛₗ` constructs a linear map that takes a semilinear map $g \colon N \to_{[\sigma_{23}]} P$ and returns the composition $g \circ f \colon M \to_{[\sigma_{13}]} P$. Here, $\sigma_{12} \colon R \to R_2$, $\sigma_{23} \colon R_2 \to R_3$, and $\sigma_{13} \colon R \to R_3$ are ring homomorphisms, and the composition is performed in a way that respects the semilinearity in both arguments.

LinearMap.lcompₛₗ_apply theorem

(f : M →ₛₗ[σ₁₂] N) (g : N →ₛₗ[σ₂₃] P) (x : M) : lcompₛₗ P σ₂₃ f g x = g (f x)

Full source

@[simp]
theorem lcompₛₗ_apply (f : M →ₛₗ[σ₁₂] N) (g : N →ₛₗ[σ₂₃] P) (x : M) :
    lcompₛₗ P σ₂₃ f g x = g (f x) := rfl

Evaluation of Semilinear Map Composition: $(g \circ f)(x) = g(f(x))$

Informal description

Given semilinear maps $f \colon M \to_{[\sigma_{12}]} N$ and $g \colon N \to_{[\sigma_{23}]} P$, and an element $x \in M$, the evaluation of the composition `lcompₛₗ P σ₂₃ f g` at $x$ equals $g(f(x))$.

LinearMap.llcomp definition

: (Nₗ →ₗ[R] Pₗ) →ₗ[R] (M →ₗ[R] Nₗ) →ₗ[R] M →ₗ[R] Pₗ

Full source

/-- Composing linear maps as a bilinear map from `(M →ₗ[R] N) × (N →ₗ[R] P)` to `M →ₗ[R] P` -/
def llcomp : (Nₗ →ₗ[R] Pₗ) →ₗ[R] (M →ₗ[R] Nₗ) →ₗ[R] M →ₗ[R] Pₗ :=
  flip
    { toFun := lcomp R Pₗ
      map_add' := fun _f _f' => ext₂ fun g _x => g.map_add _ _
      map_smul' := fun (_c : R) _f => ext₂ fun g _x => g.map_smul _ _ }

Bilinear composition of linear maps

Informal description

The function `LinearMap.llcomp` constructs a bilinear map that takes two linear maps $f \colon N \to_{[R]} P$ and $g \colon M \to_{[R]} N$ and returns their composition $f \circ g \colon M \to_{[R]} P$. This operation is linear in both arguments, meaning it preserves addition and scalar multiplication in each argument separately.

LinearMap.llcomp_apply theorem

(f : Nₗ →ₗ[R] Pₗ) (g : M →ₗ[R] Nₗ) (x : M) : llcomp R M Nₗ Pₗ f g x = f (g x)

Full source

@[simp]
theorem llcomp_apply (f : Nₗ →ₗ[R] Pₗ) (g : M →ₗ[R] Nₗ) (x : M) :
    llcomp R M Nₗ Pₗ f g x = f (g x) := rfl

Evaluation of Bilinear Composition: $(f \circ g)(x) = f(g(x))$

Informal description

For any linear maps $f \colon N \to_{[R]} P$ and $g \colon M \to_{[R]} N$, and any element $x \in M$, the evaluation of the bilinear composition $\text{llcomp}_R(M,N,P)(f,g)$ at $x$ equals $f(g(x))$.

LinearMap.llcomp_apply' theorem

(f : Nₗ →ₗ[R] Pₗ) (g : M →ₗ[R] Nₗ) : llcomp R M Nₗ Pₗ f g = f ∘ₗ g

Full source

theorem llcomp_apply' (f : Nₗ →ₗ[R] Pₗ) (g : M →ₗ[R] Nₗ) : llcomp R M Nₗ Pₗ f g = f ∘ₗ g := rfl

Bilinear Composition as Linear Map Composition: $\text{llcomp}_R M N P f g = f \circ g$

Informal description

For any linear maps $f \colon N \to_{[R]} P$ and $g \colon M \to_{[R]} N$, the bilinear composition map `llcomp` satisfies $\text{llcomp}_R M N P f g = f \circ g$, where $\circ$ denotes the composition of linear maps.

LinearMap.compl₂ definition

 {R₅ : Type*} [CommSemiring R₅] [Module R₅ P] [SMulCommClass R₃ R₅ P] {σ₁₅ : R →+* R₅} (h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P)
  (g : Q →ₛₗ[σ₄₂] N) : M →ₛₗ[σ₁₅] Q →ₛₗ[σ₄₃] P

Full source

/-- Composing a linear map `Q → N` and a bilinear map `M → N → P` to
form a bilinear map `M → Q → P`. -/
def compl₂ {R₅ : Type*} [CommSemiring R₅] [Module R₅ P] [SMulCommClass R₃ R₅ P] {σ₁₅ : R →+* R₅}
    (h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P) (g : Q →ₛₗ[σ₄₂] N) : M →ₛₗ[σ₁₅] Q →ₛₗ[σ₄₃] P where
  toFun a := (lcompₛₗ P σ₂₃ g) (h a)
  map_add' _ _ := by
    simp [map_add]
  map_smul' _ _ := by
    simp only [LinearMap.map_smulₛₗ, lcompₛₗ]
    rfl

Composition of a bilinear map with a linear map in the second argument

Informal description

Given a bilinear map $h \colon M \to_{[\sigma_{15}]} N \to_{[\sigma_{23}]} P$ and a linear map $g \colon Q \to_{[\sigma_{42}]} N$, the function `LinearMap.compl₂` constructs a bilinear map $M \to_{[\sigma_{15}]} Q \to_{[\sigma_{43}]} P$ defined by $(h \circ g)(m, q) = h(m, g(q))$ for all $m \in M$ and $q \in Q$. Here, $\sigma_{15} \colon R \to R_5$, $\sigma_{23} \colon R_2 \to R_3$, and $\sigma_{42} \colon R_4 \to R_2$ are ring homomorphisms, and the resulting map is semilinear in both arguments with respect to $\sigma_{15}$ and $\sigma_{43}$.

LinearMap.compl₂_apply theorem

(g : Q →ₛₗ[σ₄₂] N) (m : M) (q : Q) : f.compl₂ g m q = f m (g q)

Full source

@[simp]
theorem compl₂_apply (g : Q →ₛₗ[σ₄₂] N) (m : M) (q : Q) : f.compl₂ g m q = f m (g q) := rfl

Application of Composition of Bilinear Map with Linear Map in Second Argument

Informal description

Given a bilinear map $f \colon M \to_{[\sigma_{15}]} N \to_{[\sigma_{23}]} P$, a linear map $g \colon Q \to_{[\sigma_{42}]} N$, an element $m \in M$, and an element $q \in Q$, the application of the composed bilinear map $f \circ g$ satisfies $(f \circ g)(m, q) = f(m, g(q))$.

LinearMap.compl₂_id theorem

: f.compl₂ LinearMap.id = f

Full source

@[simp]
theorem compl₂_id : f.compl₂ LinearMap.id = f := by
  ext
  rw [compl₂_apply, id_coe, _root_.id]

Identity Composition Property for Bilinear Maps in the Second Argument

Informal description

Given a bilinear map $f \colon M \to N \to P$, the composition of $f$ with the identity linear map $\text{id} \colon N \to N$ in the second argument yields $f$ itself, i.e., $f \circ \text{id} = f$.

LinearMap.compl₁₂ definition

 {R₁ : Type*} [CommSemiring R₁] [Module R₂ N] [Module R₂ Pₗ] [Module R₁ Pₗ] [Module R₁ Mₗ] [SMulCommClass R₂ R₁ Pₗ]
  [Module R₁ Qₗ] [Module R₂ Qₗ'] (f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ) (g : Qₗ →ₗ[R₁] Mₗ) (g' : Qₗ' →ₗ[R₂] N) :
  Qₗ →ₗ[R₁] Qₗ' →ₗ[R₂] Pₗ

Full source

/-- Composing linear maps `Q → M` and `Q' → N` with a bilinear map `M → N → P` to
form a bilinear map `Q → Q' → P`. -/
def compl₁₂ {R₁ : Type*} [CommSemiring R₁] [Module R₂ N] [Module R₂ Pₗ] [Module R₁ Pₗ]
    [Module R₁ Mₗ] [SMulCommClass R₂ R₁ Pₗ] [Module R₁ Qₗ] [Module R₂ Qₗ']
    (f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ) (g : Qₗ →ₗ[R₁] Mₗ) (g' : Qₗ' →ₗ[R₂] N) :
    Qₗ →ₗ[R₁] Qₗ' →ₗ[R₂] Pₗ :=
  (f.comp g).compl₂ g'

Composition of a bilinear map with linear maps in both arguments

Informal description

Given a bilinear map $f \colon M \to_{[R_1]} N \to_{[R_2]} P$ and linear maps $g \colon Q \to_{[R_1]} M$ and $g' \colon Q' \to_{[R_2]} N$, the function `LinearMap.compl₁₂` constructs a bilinear map $Q \to_{[R_1]} Q' \to_{[R_2]} P$ defined by $(f \circ (g, g'))(q, q') = f(g(q), g'(q'))$ for all $q \in Q$ and $q' \in Q'$. Here, $R_1$ and $R_2$ are commutative semirings, and the resulting map is linear in both arguments with respect to $R_1$ and $R_2$ respectively.

LinearMap.compl₁₂_apply theorem

 (f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Qₗ →ₗ[R] Mₗ) (g' : Qₗ' →ₗ[R] Nₗ) (x : Qₗ) (y : Qₗ') :
  f.compl₁₂ g g' x y = f (g x) (g' y)

Full source

@[simp]
theorem compl₁₂_apply (f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Qₗ →ₗ[R] Mₗ) (g' : Qₗ' →ₗ[R] Nₗ) (x : Qₗ)
    (y : Qₗ') : f.compl₁₂ g g' x y = f (g x) (g' y) := rfl

Evaluation of Composed Bilinear Map: $(f \circ (g, g'))(x, y) = f(g(x), g'(y))$

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, $Q$, and $Q'$ be modules over $R$. Given a bilinear map $f \colon M \to_{[R]} N \to_{[R]} P$ and linear maps $g \colon Q \to_{[R]} M$ and $g' \colon Q' \to_{[R]} N$, then for any $x \in Q$ and $y \in Q'$, the evaluation of the composed bilinear map $f \circ (g, g')$ at $(x, y)$ satisfies $(f \circ (g, g'))(x, y) = f(g(x), g'(y))$.

LinearMap.compl₁₂_id_id theorem

(f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ) : f.compl₁₂ LinearMap.id LinearMap.id = f

Full source

@[simp]
theorem compl₁₂_id_id (f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ) : f.compl₁₂ LinearMap.id LinearMap.id = f := by
  ext
  simp_rw [compl₁₂_apply, id_coe, _root_.id]

Identity Composition Preserves Bilinear Map

Informal description

For any bilinear map $f \colon M \to_{[R]} N \to_{[R]} P$, the composition of $f$ with the identity maps on $M$ and $N$ yields $f$ itself, i.e., $f \circ (\text{id}_M, \text{id}_N) = f$.

LinearMap.compl₁₂_inj theorem

 {f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ} {g : Qₗ →ₗ[R] Mₗ} {g' : Qₗ' →ₗ[R] Nₗ} (hₗ : Function.Surjective g)
  (hᵣ : Function.Surjective g') : f₁.compl₁₂ g g' = f₂.compl₁₂ g g' ↔ f₁ = f₂

Full source

theorem compl₁₂_inj {f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ} {g : Qₗ →ₗ[R] Mₗ} {g' : Qₗ' →ₗ[R] Nₗ}
    (hₗ : Function.Surjective g) (hᵣ : Function.Surjective g') :
    f₁.compl₁₂ g g' = f₂.compl₁₂ g g' ↔ f₁ = f₂ := by
  constructor <;> intro h
  · -- B₁.comp l r = B₂.comp l r → B₁ = B₂
    ext x y
    obtain ⟨x', hx⟩ := hₗ x
    subst hx
    obtain ⟨y', hy⟩ := hᵣ y
    subst hy
    convert LinearMap.congr_fun₂ h x' y' using 0
  · -- B₁ = B₂ → B₁.comp l r = B₂.comp l r
    subst h; rfl

Injectivity of Bilinear Map Composition under Surjective Linear Maps

Informal description

Let $R$ be a commutative semiring, and let $M, N, P, Q, Q'$ be modules over $R$. Given two bilinear maps $f_1, f_2 \colon M \to_{[R]} N \to_{[R]} P$ and linear maps $g \colon Q \to_{[R]} M$, $g' \colon Q' \to_{[R]} N$ such that $g$ and $g'$ are surjective, then the composition maps $f_1 \circ (g, g')$ and $f_2 \circ (g, g')$ are equal if and only if $f_1 = f_2$.

LinearMap.compr₂ definition

(f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ) : M →ₗ[R] Nₗ →ₗ[R] Qₗ

Full source

/-- Composing a linear map `P → Q` and a bilinear map `M → N → P` to
form a bilinear map `M → N → Q`. -/
def compr₂ (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ) : M →ₗ[R] Nₗ →ₗ[R] Qₗ :=
  llcompllcomp R Nₗ Pₗ Qₗ g ∘ₗ f

Composition of a bilinear map with a linear map

Informal description

Given a bilinear map $ f \colon M \to_{[R]} N \to_{[R]} P $ and a linear map $ g \colon P \to_{[R]} Q $, the function `LinearMap.compr₂` constructs a new bilinear map $ M \to_{[R]} N \to_{[R]} Q $ by composing $ f $ with $ g $. Specifically, for any $ m \in M $ and $ n \in N $, the resulting map is given by $ g(f(m, n)) $.

LinearMap.compr₂_apply theorem

(f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ) (m : M) (n : Nₗ) : f.compr₂ g m n = g (f m n)

Full source

@[simp]
theorem compr₂_apply (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ) (m : M) (n : Nₗ) :
    f.compr₂ g m n = g (f m n) := rfl

Evaluation of Composition of Bilinear Map with Linear Map: $(f \circ g)(m, n) = g(f(m, n))$

Informal description

Let $R$ be a commutative ring, and let $M$, $N_\ell$, $P_\ell$, $Q_\ell$ be $R$-modules. Given a bilinear map $f \colon M \to_L N_\ell \to_L P_\ell$ and a linear map $g \colon P_\ell \to_L Q_\ell$, the composition $f \circ g$ evaluated at $(m, n) \in M \times N_\ell$ satisfies $(f \circ g)(m, n) = g(f(m, n))$.

LinearMap.injective_compr₂_of_injective theorem

 (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ) (hf : Injective f) (hg : Injective g) : Injective (f.compr₂ g)

Full source

/-- A version of `Function.Injective.comp` for composition of a bilinear map with a linear map. -/
theorem injective_compr₂_of_injective (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ) (hf : Injective f)
    (hg : Injective g) : Injective (f.compr₂ g) :=
  hg.injective_linearMapComp_left.comp hf

Injectivity of Composition of Bilinear and Linear Maps

Informal description

Let $R$ be a commutative ring, and let $M$, $N$, $P$, and $Q$ be $R$-modules. Given a bilinear map $f \colon M \to N \to P$ and a linear map $g \colon P \to Q$, if both $f$ and $g$ are injective, then the composition $f \circ g \colon M \to N \to Q$ is also injective.

LinearMap.surjective_compr₂_of_exists_rightInverse theorem

 (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ) (hf : Surjective f) (hg : ∃ g' : Qₗ →ₗ[R] Pₗ, g.comp g' = LinearMap.id) :
  Surjective (f.compr₂ g)

Full source

/-- A version of `Function.Surjective.comp` for composition of a bilinear map with a linear map. -/
theorem surjective_compr₂_of_exists_rightInverse (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ)
    (hf : Surjective f) (hg : ∃ g' : Qₗ →ₗ[R] Pₗ, g.comp g' = LinearMap.id) :
    Surjective (f.compr₂ g) := (surjective_comp_left_of_exists_rightInverse hg).comp hf

Surjectivity of Bilinear-Linear Composition with Right Inverse

Informal description

Let $R$ be a commutative ring, and let $M$, $N_\ell$, $P_\ell$, and $Q_\ell$ be $R$-modules. Given a bilinear map $f \colon M \to_{[R]} N_\ell \to_{[R]} P_\ell$ and a linear map $g \colon P_\ell \to_{[R]} Q_\ell$, if $f$ is surjective and there exists a right inverse $g' \colon Q_\ell \to_{[R]} P_\ell$ of $g$ (i.e., $g \circ g' = \text{id}$), then the composition $f \circ g \colon M \to_{[R]} N_\ell \to_{[R]} Q_\ell$ is also surjective.

LinearMap.surjective_compr₂_of_equiv theorem

 (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ ≃ₗ[R] Qₗ) (hf : Surjective f) : Surjective (f.compr₂ g.toLinearMap)

Full source

/-- A version of `Function.Surjective.comp` for composition of a bilinear map with a linear map. -/
theorem surjective_compr₂_of_equiv (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ ≃ₗ[R] Qₗ) (hf : Surjective f) :
    Surjective (f.compr₂ g.toLinearMap) :=
  surjective_compr₂_of_exists_rightInverse f g.toLinearMap hf ⟨g.symm, by simp⟩

Surjectivity of Bilinear-Linear Composition with Linear Equivalence

Informal description

Let $R$ be a commutative ring, and let $M$, $N_\ell$, $P_\ell$, and $Q_\ell$ be $R$-modules. Given a bilinear map $f \colon M \to N_\ell \to P_\ell$ and a linear equivalence $g \colon P_\ell \simeq Q_\ell$, if $f$ is surjective, then the composition $f \circ g \colon M \to N_\ell \to Q_\ell$ is also surjective.

LinearMap.bijective_compr₂_of_equiv theorem

 (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ ≃ₗ[R] Qₗ) (hf : Bijective f) : Bijective (f.compr₂ g.toLinearMap)

Full source

/-- A version of `Function.Bijective.comp` for composition of a bilinear map with a linear map. -/
theorem bijective_compr₂_of_equiv (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ ≃ₗ[R] Qₗ) (hf : Bijective f) :
    Bijective (f.compr₂ g.toLinearMap) :=
  ⟨injective_compr₂_of_injective f g.toLinearMap hf.1 g.bijective.1,
  surjective_compr₂_of_equiv f g hf.2⟩

Bijectivity of Bilinear-Linear Composition with Linear Equivalence

Informal description

Let $R$ be a commutative ring, and let $M$, $N$, $P$, and $Q$ be $R$-modules. Given a bilinear map $f \colon M \to N \to P$ and a linear equivalence $g \colon P \simeq Q$, if $f$ is bijective, then the composition $f \circ g \colon M \to N \to Q$ is also bijective.

LinearMap.lsmul definition

: R →ₗ[R] M →ₗ[R] M

Full source

/-- Scalar multiplication as a bilinear map `R → M → M`. -/
def lsmul : R →ₗ[R] M →ₗ[R] M :=
  mk₂ R (· • ·) add_smul (fun _ _ _ => mul_smul _ _ _) smul_add fun r s m => by
    simp only [smul_smul, smul_eq_mul, mul_comm]

Scalar multiplication as a bilinear map

Informal description

The scalar multiplication operation $ (r, m) \mapsto r \cdot m $ as a bilinear map $ R \to M \to M $, where $ R $ is a ring and $ M $ is an $ R $-module. This map is linear in both arguments, satisfying: 1. Additivity in the first argument: $ (r_1 + r_2) \cdot m = r_1 \cdot m + r_2 \cdot m $ 2. Linearity in the first argument: $ (c \cdot r) \cdot m = c \cdot (r \cdot m) $ for any scalar $ c \in R $ 3. Additivity in the second argument: $ r \cdot (m_1 + m_2) = r \cdot m_1 + r \cdot m_2 $ 4. Linearity in the second argument: $ r \cdot (c \cdot m) = c \cdot (r \cdot m) $ for any scalar $ c \in R $

LinearMap.lsmul_eq_DistribMulAction_toLinearMap theorem

(r : R) : lsmul R M r = DistribMulAction.toLinearMap R M r

Full source

lemma lsmul_eq_DistribMulAction_toLinearMap (r : R) :
    lsmul R M r = DistribMulAction.toLinearMap R M r := rfl

Equality of Left Scalar Multiplication and Distributive Action Linear Maps

Informal description

For any element $r$ in the ring $R$, the linear map $\text{lsmul}_R M r$ (left scalar multiplication by $r$ on the $R$-module $M$) is equal to the linear map $\text{DistribMulAction.toLinearMap}_R M r$ (the linear map induced by the distributive multiplicative action of $R$ on $M$).

LinearMap.lsmul_apply theorem

(r : R) (m : M) : lsmul R M r m = r • m

Full source

@[simp]
theorem lsmul_apply (r : R) (m : M) : lsmul R M r m = r • m := rfl

Scalar Multiplication Identity: $\text{lsmul}_R^M(r)(m) = r \cdot m$

Informal description

For any scalar $r$ in a ring $R$ and any element $m$ in an $R$-module $M$, the application of the scalar multiplication bilinear map $\text{lsmul}_R^M$ to $r$ and $m$ equals the scalar multiplication $r \cdot m$.

LinearMap.BilinMap abbrev

: Type _

Full source

/-- A shorthand for the type of `R`-bilinear `Nₗ`-valued maps on `M`. -/
protected abbrev BilinMap : Type _ := M →ₗ[R] M →ₗ[R] Nₗ

Type of Bilinear Maps Between Modules

Informal description

The type of $R$-bilinear maps from $M$ to $N$, where $M$ and $N$ are modules over a commutative ring $R$. A bilinear map is a function $f: M \times M \to N$ that is linear in each argument separately.

LinearMap.BilinForm abbrev

: Type _

Full source

/-- For convenience, a shorthand for the type of bilinear forms from `M` to `R`. -/
protected abbrev BilinForm : Type _ := LinearMap.BilinMap R M R

Type of Bilinear Forms on a Module

Informal description

The type of bilinear forms from a module $M$ over a commutative ring $R$ to $R$ itself. A bilinear form is a function $B: M \times M \to R$ that is linear in each argument separately.

LinearMap.lsmul_injective theorem

[NoZeroSMulDivisors R M] {x : R} (hx : x ≠ 0) : Function.Injective (lsmul R M x)

Full source

theorem lsmul_injective [NoZeroSMulDivisors R M] {x : R} (hx : x ≠ 0) :
    Function.Injective (lsmul R M x) :=
  smul_right_injective _ hx

Injectivity of Scalar Multiplication by Nonzero Elements

Informal description

Let $R$ be a ring and $M$ an $R$-module with no zero scalar divisors. For any nonzero element $x \in R$, the scalar multiplication map $m \mapsto x \cdot m$ is injective.

LinearMap.ker_lsmul theorem

[NoZeroSMulDivisors R M] {a : R} (ha : a ≠ 0) : LinearMap.ker (LinearMap.lsmul R M a) = ⊥

Full source

theorem ker_lsmul [NoZeroSMulDivisors R M] {a : R} (ha : a ≠ 0) :
    LinearMap.ker (LinearMap.lsmul R M a) = ⊥ :=
  LinearMap.ker_eq_bot_of_injective (LinearMap.lsmul_injective ha)

Trivial Kernel of Scalar Multiplication by Nonzero Elements

Informal description

Let $R$ be a ring and $M$ an $R$-module with no zero scalar divisors. For any nonzero element $a \in R$, the kernel of the scalar multiplication map $m \mapsto a \cdot m$ is trivial, i.e., $\ker(a \cdot) = \{0\}$.

LinearMap.restrictScalarsRange definition

: M' →ₗ[S] P'

Full source

/-- Restrict the scalars and range of a linear map. -/
noncomputable def restrictScalarsRange :
    M' →ₗ[S] P' :=
  ((f.restrictScalars S).comp i).codLift k hk hf

Restriction of scalars and range of a linear map

Informal description

Given a linear map `f : M →ₗ[R] P` and module homomorphisms `i : M' →ₗ[S] M` and `k : P →ₗ[S] P'` such that `k` is surjective and `f` maps the range of `i` into the kernel of `k`, the function constructs a linear map from `M'` to `P'` by first restricting scalars of `f` to `S`, composing with `i`, and then lifting through `k`.

LinearMap.restrictScalarsRange_apply theorem

(m : M') : k (restrictScalarsRange i k hk f hf m) = f (i m)

Full source

@[simp]
lemma restrictScalarsRange_apply (m : M') :
    k (restrictScalarsRange i k hk f hf m) = f (i m) := by
  have : k (restrictScalarsRange i k hk f hf m) =
      (k ∘ₗ ((f.restrictScalars S).comp i).codLift k hk hf) m :=
    rfl
  rw [this, comp_codLift, comp_apply, restrictScalars_apply]

Commutativity of Restriction of Scalars and Range with Composition: $k \circ \text{restrictScalarsRange}(i, k, hk, f, hf)(m) = f \circ i(m)$

Informal description

For any element $m \in M'$, the image of $m$ under the linear map $\text{restrictScalarsRange}(i, k, hk, f, hf)$ composed with $k$ equals the image of $i(m)$ under $f$, i.e., $k(\text{restrictScalarsRange}(i, k, hk, f, hf)(m)) = f(i(m))$.

LinearMap.restrictScalarsRange_apply_eq_zero_iff theorem

(m : M') : restrictScalarsRange i k hk f hf m = 0 ↔ f (i m) = 0

Full source

@[simp]
lemma restrictScalarsRange_apply_eq_zero_iff (m : M') :
    restrictScalarsRangerestrictScalarsRange i k hk f hf m = 0 ↔ f (i m) = 0 := by
  rw [← hk.eq_iff, restrictScalarsRange_apply, map_zero]

Zero Criterion for Restricted Scalar Range Map: $\text{restrictScalarsRange}(i, k, hk, f, hf)(m) = 0 \leftrightarrow f(i(m)) = 0$

Informal description

For any element $m \in M'$, the linear map $\text{restrictScalarsRange}(i, k, hk, f, hf)$ evaluated at $m$ is zero if and only if the linear map $f$ evaluated at $i(m)$ is zero, i.e., $\text{restrictScalarsRange}(i, k, hk, f, hf)(m) = 0 \leftrightarrow f(i(m)) = 0$.

LinearMap.restrictScalarsRange₂ definition

: M' →ₗ[S] N' →ₗ[S] P'

Full source

/-- Restrict the scalars, domains, and range of a bilinear map. -/
noncomputable def restrictScalarsRange₂ :
    M' →ₗ[S] N' →ₗ[S] P' :=
  (((LinearMap.restrictScalarsₗ S R _ _ _).comp
    (B.restrictScalars S)).compl₁₂ i j).codRestrict₂ k hk hB

Bilinear map with restricted scalar range

Informal description

Given modules $M'$, $N'$, and $P'$ over a semiring $S$, and a bilinear map $B \colon M \to_{[R]} N \to_{[R]} P$ over another semiring $R$, the function `LinearMap.restrictScalarsRange₂` constructs a bilinear map $M' \to_{[S]} N' \to_{[S]} P'$ by restricting the scalars of the range of $B$ to $S$. This is achieved by composing $B$ with linear maps $i \colon M' \to_{[S]} M$ and $j \colon N' \to_{[S]} N$, and then restricting the codomain to $P'$ via a linear map $k \colon P \to_{[S]} P'$ that preserves the scalar action.

LinearMap.restrictScalarsRange₂_apply theorem

(m : M') (n : N') : k (restrictScalarsRange₂ i j k hk B hB m n) = B (i m) (j n)

Full source

@[simp] lemma restrictScalarsRange₂_apply (m : M') (n : N') :
    k (restrictScalarsRange₂ i j k hk B hB m n) = B (i m) (j n) := by
  simp [restrictScalarsRange₂]

Compatibility of Restricted Scalar Range Bilinear Map with Original Bilinear Map

Informal description

For any elements $m \in M'$ and $n \in N'$, the image of $(m, n)$ under the bilinear map $\text{restrictScalarsRange₂}(i, j, k, hk, B, hB)$ composed with $k$ equals the image of $(i(m), j(n))$ under the original bilinear map $B$, i.e., $$ k(\text{restrictScalarsRange₂}(i, j, k, hk, B, hB)(m, n)) = B(i(m), j(n)). $$

LinearMap.restrictScalarsRange₂_apply_eq_zero_iff theorem

(m : M') (n : N') : restrictScalarsRange₂ i j k hk B hB m n = 0 ↔ B (i m) (j n) = 0

Full source

@[simp]
lemma restrictScalarsRange₂_apply_eq_zero_iff (m : M') (n : N') :
    restrictScalarsRange₂restrictScalarsRange₂ i j k hk B hB m n = 0 ↔ B (i m) (j n) = 0 := by
  rw [← hk.eq_iff, restrictScalarsRange₂_apply, map_zero]

Zero Criterion for Restricted Scalar Range Bilinear Map

Informal description

For any elements $m \in M'$ and $n \in N'$, the bilinear map $\text{restrictScalarsRange₂}(i, j, k, hk, B, hB)$ evaluated at $(m, n)$ equals zero if and only if the original bilinear map $B$ evaluated at $(i(m), j(n))$ equals zero. That is, $$\text{restrictScalarsRange₂}(i, j, k, hk, B, hB)(m, n) = 0 \leftrightarrow B(i(m), j(n)) = 0.$$

Mathlib.LinearAlgebra.BilinearMap

Main declarations

Tags