Documentation

Mathlib.LinearAlgebra.BilinearMap

Basics on bilinear maps #

This file provides basics on bilinear maps. The most general form considered are maps that are semilinear in both arguments. They are of type M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P, where M and N are modules over R and S respectively, P is a module over both R₂ and S₂ with commuting actions, and ρ₁₂ : R →+* R₂ and σ₁₂ : S →+* S₂.

Main declarations #

Tags #

bilinear

def LinearMap.mk₂'ₛₗ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] (ρ₁₂ : R →+* R₂) (σ₁₂ : S →+* S₂) (f : MNP) (H1 : ∀ (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n) (H2 : ∀ (c : R) (m : M) (n : N), f (c m) n = ρ₁₂ c f m n) (H3 : ∀ (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂) (H4 : ∀ (c : S) (m : M) (n : N), f m (c n) = σ₁₂ c f m n) :
M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P

Create a bilinear map from a function that is semilinear in each component. See mk₂' and mk₂ for the linear case.

Equations
  • LinearMap.mk₂'ₛₗ ρ₁₂ σ₁₂ f H1 H2 H3 H4 = { toFun := fun (m : M) => { toFun := f m, map_add' := , map_smul' := }, map_add' := , map_smul' := }
Instances For
    @[simp]
    theorem LinearMap.mk₂'ₛₗ_apply {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : MNP) {H1 : ∀ (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n} {H2 : ∀ (c : R) (m : M) (n : N), f (c m) n = ρ₁₂ c f m n} {H3 : ∀ (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂} {H4 : ∀ (c : S) (m : M) (n : N), f m (c n) = σ₁₂ c f m n} (m : M) (n : N) :
    ((LinearMap.mk₂'ₛₗ ρ₁₂ σ₁₂ f H1 H2 H3 H4) m) n = f m n
    def LinearMap.mk₂' (R : Type u_1) [Semiring R] (S : Type u_2) [Semiring S] {M : Type u_5} {N : Type u_6} {Pₗ : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid Pₗ] [Module R M] [Module S N] [Module R Pₗ] [Module S Pₗ] [SMulCommClass S R Pₗ] (f : MNPₗ) (H1 : ∀ (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n) (H2 : ∀ (c : R) (m : M) (n : N), f (c m) n = c f m n) (H3 : ∀ (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂) (H4 : ∀ (c : S) (m : M) (n : N), f m (c n) = c f m n) :
    M →ₗ[R] N →ₗ[S] Pₗ

    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.

    Equations
    Instances For
      @[simp]
      theorem LinearMap.mk₂'_apply {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {M : Type u_5} {N : Type u_6} {Pₗ : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid Pₗ] [Module R M] [Module S N] [Module R Pₗ] [Module S Pₗ] [SMulCommClass S R Pₗ] (f : MNPₗ) {H1 : ∀ (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n} {H2 : ∀ (c : R) (m : M) (n : N), f (c m) n = c f m n} {H3 : ∀ (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂} {H4 : ∀ (c : S) (m : M) (n : N), f m (c n) = c f m n} (m : M) (n : N) :
      ((LinearMap.mk₂' R S f H1 H2 H3 H4) m) n = f m n
      theorem LinearMap.ext₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} {f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} {g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (H : ∀ (m : M) (n : N), (f m) n = (g m) n) :
      f = g
      theorem LinearMap.congr_fun₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} {f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} {g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (h : f = g) (x : M) (y : N) :
      (f x) y = (g x) y
      theorem LinearMap.ext_iff₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} {f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} {g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} :
      f = g ∀ (m : M) (n : N), (f m) n = (g m) n
      def LinearMap.flip {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) :
      N →ₛₗ[σ₁₂] M →ₛₗ[ρ₁₂] P

      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.

      Equations
      Instances For
        @[simp]
        theorem LinearMap.flip_apply {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (m : M) (n : N) :
        (f.flip n) m = (f m) n
        @[simp]
        theorem LinearMap.flip_flip {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) :
        f.flip.flip = f
        theorem LinearMap.flip_inj {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} {f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} {g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (H : f.flip = g.flip) :
        f = g
        theorem LinearMap.map_zero₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (y : N) :
        (f 0) y = 0
        theorem LinearMap.map_neg₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {N : Type u_6} {M' : Type u_12} {P' : Type u_13} [AddCommMonoid N] [AddCommGroup M'] [AddCommGroup P'] [Module S N] [Module R M'] [Module R₂ P'] [Module S₂ P'] [SMulCommClass S₂ R₂ P'] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P') (x : M') (y : N) :
        (f (-x)) y = -(f x) y
        theorem LinearMap.map_sub₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {N : Type u_6} {M' : Type u_12} {P' : Type u_13} [AddCommMonoid N] [AddCommGroup M'] [AddCommGroup P'] [Module S N] [Module R M'] [Module R₂ P'] [Module S₂ P'] [SMulCommClass S₂ R₂ P'] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M' →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P') (x : M') (y : M') (z : N) :
        (f (x - y)) z = (f x) z - (f y) z
        theorem LinearMap.map_add₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (x₁ : M) (x₂ : M) (y : N) :
        (f (x₁ + x₂)) y = (f x₁) y + (f x₂) y
        theorem LinearMap.map_smul₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {S₂ : Type u_4} [Semiring S₂] {M₂ : Type u_8} {N₂ : Type u_9} {P₂ : Type u_10} [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid P₂] [Module R M₂] [Module S N₂] [Module R P₂] [Module S₂ P₂] [SMulCommClass S₂ R P₂] {σ₁₂ : S →+* S₂} (f : M₂ →ₗ[R] N₂ →ₛₗ[σ₁₂] P₂) (r : R) (x : M₂) (y : N₂) :
        (f (r x)) y = r (f x) y
        theorem LinearMap.map_smulₛₗ₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (r : R) (x : M) (y : N) :
        (f (r x)) y = ρ₁₂ r (f x) y
        theorem LinearMap.map_sum₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} {ι : Type u_14} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (t : Finset ι) (x : ιM) (y : N) :
        (f (∑ it, x i)) y = it, (f (x i)) y
        def LinearMap.domRestrict₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (q : Submodule S N) :
        M →ₛₗ[ρ₁₂] q →ₛₗ[σ₁₂] P

        Restricting a bilinear map in the second entry

        Equations
        • f.domRestrict₂ q = { toFun := fun (m : M) => (f m).domRestrict q, map_add' := , map_smul' := }
        Instances For
          theorem LinearMap.domRestrict₂_apply {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (q : Submodule S N) (x : M) (y : q) :
          ((f.domRestrict₂ q) x) y = (f x) y
          def LinearMap.domRestrict₁₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (p : Submodule R M) (q : Submodule S N) :
          p →ₛₗ[ρ₁₂] q →ₛₗ[σ₁₂] P

          Restricting a bilinear map in both components

          Equations
          • f.domRestrict₁₂ p q = (f.domRestrict p).domRestrict₂ q
          Instances For
            theorem LinearMap.domRestrict₁₂_apply {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {R₂ : Type u_3} [Semiring R₂] {S₂ : Type u_4} [Semiring S₂] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module S N] [Module R₂ P] [Module S₂ P] [SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (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
            @[simp]
            theorem LinearMap.restrictScalars₁₂_apply_apply {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {M : Type u_5} {N : Type u_6} {Pₗ : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid Pₗ] [Module R M] [Module S N] [Module R Pₗ] [Module S Pₗ] [SMulCommClass S R Pₗ] (R' : Type u_14) (S' : Type u_15) [Semiring R'] [Semiring S'] [Module R' M] [Module S' N] [Module R' Pₗ] [Module S' Pₗ] [SMulCommClass S' R' Pₗ] [SMul S' S] [IsScalarTower S' S N] [IsScalarTower S' S Pₗ] [SMul R' R] [IsScalarTower R' R M] [IsScalarTower R' R Pₗ] (B : M →ₗ[R] N →ₗ[S] Pₗ) (m : M) :
            ∀ (x2 : N), ((LinearMap.restrictScalars₁₂ R' S' B) m) x2 = (B m) x2
            def LinearMap.restrictScalars₁₂ {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {M : Type u_5} {N : Type u_6} {Pₗ : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid Pₗ] [Module R M] [Module S N] [Module R Pₗ] [Module S Pₗ] [SMulCommClass S R Pₗ] (R' : Type u_14) (S' : Type u_15) [Semiring R'] [Semiring S'] [Module R' M] [Module S' N] [Module R' Pₗ] [Module S' Pₗ] [SMulCommClass S' R' Pₗ] [SMul S' S] [IsScalarTower S' S N] [IsScalarTower S' S Pₗ] [SMul R' R] [IsScalarTower R' R M] [IsScalarTower R' R Pₗ] (B : M →ₗ[R] N →ₗ[S] Pₗ) :
            M →ₗ[R'] N →ₗ[S'] Pₗ

            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.

            Equations
            Instances For
              theorem LinearMap.restrictScalars₁₂_injective {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {M : Type u_5} {N : Type u_6} {Pₗ : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid Pₗ] [Module R M] [Module S N] [Module R Pₗ] [Module S Pₗ] [SMulCommClass S R Pₗ] (R' : Type u_14) (S' : Type u_15) [Semiring R'] [Semiring S'] [Module R' M] [Module S' N] [Module R' Pₗ] [Module S' Pₗ] [SMulCommClass S' R' Pₗ] [SMul S' S] [IsScalarTower S' S N] [IsScalarTower S' S Pₗ] [SMul R' R] [IsScalarTower R' R M] [IsScalarTower R' R Pₗ] :
              @[simp]
              theorem LinearMap.restrictScalars₁₂_inj {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] {M : Type u_5} {N : Type u_6} {Pₗ : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid Pₗ] [Module R M] [Module S N] [Module R Pₗ] [Module S Pₗ] [SMulCommClass S R Pₗ] (R' : Type u_14) (S' : Type u_15) [Semiring R'] [Semiring S'] [Module R' M] [Module S' N] [Module R' Pₗ] [Module S' Pₗ] [SMulCommClass S' R' Pₗ] [SMul S' S] [IsScalarTower S' S N] [IsScalarTower S' S Pₗ] [SMul R' R] [IsScalarTower R' R M] [IsScalarTower R' R Pₗ] {B : M →ₗ[R] N →ₗ[S] Pₗ} {B' : M →ₗ[R] N →ₗ[S] Pₗ} :
              def LinearMap.mk₂ (R : Type u_1) [CommSemiring R] {M : Type u_5} {Nₗ : Type u_10} {Pₗ : Type u_11} [AddCommMonoid M] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ] [Module R M] [Module R Nₗ] [Module R Pₗ] (f : MNₗPₗ) (H1 : ∀ (m₁ m₂ : M) (n : Nₗ), f (m₁ + m₂) n = f m₁ n + f m₂ n) (H2 : ∀ (c : R) (m : M) (n : Nₗ), f (c m) n = c f m n) (H3 : ∀ (m : M) (n₁ n₂ : Nₗ), f m (n₁ + n₂) = f m n₁ + f m n₂) (H4 : ∀ (c : R) (m : M) (n : Nₗ), f m (c n) = c f m n) :
              M →ₗ[R] Nₗ →ₗ[R] Pₗ

              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.

              Equations
              Instances For
                @[simp]
                theorem LinearMap.mk₂_apply (R : Type u_1) [CommSemiring R] {M : Type u_5} {Nₗ : Type u_10} {Pₗ : Type u_11} [AddCommMonoid M] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ] [Module R M] [Module R Nₗ] [Module R Pₗ] (f : MNₗPₗ) {H1 : ∀ (m₁ m₂ : M) (n : Nₗ), f (m₁ + m₂) n = f m₁ n + f m₂ n} {H2 : ∀ (c : R) (m : M) (n : Nₗ), f (c m) n = c f m n} {H3 : ∀ (m : M) (n₁ n₂ : Nₗ), f m (n₁ + n₂) = f m n₁ + f m n₂} {H4 : ∀ (c : R) (m : M) (n : Nₗ), f m (c n) = c f m n} (m : M) (n : Nₗ) :
                ((LinearMap.mk₂ R f H1 H2 H3 H4) m) n = f m n
                def LinearMap.lflip {R : Type u_1} [CommSemiring R] {R₂ : Type u_2} [CommSemiring R₂] {R₃ : Type u_3} [CommSemiring R₃] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R₂ N] [Module R₃ P] {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} :
                (M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) →ₗ[R₃] N →ₛₗ[σ₂₃] M →ₛₗ[σ₁₃] P

                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.

                Equations
                • LinearMap.lflip = { toFun := LinearMap.flip, map_add' := , map_smul' := }
                Instances For
                  @[simp]
                  theorem LinearMap.lflip_apply {R : Type u_1} [CommSemiring R] {R₂ : Type u_2} [CommSemiring R₂] {R₃ : Type u_3} [CommSemiring R₃] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R₂ N] [Module R₃ P] {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) (m : M) (n : N) :
                  ((LinearMap.lflip f) n) m = (f m) n
                  def LinearMap.lcomp (R : Type u_1) [CommSemiring R] {M : Type u_5} {Nₗ : Type u_10} (Pₗ : Type u_11) [AddCommMonoid M] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ] [Module R M] [Module R Nₗ] [Module R Pₗ] (f : M →ₗ[R] Nₗ) :
                  (Nₗ →ₗ[R] Pₗ) →ₗ[R] M →ₗ[R] Pₗ

                  Composing a linear map M → N and a linear map N → P to form a linear map M → P.

                  Equations
                  Instances For
                    @[simp]
                    theorem LinearMap.lcomp_apply {R : Type u_1} [CommSemiring R] {M : Type u_5} {Nₗ : Type u_10} {Pₗ : Type u_11} [AddCommMonoid M] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ] [Module R M] [Module R Nₗ] [Module R Pₗ] (f : M →ₗ[R] Nₗ) (g : Nₗ →ₗ[R] Pₗ) (x : M) :
                    ((LinearMap.lcomp R Pₗ f) g) x = g (f x)
                    theorem LinearMap.lcomp_apply' {R : Type u_1} [CommSemiring R] {M : Type u_5} {Nₗ : Type u_10} {Pₗ : Type u_11} [AddCommMonoid M] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ] [Module R M] [Module R Nₗ] [Module R Pₗ] (f : M →ₗ[R] Nₗ) (g : Nₗ →ₗ[R] Pₗ) :
                    (LinearMap.lcomp R Pₗ f) g = g ∘ₗ f
                    def LinearMap.lcompₛₗ {R : Type u_1} [CommSemiring R] {R₂ : Type u_2} [CommSemiring R₂] {R₃ : Type u_3} [CommSemiring R₃] {M : Type u_5} {N : Type u_6} (P : Type u_7) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R₂ N] [Module R₃ P] {σ₁₂ : R →+* R₂} (σ₂₃ : R₂ →+* R₃) {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] N) :
                    (N →ₛₗ[σ₂₃] P) →ₗ[R₃] M →ₛₗ[σ₁₃] P

                    Composing a semilinear map M → N and a semilinear map N → P to form a semilinear map M → P is itself a linear map.

                    Equations
                    Instances For
                      @[simp]
                      theorem LinearMap.lcompₛₗ_apply {R : Type u_1} [CommSemiring R] {R₂ : Type u_2} [CommSemiring R₂] {R₃ : Type u_3} [CommSemiring R₃] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R₂ N] [Module R₃ P] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] N) (g : N →ₛₗ[σ₂₃] P) (x : M) :
                      ((LinearMap.lcompₛₗ P σ₂₃ f) g) x = g (f x)
                      def LinearMap.llcomp (R : Type u_1) [CommSemiring R] (M : Type u_5) (Nₗ : Type u_10) (Pₗ : Type u_11) [AddCommMonoid M] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ] [Module R M] [Module R Nₗ] [Module R Pₗ] :
                      (Nₗ →ₗ[R] Pₗ) →ₗ[R] (M →ₗ[R] Nₗ) →ₗ[R] M →ₗ[R] Pₗ

                      Composing a linear map M → N and a linear map N → P to form a linear map M → P.

                      Equations
                      Instances For
                        @[simp]
                        theorem LinearMap.llcomp_apply {R : Type u_1} [CommSemiring R] {M : Type u_5} {Nₗ : Type u_10} {Pₗ : Type u_11} [AddCommMonoid M] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ] [Module R M] [Module R Nₗ] [Module R Pₗ] (f : Nₗ →ₗ[R] Pₗ) (g : M →ₗ[R] Nₗ) (x : M) :
                        (((LinearMap.llcomp R M Nₗ Pₗ) f) g) x = f (g x)
                        theorem LinearMap.llcomp_apply' {R : Type u_1} [CommSemiring R] {M : Type u_5} {Nₗ : Type u_10} {Pₗ : Type u_11} [AddCommMonoid M] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ] [Module R M] [Module R Nₗ] [Module R Pₗ] (f : Nₗ →ₗ[R] Pₗ) (g : M →ₗ[R] Nₗ) :
                        ((LinearMap.llcomp R M Nₗ Pₗ) f) g = f ∘ₗ g
                        def LinearMap.compl₂ {R : Type u_1} [CommSemiring R] {R₂ : Type u_2} [CommSemiring R₂] {R₃ : Type u_3} [CommSemiring R₃] {R₄ : Type u_4} [CommSemiring R₄] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R₂ N] [Module R₃ P] [Module R₄ Q] {σ₂₃ : R₂ →+* R₃} {σ₄₂ : R₄ →+* R₂} {σ₄₃ : R₄ →+* R₃} [RingHomCompTriple σ₄₂ σ₂₃ σ₄₃] {R₅ : Type u_14} [CommSemiring R₅] [Module R₅ P] [SMulCommClass R₃ R₅ P] {σ₁₅ : R →+* R₅} (h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P) (g : Q →ₛₗ[σ₄₂] N) :
                        M →ₛₗ[σ₁₅] Q →ₛₗ[σ₄₃] P

                        Composing a linear map Q → N and a bilinear map M → N → P to form a bilinear map M → Q → P.

                        Equations
                        • h.compl₂ g = { toFun := fun (a : M) => (LinearMap.lcompₛₗ P σ₂₃ g) (h a), map_add' := , map_smul' := }
                        Instances For
                          @[simp]
                          theorem LinearMap.compl₂_apply {R : Type u_1} [CommSemiring R] {R₂ : Type u_2} [CommSemiring R₂] {R₃ : Type u_3} [CommSemiring R₃] {R₄ : Type u_4} [CommSemiring R₄] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R₂ N] [Module R₃ P] [Module R₄ Q] {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {σ₄₂ : R₄ →+* R₂} {σ₄₃ : R₄ →+* R₃} [RingHomCompTriple σ₄₂ σ₂₃ σ₄₃] (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) (g : Q →ₛₗ[σ₄₂] N) (m : M) (q : Q) :
                          ((f.compl₂ g) m) q = (f m) (g q)
                          @[simp]
                          theorem LinearMap.compl₂_id {R : Type u_1} [CommSemiring R] {R₂ : Type u_2} [CommSemiring R₂] {R₃ : Type u_3} [CommSemiring R₃] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R₂ N] [Module R₃ P] {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) :
                          f.compl₂ LinearMap.id = f
                          def LinearMap.compl₁₂ {R₂ : Type u_2} [CommSemiring R₂] {N : Type u_6} {Mₗ : Type u_9} {Pₗ : Type u_11} {Qₗ : Type u_12} {Qₗ' : Type u_13} [AddCommMonoid N] [AddCommMonoid Mₗ] [AddCommMonoid Pₗ] [AddCommMonoid Qₗ] [AddCommMonoid Qₗ'] {R₁ : Type u_14} [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ₗ

                          Composing linear maps Q → M and Q' → N with a bilinear map M → N → P to form a bilinear map Q → Q' → P.

                          Equations
                          • f.compl₁₂ g g' = (f ∘ₗ g).compl₂ g'
                          Instances For
                            @[simp]
                            theorem LinearMap.compl₁₂_apply {R : Type u_1} [CommSemiring R] {Mₗ : Type u_9} {Nₗ : Type u_10} {Pₗ : Type u_11} {Qₗ : Type u_12} {Qₗ' : Type u_13} [AddCommMonoid Mₗ] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ] [AddCommMonoid Qₗ] [AddCommMonoid Qₗ'] [Module R Mₗ] [Module R Nₗ] [Module R Pₗ] [Module R Qₗ] [Module R Qₗ'] (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)
                            @[simp]
                            theorem LinearMap.compl₁₂_id_id {R : Type u_1} [CommSemiring R] {Mₗ : Type u_9} {Nₗ : Type u_10} {Pₗ : Type u_11} [AddCommMonoid Mₗ] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ] [Module R Mₗ] [Module R Nₗ] [Module R Pₗ] (f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ) :
                            f.compl₁₂ LinearMap.id LinearMap.id = f
                            theorem LinearMap.compl₁₂_inj {R : Type u_1} [CommSemiring R] {Mₗ : Type u_9} {Nₗ : Type u_10} {Pₗ : Type u_11} {Qₗ : Type u_12} {Qₗ' : Type u_13} [AddCommMonoid Mₗ] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ] [AddCommMonoid Qₗ] [AddCommMonoid Qₗ'] [Module R Mₗ] [Module R Nₗ] [Module R Pₗ] [Module R Qₗ] [Module R Qₗ'] {f₁ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ} {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₂
                            def LinearMap.compr₂ {R : Type u_1} [CommSemiring R] {M : Type u_5} {Nₗ : Type u_10} {Pₗ : Type u_11} {Qₗ : Type u_12} [AddCommMonoid M] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ] [AddCommMonoid Qₗ] [Module R M] [Module R Nₗ] [Module R Pₗ] [Module R Qₗ] (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ) :
                            M →ₗ[R] Nₗ →ₗ[R] Qₗ

                            Composing a linear map P → Q and a bilinear map M → N → P to form a bilinear map M → N → Q.

                            Equations
                            Instances For
                              @[simp]
                              theorem LinearMap.compr₂_apply {R : Type u_1} [CommSemiring R] {M : Type u_5} {Nₗ : Type u_10} {Pₗ : Type u_11} {Qₗ : Type u_12} [AddCommMonoid M] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ] [AddCommMonoid Qₗ] [Module R M] [Module R Nₗ] [Module R Pₗ] [Module R Qₗ] (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ) (m : M) (n : Nₗ) :
                              ((f.compr₂ g) m) n = g ((f m) n)
                              def LinearMap.lsmul (R : Type u_1) [CommSemiring R] (M : Type u_5) [AddCommMonoid M] [Module R M] :

                              Scalar multiplication as a bilinear map R → M → M.

                              Equations
                              Instances For
                                @[simp]
                                theorem LinearMap.lsmul_apply {R : Type u_1} [CommSemiring R] {M : Type u_5} [AddCommMonoid M] [Module R M] (r : R) (m : M) :
                                ((LinearMap.lsmul R M) r) m = r m
                                @[reducible, inline]
                                abbrev LinearMap.BilinMap (R : Type u_1) [CommSemiring R] (M : Type u_5) (Nₗ : Type u_10) [AddCommMonoid M] [AddCommMonoid Nₗ] [Module R M] [Module R Nₗ] :
                                Type (max u_10 u_5)

                                A shorthand for the type of R-bilinear Nₗ-valued maps on M.

                                Equations
                                Instances For
                                  @[reducible, inline]
                                  abbrev LinearMap.BilinForm (R : Type u_1) [CommSemiring R] (M : Type u_5) [AddCommMonoid M] [Module R M] :
                                  Type (max u_1 u_5)

                                  For convenience, a shorthand for the type of bilinear forms from M to R.

                                  Equations
                                  Instances For
                                    theorem LinearMap.lsmul_injective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {x : R} (hx : x 0) :
                                    theorem LinearMap.ker_lsmul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {a : R} (ha : a 0) :