Mathlib.LinearAlgebra.TensorProduct.Basic

TensorProduct.Eqv inductive

: FreeAddMonoid (M × N) → FreeAddMonoid (M × N) → Prop

Full source

/-- The relation on `FreeAddMonoid (M × N)` that generates a congruence whose quotient is
the tensor product. -/
inductive Eqv : FreeAddMonoid (M × N) → FreeAddMonoid (M × N) → Prop
  | of_zero_left : ∀ n : N, Eqv (.of (0, n)) 0
  | of_zero_right : ∀ m : M, Eqv (.of (m, 0)) 0
  | of_add_left : ∀ (m₁ m₂ : M) (n : N), Eqv (.of (m₁, n) + .of (m₂, n)) (.of (m₁ + m₂, n))
  | of_add_right : ∀ (m : M) (n₁ n₂ : N), Eqv (.of (m, n₁) + .of (m, n₂)) (.of (m, n₁ + n₂))
  | of_smul : ∀ (r : R) (m : M) (n : N), Eqv (.of (r • m, n)) (.of (m, r • n))
  | add_comm : ∀ x y, Eqv (x + y) (y + x)

Tensor product equivalence relation

Informal description

The equivalence relation `TensorProduct.Eqv` on the free additive monoid over the product `M × N` that generates the congruence relation whose quotient is the tensor product of modules `M` and `N` over a commutative semiring `R`. This relation identifies pairs of elements in the free additive monoid that should be considered equal in the tensor product space.

TensorProduct.term_⊗_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc TensorProduct] scoped[TensorProduct] infixl:100 " ⊗ " => TensorProduct _

Tensor product notation (⊗)

Informal description

The infix notation `⊗` represents the tensor product operation between two modules over a commutative semiring. For modules $M$ and $N$ over a semiring $R$, the expression $M ⊗ N$ denotes the tensor product space `TensorProduct R M N`, and $m ⊗ n$ represents the tensor product of elements $m ∈ M$ and $n ∈ N$.

TensorProduct.term_⊗[_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] scoped[TensorProduct] notation:100 M " ⊗[" R "] " N:100 => TensorProduct R M N

Tensor product notation `M ⊗[R] N`

Informal description

The notation `M ⊗[R] N` represents the tensor product of modules `M` and `N` over a commutative semiring `R`. This construction satisfies the universal property of tensor products: for any bilinear map `f : M → N → P`, there exists a unique linear map `M ⊗[R] N → P` factoring through the canonical bilinear map `M → N → M ⊗[R] N`.

TensorProduct.term_⊗ₜ_ definition

: Lean.TrailingParserDescr✝

Full source

/-- The canonical function `M → N → M ⊗ N`. -/
infixl:100 " ⊗ₜ " => tmul _

Tensor product of elements

Informal description

The canonical bilinear map $ M \times N \to M \otimes N $, denoted by $ m \otimes n $, which sends a pair $(m, n)$ to their tensor product $ m \otimes n $.

TensorProduct.term_⊗ₜ[_]_ definition

: Lean.TrailingParserDescr✝

Full source

/-- The canonical function `M → N → M ⊗ N`. -/
notation:100 x " ⊗ₜ[" R "] " y:100 => tmul R x y

Tensor product notation over a commutative semiring

Informal description

The notation $ x \otimes_R y $ represents the tensor product of elements $ x $ and $ y $ over the commutative semiring $ R $, which is the canonical bilinear map $ M \times N \to M \otimes_R N $.

TensorProduct.induction_on theorem

 {motive : M ⊗[R] N → Prop} (z : M ⊗[R] N) (zero : motive 0) (tmul : ∀ x y, motive <| x ⊗ₜ[R] y)
  (add : ∀ x y, motive x → motive y → motive (x + y)) : motive z

Full source

@[elab_as_elim, induction_eliminator]
protected theorem induction_on {motive : M ⊗[R] N → Prop} (z : M ⊗[R] N)
    (zero : motive 0)
    (tmul : ∀ x y, motive <| x ⊗ₜ[R] y)
    (add : ∀ x y, motive x → motive y → motive (x + y)) : motive z :=
  AddCon.induction_on z fun x =>
    FreeAddMonoid.recOn x zero fun ⟨m, n⟩ y ih => by
      rw [AddCon.coe_add]
      exact add _ _ (tmul ..) ih

Induction Principle for Tensor Product of Modules

Informal description

Let $M$ and $N$ be modules over a commutative semiring $R$, and let $z$ be an element of their tensor product $M \otimes_R N$. To prove a property $\text{motive}(z)$ holds for all $z \in M \otimes_R N$, it suffices to: 1. Show that $\text{motive}(0)$ holds, 2. Show that $\text{motive}(x \otimes y)$ holds for all $x \in M$ and $y \in N$, 3. Show that $\text{motive}$ is additive, i.e., for any $x, y \in M \otimes_R N$, if $\text{motive}(x)$ and $\text{motive}(y)$ hold, then $\text{motive}(x + y)$ holds.

TensorProduct.liftAddHom_tmul theorem

 (f : M →+ N →+ P) (hf : ∀ (r : R) (m : M) (n : N), f (r • m) n = f m (r • n)) (m : M) (n : N) :
  liftAddHom f hf (m ⊗ₜ n) = f m n

Full source

@[simp]
theorem liftAddHom_tmul (f : M →+ N →+ P)
    (hf : ∀ (r : R) (m : M) (n : N), f (r • m) n = f m (r • n)) (m : M) (n : N) :
    liftAddHom f hf (m ⊗ₜ n) = f m n :=
  rfl

Evaluation of Lifted Bilinear Map on Tensor Product: $\text{liftAddHom}(f)(m \otimes n) = f(m, n)$

Informal description

Let $M$, $N$, and $P$ be additive commutative monoids over a commutative semiring $R$, and let $f: M \to N \to P$ be an additive monoid homomorphism in each argument that satisfies the bilinearity condition $f(r \cdot m, n) = f(m, r \cdot n)$ for all $r \in R$, $m \in M$, and $n \in N$. Then the lifted homomorphism $\text{liftAddHom}(f)$ applied to the tensor product $m \otimes n$ equals $f(m, n)$.

TensorProduct.zero_tmul theorem

(n : N) : (0 : M) ⊗ₜ[R] n = 0

Full source

@[simp]
theorem zero_tmul (n : N) : (0 : M) ⊗ₜ[R] n = 0 :=
  Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_zero_left _

Tensor product with zero on the left: $0 \otimes_R n = 0$

Informal description

For any element $n$ in an $R$-module $N$, the tensor product of the zero element from an $R$-module $M$ with $n$ is equal to the zero element in the tensor product module $M \otimes_R N$, i.e., $0 \otimes_R n = 0$.

TensorProduct.add_tmul theorem

(m₁ m₂ : M) (n : N) : (m₁ + m₂) ⊗ₜ n = m₁ ⊗ₜ n + m₂ ⊗ₜ[R] n

Full source

theorem add_tmul (m₁ m₂ : M) (n : N) : (m₁ + m₂) ⊗ₜ n = m₁ ⊗ₜ n + m₂ ⊗ₜ[R] n :=
  Eq.symm <| Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_add_left _ _ _

Additivity of Tensor Product in First Argument: $(m_1 + m_2) \otimes n = m_1 \otimes n + m_2 \otimes n$

Informal description

For any elements $m_1, m_2$ in an $R$-module $M$ and any element $n$ in an $R$-module $N$, the tensor product of the sum $m_1 + m_2$ with $n$ is equal to the sum of the tensor products $m_1 \otimes n$ and $m_2 \otimes n$. That is, $(m_1 + m_2) \otimes n = m_1 \otimes n + m_2 \otimes n$.

TensorProduct.tmul_zero theorem

(m : M) : m ⊗ₜ[R] (0 : N) = 0

Full source

@[simp]
theorem tmul_zero (m : M) : m ⊗ₜ[R] (0 : N) = 0 :=
  Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_zero_right _

Tensor product with zero element: $m \otimes 0 = 0$

Informal description

For any element $m$ of a module $M$ over a commutative semiring $R$, the tensor product of $m$ with the zero element of another module $N$ over $R$ is equal to the zero element in the tensor product space $M \otimes_R N$, i.e., $m \otimes 0 = 0$.

TensorProduct.tmul_add theorem

(m : M) (n₁ n₂ : N) : m ⊗ₜ (n₁ + n₂) = m ⊗ₜ n₁ + m ⊗ₜ[R] n₂

Full source

theorem tmul_add (m : M) (n₁ n₂ : N) : m ⊗ₜ (n₁ + n₂) = m ⊗ₜ n₁ + m ⊗ₜ[R] n₂ :=
  Eq.symm <| Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_add_right _ _ _

Tensor Product Distributes Over Addition in Second Argument: $m \otimes (n₁ + n₂) = m \otimes n₁ + m \otimes n₂$

Informal description

For any element $m$ in a module $M$ and any elements $n₁, n₂$ in a module $N$ over a commutative semiring $R$, the tensor product of $m$ with the sum $n₁ + n₂$ is equal to the sum of the tensor products $m \otimes n₁$ and $m \otimes n₂$. That is, \[ m \otimes (n₁ + n₂) = m \otimes n₁ + m \otimes n₂. \]

TensorProduct.CompatibleSMul structure

[DistribMulAction R' N]

Full source

/-- A typeclass for `SMul` structures which can be moved across a tensor product.

This typeclass is generated automatically from an `IsScalarTower` instance, but exists so that
we can also add an instance for `AddCommGroup.toIntModule`, allowing `z •` to be moved even if
`R` does not support negation.

Note that `Module R' (M ⊗[R] N)` is available even without this typeclass on `R'`; it's only
needed if `TensorProduct.smul_tmul`, `TensorProduct.smul_tmul'`, or `TensorProduct.tmul_smul` is
used.
-/
class CompatibleSMul [DistribMulAction R' N] : Prop where
  smul_tmul : ∀ (r : R') (m : M) (n : N), (r • m) ⊗ₜ n = m ⊗ₜ[R] (r • n)

Compatible scalar multiplication for tensor products

Informal description

A typeclass for scalar multiplication structures that can be moved across a tensor product. Specifically, it ensures that for a scalar $r$ from $R'$, the operation $r \cdot (m \otimes n)$ can be rewritten as $m \otimes (r \cdot n)$, where $m$ is an element of module $M$ and $n$ is an element of module $N$ over a commutative semiring $R$.

TensorProduct.smul_tmul theorem

[DistribMulAction R' N] [CompatibleSMul R R' M N] (r : R') (m : M) (n : N) : (r • m) ⊗ₜ n = m ⊗ₜ[R] (r • n)

Full source

/-- `smul` can be moved from one side of the product to the other . -/
theorem smul_tmul [DistribMulAction R' N] [CompatibleSMul R R' M N] (r : R') (m : M) (n : N) :
    (r • m) ⊗ₜ n = m ⊗ₜ[R] (r • n) :=
  CompatibleSMul.smul_tmul _ _ _

Scalar Multiplication Commutes with Tensor Product: $(r \cdot m) \otimes n = m \otimes (r \cdot n)$

Informal description

Let $R$ be a commutative semiring, $R'$ a type with a distributive multiplicative action on an $R$-module $N$, and $M$ another $R$-module. Suppose the scalar multiplication from $R'$ is compatible with the tensor product over $R$. Then for any scalar $r \in R'$ and elements $m \in M$, $n \in N$, we have the equality: \[ (r \cdot m) \otimes n = m \otimes (r \cdot n) \] in the tensor product $M \otimes_R N$.

TensorProduct.SMul.aux_of theorem

{R' : Type*} [SMul R' M] (r : R') (m : M) (n : N) : SMul.aux r (.of (m, n)) = (r • m) ⊗ₜ[R] n

Full source

theorem SMul.aux_of {R' : Type*} [SMul R' M] (r : R') (m : M) (n : N) :
    SMul.aux r (.of (m, n)) = (r • m) ⊗ₜ[R] n :=
  rfl

Auxiliary Scalar Multiplication on Canonical Tensor Elements: $\text{SMul.aux}\, r\, (m \otimes n) = (r \cdot m) \otimes n$

Informal description

For any scalar $r \in R'$ with a scalar multiplication action on an $R$-module $M$, and for any elements $m \in M$ and $n \in N$, the auxiliary scalar multiplication operation `SMul.aux` satisfies: \[ \text{SMul.aux}\, r\, (\text{of}\, (m, n)) = (r \cdot m) \otimes_R n \] where $\text{of}\, (m, n)$ represents the canonical inclusion of $(m, n)$ into the tensor product $M \otimes_R N$.

TensorProduct.smul_zero theorem

(r : R') : r • (0 : M ⊗[R] N) = 0

Full source

protected theorem smul_zero (r : R') : r • (0 : M ⊗[R] N) = 0 :=
  AddMonoidHom.map_zero _

Scalar Multiplication Annihilates Zero in Tensor Product: $r \cdot 0 = 0$

Informal description

For any scalar $r$ in $R'$, the scalar multiplication of $r$ with the zero element in the tensor product $M \otimes_R N$ yields the zero element, i.e., $r \cdot 0 = 0$.

TensorProduct.smul_add theorem

(r : R') (x y : M ⊗[R] N) : r • (x + y) = r • x + r • y

Full source

protected theorem smul_add (r : R') (x y : M ⊗[R] N) : r • (x + y) = r • x + r • y :=
  AddMonoidHom.map_add _ _ _

Distributivity of Scalar Multiplication over Addition in Tensor Product

Informal description

For any scalar $r \in R'$ and any elements $x, y$ in the tensor product $M \otimes_R N$, the scalar multiplication satisfies the distributive property: \[ r \cdot (x + y) = r \cdot x + r \cdot y \]

TensorProduct.zero_smul theorem

(x : M ⊗[R] N) : (0 : R'') • x = 0

Full source

protected theorem zero_smul (x : M ⊗[R] N) : (0 : R'') • x = 0 :=
  have : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ n := fun _ _ _ => rfl
  x.induction_on (by rw [TensorProduct.smul_zero])
    (fun m n => by rw [this, zero_smul, zero_tmul]) fun x y ihx ihy => by
    rw [TensorProduct.smul_add, ihx, ihy, add_zero]

Zero Scalar Multiplication Annihilates Tensor Product Elements: $0 \cdot x = 0$

Informal description

For any element $x$ in the tensor product $M \otimes_R N$ of modules over a commutative semiring $R$, the scalar multiplication by the zero element of $R''$ yields the zero element, i.e., $0 \cdot x = 0$.

TensorProduct.one_smul theorem

(x : M ⊗[R] N) : (1 : R') • x = x

Full source

protected theorem one_smul (x : M ⊗[R] N) : (1 : R') • x = x :=
  have : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ n := fun _ _ _ => rfl
  x.induction_on (by rw [TensorProduct.smul_zero])
    (fun m n => by rw [this, one_smul])
    fun x y ihx ihy => by rw [TensorProduct.smul_add, ihx, ihy]

Identity Scalar Multiplication in Tensor Product: $1 \cdot x = x$

Informal description

For any element $x$ in the tensor product $M \otimes_R N$ of modules over a commutative semiring $R$, the scalar multiplication by the multiplicative identity $1 \in R'$ satisfies $1 \cdot x = x$.

TensorProduct.add_smul theorem

(r s : R'') (x : M ⊗[R] N) : (r + s) • x = r • x + s • x

Full source

protected theorem add_smul (r s : R'') (x : M ⊗[R] N) : (r + s) • x = r • x + s • x :=
  have : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ n := fun _ _ _ => rfl
  x.induction_on (by simp_rw [TensorProduct.smul_zero, add_zero])
    (fun m n => by simp_rw [this, add_smul, add_tmul]) fun x y ihx ihy => by
    simp_rw [TensorProduct.smul_add]
    rw [ihx, ihy, add_add_add_comm]

Additivity of Scalar Multiplication in Tensor Product: $(r + s) \cdot x = r \cdot x + s \cdot x$

Informal description

For any scalars $r, s$ in $R''$ and any element $x$ in the tensor product $M \otimes_R N$, the scalar multiplication satisfies the additive property: \[ (r + s) \cdot x = r \cdot x + s \cdot x. \]

TensorProduct.smul_tmul' theorem

(r : R') (m : M) (n : N) : r • m ⊗ₜ[R] n = (r • m) ⊗ₜ n

Full source

theorem smul_tmul' (r : R') (m : M) (n : N) : r • m ⊗ₜ[R] n = (r • m) ⊗ₜ n :=
  rfl

Scalar Multiplication Commutes with Tensor Product: $r \cdot (m \otimes n) = (r \cdot m) \otimes n$

Informal description

For any scalar $r$ in a commutative semiring $R'$, and any elements $m \in M$ and $n \in N$ of modules over $R$, the scalar multiplication of $r$ with the tensor product $m \otimes n$ is equal to the tensor product of $r \cdot m$ with $n$, i.e., \[ r \cdot (m \otimes n) = (r \cdot m) \otimes n. \]

TensorProduct.tmul_smul theorem

[DistribMulAction R' N] [CompatibleSMul R R' M N] (r : R') (x : M) (y : N) : x ⊗ₜ (r • y) = r • x ⊗ₜ[R] y

Full source

@[simp]
theorem tmul_smul [DistribMulAction R' N] [CompatibleSMul R R' M N] (r : R') (x : M) (y : N) :
    x ⊗ₜ (r • y) = r • x ⊗ₜ[R] y :=
  (smul_tmul _ _ _).symm

Tensor Product Scalar Multiplication: $x \otimes (r \cdot y) = r \cdot (x \otimes y)$

Informal description

Let $R$ be a commutative semiring, $R'$ a type with a distributive multiplicative action on an $R$-module $N$, and $M$ another $R$-module. Suppose the scalar multiplication from $R'$ is compatible with the tensor product over $R$. Then for any scalar $r \in R'$ and elements $x \in M$, $y \in N$, we have the equality: \[ x \otimes (r \cdot y) = r \cdot (x \otimes y) \] in the tensor product $M \otimes_R N$.

TensorProduct.smul_tmul_smul theorem

(r s : R) (m : M) (n : N) : (r • m) ⊗ₜ[R] (s • n) = (r * s) • m ⊗ₜ[R] n

Full source

theorem smul_tmul_smul (r s : R) (m : M) (n : N) : (r • m) ⊗ₜ[R] (s • n) = (r * s) • m ⊗ₜ[R] n := by
  simp_rw [smul_tmul, tmul_smul, mul_smul]

Scalar Multiplication Compatibility in Tensor Product: $(r \cdot m) \otimes_R (s \cdot n) = (r \cdot s) \cdot (m \otimes_R n)$

Informal description

Let $R$ be a commutative semiring, and let $M$ and $N$ be modules over $R$. For any scalars $r, s \in R$ and elements $m \in M$, $n \in N$, the tensor product of the scalar multiples $(r \cdot m) \otimes_R (s \cdot n)$ is equal to the scalar multiple $(r \cdot s) \cdot (m \otimes_R n)$.

TensorProduct.mk_apply theorem

(m : M) (n : N) : mk R M N m n = m ⊗ₜ n

Full source

@[simp]
theorem mk_apply (m : M) (n : N) : mk R M N m n = m ⊗ₜ n :=
  rfl

Canonical Bilinear Map Evaluates to Tensor Product: $\text{mk}_R(m, n) = m \otimes_R n$

Informal description

For any elements $m \in M$ and $n \in N$, the canonical bilinear map $\text{mk}_R$ evaluated at $(m, n)$ equals the tensor product $m \otimes_R n$.

TensorProduct.ite_tmul theorem

 (x₁ : M) (x₂ : N) (P : Prop) [Decidable P] : (if P then x₁ else 0) ⊗ₜ[R] x₂ = if P then x₁ ⊗ₜ x₂ else 0

Full source

theorem ite_tmul (x₁ : M) (x₂ : N) (P : Prop) [Decidable P] :
    (if P then x₁ else 0) ⊗ₜ[R] x₂ = if P then x₁ ⊗ₜ x₂ else 0 := by split_ifs <;> simp

Conditional Tensor Product: $(P ? x_1 : 0) \otimes_R x_2 = P ? (x_1 \otimes_R x_2) : 0$

Informal description

Let $M$ and $N$ be modules over a commutative semiring $R$, and let $x_1 \in M$, $x_2 \in N$. For any proposition $P$ (with a decision procedure), the tensor product $( \text{if } P \text{ then } x_1 \text{ else } 0 ) \otimes_R x_2$ equals $\text{if } P \text{ then } (x_1 \otimes_R x_2) \text{ else } 0$.

TensorProduct.tmul_ite theorem

 (x₁ : M) (x₂ : N) (P : Prop) [Decidable P] : (x₁ ⊗ₜ[R] if P then x₂ else 0) = if P then x₁ ⊗ₜ x₂ else 0

Full source

theorem tmul_ite (x₁ : M) (x₂ : N) (P : Prop) [Decidable P] :
    (x₁ ⊗ₜ[R] if P then x₂ else 0) = if P then x₁ ⊗ₜ x₂ else 0 := by split_ifs <;> simp

Tensor Product with Conditional: $x_1 \otimes_R (P ? x_2 : 0) = P ? (x_1 \otimes_R x_2) : 0$

Informal description

Let $M$ and $N$ be modules over a commutative semiring $R$, and let $x_1 \in M$, $x_2 \in N$. For any proposition $P$ (with a decision procedure), the tensor product $x_1 \otimes_R (\text{if } P \text{ then } x_2 \text{ else } 0)$ equals $\text{if } P \text{ then } (x_1 \otimes_R x_2) \text{ else } 0$.

TensorProduct.tmul_single theorem

 {ι : Type*} [DecidableEq ι] {M : ι → Type*} [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)] (i : ι) (x : N) (m : M i)
  (j : ι) : x ⊗ₜ[R] Pi.single i m j = (Pi.single i (x ⊗ₜ[R] m) : ∀ i, N ⊗[R] M i) j

Full source

lemma tmul_single {ι : Type*} [DecidableEq ι] {M : ι → Type*} [∀ i, AddCommMonoid (M i)]
    [∀ i, Module R (M i)] (i : ι) (x : N) (m : M i) (j : ι) :
    x ⊗ₜ[R] Pi.single i m j = (Pi.single i (x ⊗ₜ[R] m) : ∀ i, N ⊗[R] M i) j := by
  by_cases h : i = j <;> aesop

Tensor Product with Single Function: $x \otimes_R (\text{single}_i m)_j = (\text{single}_i (x \otimes_R m))_j$

Informal description

Let $R$ be a commutative semiring, $N$ an $R$-module, and $\{M_i\}_{i \in \iota}$ a family of $R$-modules indexed by a type $\iota$ with decidable equality. For any $i \in \iota$, $x \in N$, and $m \in M_i$, the tensor product $x \otimes_R (\text{Pi.single}_i m)_j$ equals $(\text{Pi.single}_i (x \otimes_R m))_j$ for all $j \in \iota$, where $\text{Pi.single}_i$ denotes the function that is $m$ at $i$ and zero elsewhere.

TensorProduct.single_tmul theorem

 {ι : Type*} [DecidableEq ι] {M : ι → Type*} [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)] (i : ι) (x : N) (m : M i)
  (j : ι) : Pi.single i m j ⊗ₜ[R] x = (Pi.single i (m ⊗ₜ[R] x) : ∀ i, M i ⊗[R] N) j

Full source

lemma single_tmul {ι : Type*} [DecidableEq ι] {M : ι → Type*} [∀ i, AddCommMonoid (M i)]
    [∀ i, Module R (M i)] (i : ι) (x : N) (m : M i) (j : ι) :
    Pi.singlePi.single i m j ⊗ₜ[R] x = (Pi.single i (m ⊗ₜ[R] x) : ∀ i, M i ⊗[R] N) j := by
  by_cases h : i = j <;> aesop

Tensor Product with Single Function Component: $(\text{single}_i(m))_j \otimes_R x = (\text{single}_i(m \otimes_R x))_j$

Informal description

Let $R$ be a commutative semiring, $N$ an $R$-module, and $\{M_i\}_{i \in \iota}$ a family of $R$-modules indexed by a type $\iota$ with decidable equality. For any $i \in \iota$, elements $x \in N$ and $m \in M_i$, and any index $j \in \iota$, the tensor product of the $j$-th component of the single function $\text{Pi.single}_i(m)$ with $x$ equals the $j$-th component of the single function $\text{Pi.single}_i(m \otimes_R x)$. That is, \[ (\text{Pi.single}_i(m))_j \otimes_R x = (\text{Pi.single}_i(m \otimes_R x))_j. \]

TensorProduct.sum_tmul theorem

{α : Type*} (s : Finset α) (m : α → M) (n : N) : (∑ a ∈ s, m a) ⊗ₜ[R] n = ∑ a ∈ s, m a ⊗ₜ[R] n

Full source

theorem sum_tmul {α : Type*} (s : Finset α) (m : α → M) (n : N) :
    (∑ a ∈ s, m a) ⊗ₜ[R] n = ∑ a ∈ s, m a ⊗ₜ[R] n := by
  classical
    induction s using Finset.induction with
    | empty => simp
    | insert _ _ has ih => simp [Finset.sum_insert has, add_tmul, ih]

Distributivity of Tensor Product over Finite Sum in First Argument: $(\sum_{a \in s} m(a)) \otimes_R n = \sum_{a \in s} (m(a) \otimes_R n)$

Informal description

Let $R$ be a commutative semiring, $M$ and $N$ be $R$-modules, and $\alpha$ be a type. For any finite set $s \subseteq \alpha$, any function $m \colon \alpha \to M$, and any element $n \in N$, the tensor product of the sum $\sum_{a \in s} m(a)$ with $n$ is equal to the sum of the tensor products $\sum_{a \in s} (m(a) \otimes_R n)$. That is, \[ \left(\sum_{a \in s} m(a)\right) \otimes_R n = \sum_{a \in s} \left(m(a) \otimes_R n\right). \]

TensorProduct.tmul_sum theorem

(m : M) {α : Type*} (s : Finset α) (n : α → N) : (m ⊗ₜ[R] ∑ a ∈ s, n a) = ∑ a ∈ s, m ⊗ₜ[R] n a

Full source

theorem tmul_sum (m : M) {α : Type*} (s : Finset α) (n : α → N) :
    (m ⊗ₜ[R] ∑ a ∈ s, n a) = ∑ a ∈ s, m ⊗ₜ[R] n a := by
  classical
    induction s using Finset.induction with
    | empty => simp
    | insert _ _ has ih => simp [Finset.sum_insert has, tmul_add, ih]

Tensor Product Distributes Over Finite Sum in Second Argument: $m \otimes (\sum n_a) = \sum (m \otimes n_a)$

Informal description

For any element $m$ in an $R$-module $M$, any finite set $s$ with elements of type $\alpha$, and any function $n : \alpha \to N$ where $N$ is another $R$-module, the tensor product of $m$ with the sum $\sum_{a \in s} n(a)$ is equal to the sum of the tensor products $\sum_{a \in s} (m \otimes_R n(a))$. That is, \[ m \otimes_R \left(\sum_{a \in s} n(a)\right) = \sum_{a \in s} (m \otimes_R n(a)). \]

TensorProduct.span_tmul_eq_top theorem

: Submodule.span R {t : M ⊗[R] N | ∃ m n, m ⊗ₜ n = t} = ⊤

Full source

/-- The simple (aka pure) elements span the tensor product. -/
theorem span_tmul_eq_top : Submodule.span R { t : M ⊗[R] N | ∃ m n, m ⊗ₜ n = t } = ⊤ := by
  ext t; simp only [Submodule.mem_top, iff_true]
  refine t.induction_on ?_ ?_ ?_
  · exact Submodule.zero_mem _
  · intro m n
    apply Submodule.subset_span
    use m, n
  · intro t₁ t₂ ht₁ ht₂
    exact Submodule.add_mem _ ht₁ ht₂

Pure Tensors Span the Tensor Product: $\operatorname{span}_R \{m \otimes n \mid m \in M, n \in N\} = M \otimes_R N$

Informal description

The span of the set of all pure tensors $m \otimes n$ in the tensor product $M \otimes_R N$ is equal to the entire space $M \otimes_R N$. In other words, every element of the tensor product can be written as a finite linear combination of pure tensors.

TensorProduct.map₂_mk_top_top_eq_top theorem

: Submodule.map₂ (mk R M N) ⊤ ⊤ = ⊤

Full source

@[simp]
theorem map₂_mk_top_top_eq_top : Submodule.map₂ (mk R M N) ⊤ ⊤ = ⊤ := by
  rw [← top_le_iff, ← span_tmul_eq_top, Submodule.map₂_eq_span_image2]
  exact Submodule.span_mono fun _ ⟨m, n, h⟩ => ⟨m, trivial, n, trivial, h⟩

Image of Bilinear Map on Top Submodules Spans Tensor Product: $\text{map}_2(\text{mk}_R, M, N) = M \otimes_R N$

Informal description

For modules $M$ and $N$ over a commutative semiring $R$, the image of the top submodules under the bilinear map $\text{mk}_R : M \to N \to M \otimes_R N$ is equal to the top submodule of $M \otimes_R N$. In other words, the span of all elements of the form $\text{mk}_R(m)(n)$ for $m \in M$ and $n \in N$ is the entire tensor product space $M \otimes_R N$.

TensorProduct.exists_eq_tmul_of_forall theorem

 (x : TensorProduct R M N) (h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ m n, m₁ ⊗ₜ n₁ + m₂ ⊗ₜ n₂ = m ⊗ₜ[R] n) : ∃ m n, x = m ⊗ₜ n

Full source

theorem exists_eq_tmul_of_forall (x : TensorProduct R M N)
    (h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ m n, m₁ ⊗ₜ n₁ + m₂ ⊗ₜ n₂ = m ⊗ₜ[R] n) :
    ∃ m n, x = m ⊗ₜ n := by
  induction x with
  | zero =>
    use 0, 0
    rw [TensorProduct.zero_tmul]
  | tmul m n => use m, n
  | add x y h₁ h₂ =>
    obtain ⟨m₁, n₁, rfl⟩ := h₁
    obtain ⟨m₂, n₂, rfl⟩ := h₂
    apply h

Tensor Product Element as Pure Tensor Under Additive Condition

Informal description

Let $M$ and $N$ be modules over a commutative semiring $R$, and let $x$ be an element of their tensor product $M \otimes_R N$. Suppose that for any $m_1, m_2 \in M$ and $n_1, n_2 \in N$, there exist $m \in M$ and $n \in N$ such that $m_1 \otimes n_1 + m_2 \otimes n_2 = m \otimes n$. Then there exist $m \in M$ and $n \in N$ such that $x = m \otimes n$.

TensorProduct.liftAux_tmul theorem

(m n) : liftAux f (m ⊗ₜ n) = f m n

Full source

theorem liftAux_tmul (m n) : liftAux f (m ⊗ₜ n) = f m n :=
  rfl

Auxiliary Tensor Lift on Pure Tensors

Informal description

For any bilinear map $f \colon M \to N \to P$ and any elements $m \in M$ and $n \in N$, the auxiliary lifting function $\text{liftAux}(f)$ satisfies $\text{liftAux}(f)(m \otimes n) = f(m)(n)$.

TensorProduct.liftAux.smul theorem

(r : R) (x) : liftAux f (r • x) = r • liftAux f x

Full source

@[simp]
theorem liftAux.smul (r : R) (x) : liftAux f (r • x) = r • liftAux f x :=
  TensorProduct.induction_on x (smul_zero _).symm
    (fun p q => by simp_rw [← tmul_smul, liftAux_tmul, (f p).map_smul])
    fun p q ih1 ih2 => by simp_rw [smul_add, (liftAux f).map_add, ih1, ih2, smul_add]

Linearity of Auxiliary Tensor Lift with Respect to Scalar Multiplication

Informal description

For any bilinear map $f \colon M \to N \to P$, any scalar $r \in R$, and any element $x \in M \otimes_R N$, the auxiliary lifting function $\text{liftAux}(f)$ satisfies $\text{liftAux}(f)(r \cdot x) = r \cdot \text{liftAux}(f)(x)$.

TensorProduct.lift.tmul theorem

(x y) : lift f (x ⊗ₜ y) = f x y

Full source

@[simp]
theorem lift.tmul (x y) : lift f (x ⊗ₜ y) = f x y :=
  rfl

Lifted Tensor Map Evaluates as Original Bilinear Map on Simple Tensors

Informal description

For any bilinear map $f \colon M \to N \to P$ and any elements $x \in M$, $y \in N$, the lifted linear map $\text{lift}(f)$ satisfies $\text{lift}(f)(x \otimes y) = f(x)(y)$.

TensorProduct.lift.tmul' theorem

(x y) : (lift f).1 (x ⊗ₜ y) = f x y

Full source

@[simp]
theorem lift.tmul' (x y) : (lift f).1 (x ⊗ₜ y) = f x y :=
  rfl

Action of Tensor Lift on Simple Tensors

Informal description

For any bilinear map $f \colon M \to N \to P$ and any elements $x \in M$, $y \in N$, the linear map $\text{lift}(f) \colon M \otimes_R N \to P$ satisfies $\text{lift}(f)(x \otimes y) = f(x)(y)$.

TensorProduct.ext' theorem

{g h : M ⊗[R] N →ₗ[R] P} (H : ∀ x y, g (x ⊗ₜ y) = h (x ⊗ₜ y)) : g = h

Full source

theorem ext' {g h : M ⊗[R] NM ⊗[R] N →ₗ[R] P} (H : ∀ x y, g (x ⊗ₜ y) = h (x ⊗ₜ y)) : g = h :=
  LinearMap.ext fun z =>
    TensorProduct.induction_on z (by simp_rw [LinearMap.map_zero]) H fun x y ihx ihy => by
      rw [g.map_add, h.map_add, ihx, ihy]

Uniqueness of Linear Maps on Tensor Products via Action on Simple Tensors

Informal description

Let $M$ and $N$ be modules over a commutative semiring $R$, and let $P$ be another $R$-module. For any two linear maps $g, h: M \otimes_R N \to P$, if $g(x \otimes y) = h(x \otimes y)$ for all $x \in M$ and $y \in N$, then $g = h$.

TensorProduct.lift.unique theorem

{g : M ⊗[R] N →ₗ[R] P} (H : ∀ x y, g (x ⊗ₜ y) = f x y) : g = lift f

Full source

theorem lift.unique {g : M ⊗[R] NM ⊗[R] N →ₗ[R] P} (H : ∀ x y, g (x ⊗ₜ y) = f x y) : g = lift f :=
  ext' fun m n => by rw [H, lift.tmul]

Uniqueness of Tensor Product Lift

Informal description

Let $M$ and $N$ be modules over a commutative semiring $R$, and let $P$ be another $R$-module. Given a bilinear map $f \colon M \to N \to P$, for any linear map $g \colon M \otimes_R N \to P$ satisfying $g(x \otimes y) = f(x)(y)$ for all $x \in M$ and $y \in N$, we have $g = \text{lift}(f)$.

TensorProduct.lift_mk theorem

: lift (mk R M N) = LinearMap.id

Full source

theorem lift_mk : lift (mk R M N) = LinearMap.id :=
  Eq.symm <| lift.unique fun _ _ => rfl

Lifting the Canonical Bilinear Map Yields the Identity Map on Tensor Product

Informal description

Let $M$ and $N$ be modules over a commutative semiring $R$. The linear map obtained by lifting the canonical bilinear map $\text{mk}_R \colon M \to N \to M \otimes_R N$ is equal to the identity map on $M \otimes_R N$, i.e., $\text{lift}(\text{mk}_R) = \text{id}$.

TensorProduct.lift_compr₂ theorem

(g : P →ₗ[R] Q) : lift (f.compr₂ g) = g.comp (lift f)

Full source

theorem lift_compr₂ (g : P →ₗ[R] Q) : lift (f.compr₂ g) = g.comp (lift f) :=
  Eq.symm <| lift.unique fun _ _ => by simp

Compatibility of Tensor Product Lift with Composition: $\text{lift}(f \circ g) = g \circ \text{lift}(f)$

Informal description

Let $M$, $N$, $P$, and $Q$ be modules over a commutative semiring $R$. Given a bilinear map $f \colon M \to N \to P$ and a linear map $g \colon P \to Q$, the lift of the composition $f \circ g$ is equal to the composition of $g$ with the lift of $f$, i.e., $\text{lift}(f \circ g) = g \circ \text{lift}(f)$.

TensorProduct.lift_mk_compr₂ theorem

(f : M ⊗ N →ₗ[R] P) : lift ((mk R M N).compr₂ f) = f

Full source

theorem lift_mk_compr₂ (f : M ⊗ NM ⊗ N →ₗ[R] P) : lift ((mk R M N).compr₂ f) = f := by
  rw [lift_compr₂ f, lift_mk, LinearMap.comp_id]

Lift of Composition with Canonical Bilinear Map Equals Original Map: $\text{lift}(\text{mk}_R \circ f) = f$

Informal description

Let $M$, $N$, and $P$ be modules over a commutative semiring $R$. For any linear map $f \colon M \otimes_R N \to P$, the lift of the composition of the canonical bilinear map $\text{mk}_R \colon M \to N \to M \otimes_R N$ with $f$ is equal to $f$ itself, i.e., $\text{lift}(\text{mk}_R \circ f) = f$.

TensorProduct.ext theorem

{g h : M ⊗ N →ₗ[R] P} (H : (mk R M N).compr₂ g = (mk R M N).compr₂ h) : g = h

Full source

/-- This used to be an `@[ext]` lemma, but it fails very slowly when the `ext` tactic tries to apply
it in some cases, notably when one wants to show equality of two linear maps. The `@[ext]`
attribute is now added locally where it is needed. Using this as the `@[ext]` lemma instead of
`TensorProduct.ext'` allows `ext` to apply lemmas specific to `M →ₗ _` and `N →ₗ _`.

See note [partially-applied ext lemmas]. -/
theorem ext {g h : M ⊗ NM ⊗ N →ₗ[R] P} (H : (mk R M N).compr₂ g = (mk R M N).compr₂ h) : g = h := by
  rw [← lift_mk_compr₂ g, H, lift_mk_compr₂]

Uniqueness of Linear Maps from Tensor Product via Canonical Bilinear Map

Informal description

Let $M$, $N$, and $P$ be modules over a commutative semiring $R$. For any two linear maps $g, h \colon M \otimes_R N \to P$, if the compositions of the canonical bilinear map $\text{mk}_R \colon M \to N \to M \otimes_R N$ with $g$ and $h$ are equal, i.e., $\text{mk}_R \circ g = \text{mk}_R \circ h$, then $g = h$.

TensorProduct.uncurry_apply theorem

(f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) : uncurry R M N P f (m ⊗ₜ n) = f m n

Full source

@[simp]
theorem uncurry_apply (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) :
    uncurry R M N P f (m ⊗ₜ n) = f m n := by rw [uncurry, LinearMap.flip_apply, lift.tmul]; rfl

Evaluation of Uncurried Tensor Map on Simple Tensors: $\text{uncurry}(f)(m \otimes n) = f(m)(n)$

Informal description

For any $R$-linear map $f \colon M \to_R N \to_R P$ and any elements $m \in M$, $n \in N$, the uncurried map $\text{uncurry}(f)$ satisfies $\text{uncurry}(f)(m \otimes n) = f(m)(n)$.

TensorProduct.lift.equiv_apply theorem

(f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) : lift.equiv R M N P f (m ⊗ₜ n) = f m n

Full source

@[simp]
theorem lift.equiv_apply (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) :
    lift.equiv R M N P f (m ⊗ₜ n) = f m n :=
  uncurry_apply f m n

Evaluation of Tensor Lift Equivalence on Simple Tensors: $\text{lift.equiv}(f)(m \otimes_R n) = f(m)(n)$

Informal description

For any $R$-bilinear map $f \colon M \to_R N \to_R P$ and any elements $m \in M$, $n \in N$, the tensor product lift equivalence satisfies $\text{lift.equiv}(f)(m \otimes_R n) = f(m)(n)$.

TensorProduct.lift.equiv_symm_apply theorem

(f : M ⊗[R] N →ₗ[R] P) (m : M) (n : N) : (lift.equiv R M N P).symm f m n = f (m ⊗ₜ n)

Full source

@[simp]
theorem lift.equiv_symm_apply (f : M ⊗[R] NM ⊗[R] N →ₗ[R] P) (m : M) (n : N) :
    (lift.equiv R M N P).symm f m n = f (m ⊗ₜ n) :=
  rfl

Inverse Tensor Lift Equivalence Evaluation: $(\text{lift.equiv})^{-1}(f)(m)(n) = f(m \otimes n)$

Informal description

For any $R$-linear map $f \colon M \otimes_R N \to P$ and elements $m \in M$, $n \in N$, the inverse of the equivalence $\text{lift.equiv}$ satisfies $(\text{lift.equiv})^{-1}(f)(m)(n) = f(m \otimes n)$.

TensorProduct.lcurry_apply theorem

(f : M ⊗[R] N →ₗ[R] P) (m : M) (n : N) : lcurry R M N P f m n = f (m ⊗ₜ n)

Full source

@[simp]
theorem lcurry_apply (f : M ⊗[R] NM ⊗[R] N →ₗ[R] P) (m : M) (n : N) : lcurry R M N P f m n = f (m ⊗ₜ n) :=
  rfl

Evaluation of Left-Curried Tensor Map: $\text{lcurry}(f)(m)(n) = f(m \otimes n)$

Informal description

For any $R$-linear map $f \colon M \otimes_R N \to P$ and elements $m \in M$, $n \in N$, the left-curried version of $f$ satisfies $\text{lcurry}(f)(m)(n) = f(m \otimes n)$.

TensorProduct.curry_apply theorem

(f : M ⊗ N →ₗ[R] P) (m : M) (n : N) : curry f m n = f (m ⊗ₜ n)

Full source

@[simp]
theorem curry_apply (f : M ⊗ NM ⊗ N →ₗ[R] P) (m : M) (n : N) : curry f m n = f (m ⊗ₜ n) :=
  rfl

Evaluation of Curried Tensor Map: $\text{curry}(f)(m)(n) = f(m \otimes n)$

Informal description

For any $R$-linear map $f \colon M \otimes_R N \to P$ and elements $m \in M$, $n \in N$, the curried version of $f$ satisfies $\text{curry}(f)(m)(n) = f(m \otimes n)$.

TensorProduct.curry_injective theorem

: Function.Injective (curry : (M ⊗[R] N →ₗ[R] P) → M →ₗ[R] N →ₗ[R] P)

Full source

theorem curry_injective : Function.Injective (curry : (M ⊗[R] NM ⊗[R] N →ₗ[R] P) → M →ₗ[R] N →ₗ[R] P) :=
  fun _ _ H => ext H

Injectivity of Currying for Tensor Product Linear Maps

Informal description

The currying operation on linear maps from the tensor product $M \otimes_R N$ to $P$ is injective. That is, for any two $R$-linear maps $f, g \colon M \otimes_R N \to P$, if their curried versions $\text{curry}(f)$ and $\text{curry}(g)$ are equal as bilinear maps from $M$ to $N$ to $P$, then $f = g$.

TensorProduct.ext_threefold theorem

{g h : (M ⊗[R] N) ⊗[R] P →ₗ[R] Q} (H : ∀ x y z, g (x ⊗ₜ y ⊗ₜ z) = h (x ⊗ₜ y ⊗ₜ z)) : g = h

Full source

theorem ext_threefold {g h : (M ⊗[R] N) ⊗[R] P(M ⊗[R] N) ⊗[R] P →ₗ[R] Q}
    (H : ∀ x y z, g (x ⊗ₜ yx ⊗ₜ y ⊗ₜ z) = h (x ⊗ₜ yx ⊗ₜ y ⊗ₜ z)) : g = h := by
  ext x y z
  exact H x y z

Uniqueness of Linear Maps on Threefold Tensor Product via Evaluation on Pure Tensors

Informal description

Let $M$, $N$, $P$, and $Q$ be modules over a commutative semiring $R$. For any two linear maps $g, h \colon (M \otimes_R N) \otimes_R P \to Q$, if for all $x \in M$, $y \in N$, and $z \in P$ we have $g(x \otimes y \otimes z) = h(x \otimes y \otimes z)$, then $g = h$.

TensorProduct.ext_fourfold theorem

 {g h : ((M ⊗[R] N) ⊗[R] P) ⊗[R] Q →ₗ[R] S} (H : ∀ w x y z, g (w ⊗ₜ x ⊗ₜ y ⊗ₜ z) = h (w ⊗ₜ x ⊗ₜ y ⊗ₜ z)) : g = h

Full source

theorem ext_fourfold {g h : ((M ⊗[R] N) ⊗[R] P) ⊗[R] Q((M ⊗[R] N) ⊗[R] P) ⊗[R] Q →ₗ[R] S}
    (H : ∀ w x y z, g (w ⊗ₜ xw ⊗ₜ x ⊗ₜ yw ⊗ₜ x ⊗ₜ y ⊗ₜ z) = h (w ⊗ₜ xw ⊗ₜ x ⊗ₜ yw ⊗ₜ x ⊗ₜ y ⊗ₜ z)) : g = h := by
  ext w x y z
  exact H w x y z

Uniqueness of Fourfold Tensor Product Linear Maps via Evaluation on Pure Tensors

Informal description

Let $M$, $N$, $P$, $Q$, and $S$ be modules over a commutative semiring $R$. For any two linear maps $g, h \colon ((M \otimes_R N) \otimes_R P) \otimes_R Q \to S$, if for all $w \in M$, $x \in N$, $y \in P$, and $z \in Q$ we have $g(w \otimes x \otimes y \otimes z) = h(w \otimes x \otimes y \otimes z)$, then $g = h$.

TensorProduct.ext_fourfold' theorem

 {φ ψ : (M ⊗[R] N) ⊗[R] P ⊗[R] Q →ₗ[R] S} (H : ∀ w x y z, φ (w ⊗ₜ x ⊗ₜ (y ⊗ₜ z)) = ψ (w ⊗ₜ x ⊗ₜ (y ⊗ₜ z))) : φ = ψ

Full source

/-- Two linear maps (M ⊗ N) ⊗ (P ⊗ Q) → S which agree on all elements of the
form (m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q) are equal. -/
theorem ext_fourfold' {φ ψ : (M ⊗[R] N) ⊗[R] P ⊗[R] Q(M ⊗[R] N) ⊗[R] P ⊗[R] Q →ₗ[R] S}
    (H : ∀ w x y z, φ (w ⊗ₜ xw ⊗ₜ x ⊗ₜ (y ⊗ₜ z)) = ψ (w ⊗ₜ xw ⊗ₜ x ⊗ₜ (y ⊗ₜ z))) : φ = ψ := by
  ext m n p q
  exact H m n p q

Uniqueness of Linear Maps on Fourfold Tensor Product via Elementary Tensors

Informal description

Let $M$, $N$, $P$, $Q$, and $S$ be modules over a commutative semiring $R$. For any two linear maps $\varphi, \psi \colon (M \otimes_R N) \otimes_R (P \otimes_R Q) \to S$, if they agree on all elements of the form $(w \otimes x) \otimes (y \otimes z)$ for $w \in M$, $x \in N$, $y \in P$, $z \in Q$, then $\varphi = \psi$.

TensorProduct.comm_tmul theorem

(m : M) (n : N) : (TensorProduct.comm R M N) (m ⊗ₜ n) = n ⊗ₜ m

Full source

@[simp]
theorem comm_tmul (m : M) (n : N) : (TensorProduct.comm R M N) (m ⊗ₜ n) = n ⊗ₜ m :=
  rfl

Commutativity of Tensor Product: $\text{comm}(m \otimes n) = n \otimes m$

Informal description

For any elements $m \in M$ and $n \in N$, the commutativity isomorphism $\text{comm}_{R}(M, N)$ of the tensor product $M \otimes_R N$ satisfies $\text{comm}_{R}(M, N)(m \otimes n) = n \otimes m$.

TensorProduct.comm_symm_tmul theorem

(m : M) (n : N) : (TensorProduct.comm R M N).symm (n ⊗ₜ m) = m ⊗ₜ n

Full source

@[simp]
theorem comm_symm_tmul (m : M) (n : N) : (TensorProduct.comm R M N).symm (n ⊗ₜ m) = m ⊗ₜ n :=
  rfl

Inverse Commutativity Isomorphism for Tensor Product

Informal description

For any elements $m \in M$ and $n \in N$, the inverse of the commutativity isomorphism $\text{comm}_{R}(M, N)$ applied to the tensor product $n \otimes m$ equals $m \otimes n$. That is, $\text{comm}_{R}(M, N)^{-1}(n \otimes m) = m \otimes n$.

TensorProduct.lift_comp_comm_eq theorem

(f : M →ₗ[R] N →ₗ[R] P) : lift f ∘ₗ TensorProduct.comm R N M = lift f.flip

Full source

lemma lift_comp_comm_eq (f : M →ₗ[R] N →ₗ[R] P) :
    liftlift f ∘ₗ TensorProduct.comm R N M = lift f.flip :=
  ext rfl

Compatibility of Tensor Product Lift with Commutativity Isomorphism

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, and $P$ be $R$-modules. For any bilinear map $f \colon M \to_R N \to_R P$, the composition of the linear map $\text{lift}(f) \colon M \otimes_R N \to P$ with the commutativity isomorphism $\text{comm}_R(N, M) \colon N \otimes_R M \to M \otimes_R N$ is equal to the linear map $\text{lift}(f^\text{flip}) \colon N \otimes_R M \to P$, where $f^\text{flip}$ is the flipped bilinear map $N \to_R M \to_R P$. That is, \[ \text{lift}(f) \circ \text{comm}_R(N, M) = \text{lift}(f^\text{flip}). \]

TensorProduct.mapOfCompatibleSMul_tmul theorem

(m n) : mapOfCompatibleSMul R A M N (m ⊗ₜ n) = m ⊗ₜ n

Full source

@[simp] theorem mapOfCompatibleSMul_tmul (m n) : mapOfCompatibleSMul R A M N (m ⊗ₜ n) = m ⊗ₜ n :=
  rfl

Identity Property of `mapOfCompatibleSMul` on Tensor Products

Informal description

For any elements $m \in M$ and $n \in N$, the map `mapOfCompatibleSMul` applied to the tensor product $m \otimes n$ yields $m \otimes n$ itself.

TensorProduct.mapOfCompatibleSMul_surjective theorem

: Function.Surjective (mapOfCompatibleSMul R A M N)

Full source

theorem mapOfCompatibleSMul_surjective : Function.Surjective (mapOfCompatibleSMul R A M N) :=
  fun x ↦ x.induction_on (⟨0, map_zero _⟩) (fun m n ↦ ⟨_, mapOfCompatibleSMul_tmul ..⟩)
    fun _ _ ⟨x, hx⟩ ⟨y, hy⟩ ↦ ⟨x + y, by simpa using congr($hx + $hy)⟩

Surjectivity of `mapOfCompatibleSMul` on Tensor Products

Informal description

The linear map `mapOfCompatibleSMul R A M N` from the tensor product $M \otimes_R N$ to itself is surjective. That is, for every element $z \in M \otimes_R N$, there exists an element $w \in M \otimes_R N$ such that `mapOfCompatibleSMul R A M N w = z`.

TensorProduct.map_tmul theorem

(f : M →ₗ[R] P) (g : N →ₗ[R] Q) (m : M) (n : N) : map f g (m ⊗ₜ n) = f m ⊗ₜ g n

Full source

@[simp]
theorem map_tmul (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (m : M) (n : N) : map f g (m ⊗ₜ n) = f m ⊗ₜ g n :=
  rfl

Tensor Product Map Evaluates as $f(m) \otimes g(n)$ on Pure Tensors

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, and $Q$ be modules over $R$. Given linear maps $f : M \to P$ and $g : N \to Q$ over $R$, the tensor product map $\text{map}(f, g) : M \otimes_R N \to P \otimes_R Q$ satisfies $\text{map}(f, g)(m \otimes n) = f(m) \otimes g(n)$ for all $m \in M$ and $n \in N$.

TensorProduct.map_comp_comm_eq theorem

 (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : map f g ∘ₗ TensorProduct.comm R N M = TensorProduct.comm R Q P ∘ₗ map g f

Full source

/-- Given linear maps `f : M → P`, `g : N → Q`, if we identify `M ⊗ N` with `N ⊗ M` and `P ⊗ Q`
with `Q ⊗ P`, then this lemma states that `f ⊗ g = g ⊗ f`. -/
lemma map_comp_comm_eq (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
    mapmap f g ∘ₗ TensorProduct.comm R N M = TensorProduct.commTensorProduct.comm R Q P ∘ₗ map g f :=
  ext rfl

Commutativity of Tensor Product Map with Commutativity Isomorphism

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, and $Q$ be modules over $R$. Given linear maps $f \colon M \to P$ and $g \colon N \to Q$ over $R$, the composition of the tensor product map $f \otimes g$ with the commutativity isomorphism $\text{comm}_{R} \colon N \otimes_R M \to M \otimes_R N$ is equal to the composition of the commutativity isomorphism $\text{comm}_{R} \colon Q \otimes_R P \to P \otimes_R Q$ with the tensor product map $g \otimes f$. In other words, the following diagram commutes: \[ (f \otimes g) \circ \text{comm}_{R} = \text{comm}_{R} \circ (g \otimes f). \]

TensorProduct.map_comm theorem

 (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (x : N ⊗[R] M) :
  map f g (TensorProduct.comm R N M x) = TensorProduct.comm R Q P (map g f x)

Full source

lemma map_comm (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (x : N ⊗[R] M) :
    map f g (TensorProduct.comm R N M x) = TensorProduct.comm R Q P (map g f x) :=
  DFunLike.congr_fun (map_comp_comm_eq _ _) _

Commutativity of Tensor Product Map with Commutativity Isomorphism

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, and $Q$ be $R$-modules. Given $R$-linear maps $f \colon M \to P$ and $g \colon N \to Q$, and an element $x \in N \otimes_R M$, the following equality holds: \[ (f \otimes g)(\text{comm}_{R}(x)) = \text{comm}_{R}(g \otimes f)(x), \] where $\text{comm}_{R} \colon N \otimes_R M \to M \otimes_R N$ and $\text{comm}_{R} \colon Q \otimes_R P \to P \otimes_R Q$ are the commutativity isomorphisms of the tensor product.

TensorProduct.map_range_eq_span_tmul theorem

(f : M →ₗ[R] P) (g : N →ₗ[R] Q) : range (map f g) = Submodule.span R {t | ∃ m n, f m ⊗ₜ g n = t}

Full source

theorem map_range_eq_span_tmul (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
    range (map f g) = Submodule.span R { t | ∃ m n, f m ⊗ₜ g n = t } := by
  simp only [← Submodule.map_top, ← span_tmul_eq_top, Submodule.map_span, Set.mem_image,
    Set.mem_setOf_eq]
  congr; ext t
  constructor
  · rintro ⟨_, ⟨⟨m, n, rfl⟩, rfl⟩⟩
    use m, n
    simp only [map_tmul]
  · rintro ⟨m, n, rfl⟩
    refine ⟨_, ⟨⟨m, n, rfl⟩, ?_⟩⟩
    simp only [map_tmul]

Range of Tensor Product Map Equals Span of Elementary Tensors

Informal description

For any $R$-linear maps $f \colon M \to P$ and $g \colon N \to Q$, the range of the tensor product map $f \otimes g \colon M \otimes_R N \to P \otimes_R Q$ is equal to the $R$-linear span of the set $\{ f(m) \otimes g(n) \mid m \in M, n \in N \}$.

TensorProduct.range_mapIncl theorem

 (p : Submodule R P) (q : Submodule R Q) : LinearMap.range (mapIncl p q) = Submodule.span R (Set.image2 (· ⊗ₜ ·) p q)

Full source

lemma range_mapIncl (p : Submodule R P) (q : Submodule R Q) :
    LinearMap.range (mapIncl p q) = Submodule.span R (Set.image2 (· ⊗ₜ ·) p q) := by
  rw [mapIncl, map_range_eq_span_tmul]
  congr; ext; simp

Range of Tensor Product Inclusion Map Equals Span of Elementary Tensors

Informal description

Let $R$ be a commutative semiring, and let $P$ and $Q$ be $R$-modules with submodules $p \subseteq P$ and $q \subseteq Q$. The range of the inclusion map $\text{mapIncl}(p, q) \colon p \otimes_R q \to P \otimes_R Q$ is equal to the $R$-linear span of the set $\{x \otimes y \mid x \in p, y \in q\}$.

TensorProduct.map₂_eq_range_lift_comp_mapIncl theorem

 (f : P →ₗ[R] Q →ₗ[R] M) (p : Submodule R P) (q : Submodule R Q) :
  Submodule.map₂ f p q = LinearMap.range (lift f ∘ₗ mapIncl p q)

Full source

theorem map₂_eq_range_lift_comp_mapIncl (f : P →ₗ[R] Q →ₗ[R] M)
    (p : Submodule R P) (q : Submodule R Q) :
    Submodule.map₂ f p q = LinearMap.range (liftlift f ∘ₗ mapIncl p q) := by
  simp_rw [LinearMap.range_comp, range_mapIncl, Submodule.map_span,
    Set.image_image2, Submodule.map₂_eq_span_image2, lift.tmul]

Image of Bilinear Map Equals Range of Tensor Lift Composition

Informal description

Let $R$ be a commutative semiring, $P$ and $Q$ be $R$-modules with submodules $p \subseteq P$ and $q \subseteq Q$, and $f : P \to_R Q \to_R M$ be a bilinear map. Then the image of the bilinear map $f$ restricted to $p \times q$ is equal to the range of the composition of the tensor product lift of $f$ with the inclusion map from $p \otimes_R q$ to $P \otimes_R Q$. In symbols: \[ \text{map}_2(f, p, q) = \text{range}(\text{lift}(f) \circ \text{mapIncl}(p, q)) \]

TensorProduct.map_comp theorem

 (f₂ : P →ₗ[R] P') (f₁ : M →ₗ[R] P) (g₂ : Q →ₗ[R] Q') (g₁ : N →ₗ[R] Q) :
  map (f₂.comp f₁) (g₂.comp g₁) = (map f₂ g₂).comp (map f₁ g₁)

Full source

theorem map_comp (f₂ : P →ₗ[R] P') (f₁ : M →ₗ[R] P) (g₂ : Q →ₗ[R] Q') (g₁ : N →ₗ[R] Q) :
    map (f₂.comp f₁) (g₂.comp g₁) = (map f₂ g₂).comp (map f₁ g₁) :=
  ext' fun _ _ => rfl

Composition of Tensor Product Maps

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, $P'$, $Q$, $Q'$ be $R$-modules. Given linear maps $f_1: M \to P$, $f_2: P \to P'$, $g_1: N \to Q$, and $g_2: Q \to Q'$, the composition of the tensor product maps satisfies: \[ \text{map}(f_2 \circ f_1, g_2 \circ g_1) = \text{map}(f_2, g_2) \circ \text{map}(f_1, g_1) \] where $\text{map}(f,g)$ denotes the induced linear map on the tensor product spaces.

TensorProduct.range_mapIncl_mono theorem

 {p p' : Submodule R P} {q q' : Submodule R Q} (hp : p ≤ p') (hq : q ≤ q') :
  LinearMap.range (mapIncl p q) ≤ LinearMap.range (mapIncl p' q')

Full source

lemma range_mapIncl_mono {p p' : Submodule R P} {q q' : Submodule R Q} (hp : p ≤ p') (hq : q ≤ q') :
    LinearMap.range (mapIncl p q) ≤ LinearMap.range (mapIncl p' q') := by
  simp_rw [range_mapIncl]
  exact Submodule.span_mono (Set.image2_subset hp hq)

Monotonicity of Range for Tensor Product Inclusion Maps: $p \leq p' \land q \leq q' \Rightarrow \text{range}(\text{mapIncl}(p, q)) \leq \text{range}(\text{mapIncl}(p', q'))$

Informal description

Let $R$ be a commutative semiring, and let $P$ and $Q$ be $R$-modules with submodules $p, p' \subseteq P$ and $q, q' \subseteq Q$. If $p \leq p'$ and $q \leq q'$, then the range of the inclusion map $\text{mapIncl}(p, q) \colon p \otimes_R q \to P \otimes_R Q$ is contained in the range of the inclusion map $\text{mapIncl}(p', q') \colon p' \otimes_R q' \to P \otimes_R Q$.

TensorProduct.lift_comp_map theorem

 (i : P →ₗ[R] Q →ₗ[R] Q') (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : (lift i).comp (map f g) = lift ((i.comp f).compl₂ g)

Full source

theorem lift_comp_map (i : P →ₗ[R] Q →ₗ[R] Q') (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
    (lift i).comp (map f g) = lift ((i.comp f).compl₂ g) :=
  ext' fun _ _ => rfl

Composition of Tensor Product Lift with Map Equals Lift of Composed Bilinear Map

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, $Q$, $Q'$ be $R$-modules. Given a bilinear map $i \colon P \to_R Q \to_R Q'$ and linear maps $f \colon M \to_R P$, $g \colon N \to_R Q$, the composition of the induced linear map $\text{lift}(i) \colon P \otimes_R Q \to Q'$ with the tensor product map $\text{map}(f,g) \colon M \otimes_R N \to P \otimes_R Q$ equals the linear map induced by the bilinear map $(i \circ f) \circ g \colon M \to_R N \to_R Q'$. In symbols: $$(\text{lift}(i)) \circ (\text{map}(f,g)) = \text{lift}((i \circ f) \circ g)$$

TensorProduct.map_id theorem

: map (id : M →ₗ[R] M) (id : N →ₗ[R] N) = .id

Full source

@[simp]
theorem map_id : map (id : M →ₗ[R] M) (id : N →ₗ[R] N) = .id := by
  ext
  simp only [mk_apply, id_coe, compr₂_apply, _root_.id, map_tmul]

Tensor Product Map of Identity Maps is Identity

Informal description

Let $R$ be a commutative semiring, and let $M$ and $N$ be $R$-modules. The tensor product map induced by the identity linear maps $\text{id}_M \colon M \to M$ and $\text{id}_N \colon N \to N$ is equal to the identity map on $M \otimes_R N$. In symbols: \[ \text{map}(\text{id}_M, \text{id}_N) = \text{id}_{M \otimes_R N} \]

TensorProduct.map_one theorem

: map (1 : M →ₗ[R] M) (1 : N →ₗ[R] N) = 1

Full source

@[simp]
protected theorem map_one : map (1 : M →ₗ[R] M) (1 : N →ₗ[R] N) = 1 :=
  map_id

Tensor Product Map of Identity Maps is Identity

Informal description

Let $R$ be a commutative semiring, and let $M$ and $N$ be $R$-modules. The tensor product map induced by the identity linear maps $1_M \colon M \to M$ and $1_N \colon N \to N$ is equal to the identity map on $M \otimes_R N$. In symbols: \[ \text{map}(1_M, 1_N) = 1_{M \otimes_R N} \]

TensorProduct.map_mul theorem

 (f₁ f₂ : M →ₗ[R] M) (g₁ g₂ : N →ₗ[R] N) : map (f₁ * f₂) (g₁ * g₂) = map f₁ g₁ * map f₂ g₂

Full source

protected theorem map_mul (f₁ f₂ : M →ₗ[R] M) (g₁ g₂ : N →ₗ[R] N) :
    map (f₁ * f₂) (g₁ * g₂) = map f₁ g₁ * map f₂ g₂ :=
  map_comp f₁ f₂ g₁ g₂

Composition Property of Tensor Product Maps: $\text{map}(f₁ \circ f₂, g₁ \circ g₂) = \text{map}(f₁, g₁) \circ \text{map}(f₂, g₂)$

Informal description

Let $R$ be a commutative semiring, and let $M$ and $N$ be $R$-modules. For any linear maps $f₁, f₂: M \to M$ and $g₁, g₂: N \to N$, the tensor product map satisfies: \[ \text{map}(f₁ \circ f₂, g₁ \circ g₂) = \text{map}(f₁, g₁) \circ \text{map}(f₂, g₂) \] where $\text{map}(f,g)$ denotes the induced linear map on the tensor product $M \otimes_R N$.

TensorProduct.map_pow theorem

(f : M →ₗ[R] M) (g : N →ₗ[R] N) (n : ℕ) : map f g ^ n = map (f ^ n) (g ^ n)

Full source

@[simp]
protected theorem map_pow (f : M →ₗ[R] M) (g : N →ₗ[R] N) (n : ℕ) :
    map f g ^ n = map (f ^ n) (g ^ n) := by
  induction n with
  | zero => simp only [pow_zero, TensorProduct.map_one]
  | succ n ih => simp only [pow_succ', ih, TensorProduct.map_mul]

Power of Tensor Product Map Equals Tensor Product of Powers: $(\text{map}(f, g))^n = \text{map}(f^n, g^n)$

Informal description

Let $R$ be a commutative semiring, and let $M$ and $N$ be $R$-modules. For any linear maps $f \colon M \to M$ and $g \colon N \to N$, and any natural number $n$, the $n$-th power of the tensor product map $\text{map}(f, g)$ equals the tensor product map of the $n$-th powers of $f$ and $g$. That is: \[ (\text{map}(f, g))^n = \text{map}(f^n, g^n) \]

TensorProduct.map_add_left theorem

(f₁ f₂ : M →ₗ[R] P) (g : N →ₗ[R] Q) : map (f₁ + f₂) g = map f₁ g + map f₂ g

Full source

theorem map_add_left (f₁ f₂ : M →ₗ[R] P) (g : N →ₗ[R] Q) :
    map (f₁ + f₂) g = map f₁ g + map f₂ g := by
  ext
  simp only [add_tmul, compr₂_apply, mk_apply, map_tmul, add_apply]

Additivity of Tensor Product Map in First Argument: $\text{map}(f_1 + f_2, g) = \text{map}(f_1, g) + \text{map}(f_2, g)$

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, and $Q$ be $R$-modules. For any linear maps $f_1, f_2 \colon M \to P$ and $g \colon N \to Q$, the tensor product map satisfies: \[ \text{map}(f_1 + f_2, g) = \text{map}(f_1, g) + \text{map}(f_2, g) \] where $\text{map}(f,g)$ denotes the induced linear map on the tensor product $M \otimes_R N$.

TensorProduct.map_add_right theorem

(f : M →ₗ[R] P) (g₁ g₂ : N →ₗ[R] Q) : map f (g₁ + g₂) = map f g₁ + map f g₂

Full source

theorem map_add_right (f : M →ₗ[R] P) (g₁ g₂ : N →ₗ[R] Q) :
    map f (g₁ + g₂) = map f g₁ + map f g₂ := by
  ext
  simp only [tmul_add, compr₂_apply, mk_apply, map_tmul, add_apply]

Tensor Product Map Additivity in Second Argument: $\text{map}_f (g_1 + g_2) = \text{map}_f g_1 + \text{map}_f g_2$

Informal description

For any linear map $f \colon M \to_{[R]} P$ and any linear maps $g_1, g_2 \colon N \to_{[R]} Q$ over a commutative semiring $R$, the tensor product map satisfies the additivity property in the second argument: \[ \text{map}_f (g_1 + g_2) = \text{map}_f g_1 + \text{map}_f g_2. \]

TensorProduct.map_smul_left theorem

(r : R) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : map (r • f) g = r • map f g

Full source

theorem map_smul_left (r : R) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : map (r • f) g = r • map f g := by
  ext
  simp only [smul_tmul, compr₂_apply, mk_apply, map_tmul, smul_apply, tmul_smul]

Linearity of Tensor Product Map in First Argument: $\text{map}(r \cdot f, g) = r \cdot \text{map}(f, g)$

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, and $Q$ be modules over $R$. For any scalar $r \in R$ and linear maps $f \colon M \to P$ and $g \colon N \to Q$, the tensor product map satisfies: \[ \text{map}(r \cdot f, g) = r \cdot \text{map}(f, g) \] where $\text{map}(f, g) \colon M \otimes_R N \to P \otimes_R Q$ is the linear map induced by $f$ and $g$.

TensorProduct.map_smul_right theorem

(r : R) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : map f (r • g) = r • map f g

Full source

theorem map_smul_right (r : R) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : map f (r • g) = r • map f g := by
  ext
  simp only [smul_tmul, compr₂_apply, mk_apply, map_tmul, smul_apply, tmul_smul]

Tensor product map is linear in the second argument: $\text{map}_f (r \cdot g) = r \cdot \text{map}_f g$

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, $Q$ be $R$-modules. For any scalar $r \in R$, any linear map $f \colon M \to P$, and any linear map $g \colon N \to Q$, the tensor product map satisfies: \[ \text{map}_f (r \cdot g) = r \cdot \text{map}_f g \] where $\text{map}_f g$ denotes the tensor product of the maps $f$ and $g$.

TensorProduct.mapBilinear_apply theorem

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

Full source

@[simp]
theorem mapBilinear_apply (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : mapBilinear R M N P Q f g = map f g :=
  rfl

Equality of Bilinear Map and Tensor Product Map: $\text{mapBilinear}(f, g) = \text{map}(f, g)$

Informal description

For any $R$-linear maps $f \colon M \to P$ and $g \colon N \to Q$, the bilinear map $\text{mapBilinear}_R^{M,N,P,Q}(f, g)$ is equal to the tensor product map $\text{map}(f, g) \colon M \otimes_R N \to P \otimes_R Q$.

TensorProduct.lTensorHomToHomLTensor_apply theorem

(p : P) (f : M →ₗ[R] Q) (m : M) : lTensorHomToHomLTensor R M P Q (p ⊗ₜ f) m = p ⊗ₜ f m

Full source

@[simp]
theorem lTensorHomToHomLTensor_apply (p : P) (f : M →ₗ[R] Q) (m : M) :
    lTensorHomToHomLTensor R M P Q (p ⊗ₜ f) m = p ⊗ₜ f m :=
  rfl

Application of Left Tensor-Hom to Hom-Left Tensor Map: $p \otimes f$ applied to $m$ equals $p \otimes f(m)$

Informal description

For any element $p \in P$, any linear map $f \colon M \to Q$, and any element $m \in M$, the application of the linear map $\text{lTensorHomToHomLTensor}_R^{M,P,Q}(p \otimes f)$ to $m$ is equal to $p \otimes f(m)$.

TensorProduct.rTensorHomToHomRTensor_apply theorem

(f : M →ₗ[R] P) (q : Q) (m : M) : rTensorHomToHomRTensor R M P Q (f ⊗ₜ q) m = f m ⊗ₜ q

Full source

@[simp]
theorem rTensorHomToHomRTensor_apply (f : M →ₗ[R] P) (q : Q) (m : M) :
    rTensorHomToHomRTensor R M P Q (f ⊗ₜ q) m = f m ⊗ₜ q :=
  rfl

Right Tensor Homomorphism to Homomorphism Right Tensor Map Evaluation

Informal description

For any $R$-linear map $f \colon M \to P$, any element $q \in Q$, and any $m \in M$, the application of the right tensor homomorphism to homomorphism right tensor map satisfies: \[ \text{rTensorHomToHomRTensor}_R^{M,P,Q}(f \otimes q)(m) = f(m) \otimes q. \]

TensorProduct.homTensorHomMap_apply theorem

(f : M →ₗ[R] P) (g : N →ₗ[R] Q) : homTensorHomMap R M N P Q (f ⊗ₜ g) = map f g

Full source

@[simp]
theorem homTensorHomMap_apply (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
    homTensorHomMap R M N P Q (f ⊗ₜ g) = map f g :=
  rfl

Hom-Tensor-Hom Map Evaluation: $\text{homTensorHomMap}(f \otimes g) = \text{map}(f, g)$

Informal description

For any $R$-linear maps $f \colon M \to P$ and $g \colon N \to Q$, the homomorphism tensor homomorphism map satisfies: \[ \text{homTensorHomMap}_R^{M,N,P,Q}(f \otimes g) = \text{map}(f, g). \]

TensorProduct.map₂_apply_tmul theorem

 (f : M →ₗ[R] P →ₗ[R] Q) (g : N →ₗ[R] S →ₗ[R] T) (m : M) (n : N) : map₂ f g (m ⊗ₜ n) = map (f m) (g n)

Full source

@[simp]
theorem map₂_apply_tmul (f : M →ₗ[R] P →ₗ[R] Q) (g : N →ₗ[R] S →ₗ[R] T) (m : M) (n : N) :
    map₂ f g (m ⊗ₜ n) = map (f m) (g n) := rfl

Evaluation of Bilinear Tensor Product Map on Simple Tensors: $\text{map}_2(f,g)(m \otimes n) = \text{map}(f(m), g(n))$

Informal description

For any $R$-linear maps $f \colon M \to P \to_{[R]} Q$ and $g \colon N \to S \to_{[R]} T$, and any elements $m \in M$, $n \in N$, the bilinear tensor product map satisfies: \[ \text{map}_2(f, g)(m \otimes n) = \text{map}(f(m), g(n)) \] where $m \otimes n$ denotes the tensor product of $m$ and $n$, and $\text{map}(f(m), g(n))$ is the tensor product of the linear maps $f(m)$ and $g(n)$.

TensorProduct.map_zero_left theorem

(g : N →ₗ[R] Q) : map (0 : M →ₗ[R] P) g = 0

Full source

@[simp]
theorem map_zero_left (g : N →ₗ[R] Q) : map (0 : M →ₗ[R] P) g = 0 :=
  (mapBilinear R M N P Q).map_zero₂ _

Tensor product with zero map on the left is zero

Informal description

For any linear map $g \colon N \to_{[R]} Q$, the tensor product map $\text{map}(0, g)$ is equal to the zero map, where $0$ denotes the zero linear map from $M$ to $P$.

TensorProduct.map_zero_right theorem

(f : M →ₗ[R] P) : map f (0 : N →ₗ[R] Q) = 0

Full source

@[simp]
theorem map_zero_right (f : M →ₗ[R] P) : map f (0 : N →ₗ[R] Q) = 0 :=
  (mapBilinear R M N P Q _).map_zero

Tensor product map with zero right map is zero

Informal description

For any $R$-linear map $f \colon M \to P$, the tensor product map $\text{map}(f, 0)$ is equal to the zero map, where $0$ denotes the zero map from $N$ to $Q$.

TensorProduct.congr_tmul theorem

(f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (m : M) (n : N) : congr f g (m ⊗ₜ n) = f m ⊗ₜ g n

Full source

@[simp]
theorem congr_tmul (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (m : M) (n : N) :
    congr f g (m ⊗ₜ n) = f m ⊗ₜ g n :=
  rfl

Tensor Product Congruence Preserves Tensor Product of Elements

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, $Q$ be modules over $R$. Given linear equivalences $f: M \simeq P$ and $g: N \simeq Q$, and elements $m \in M$, $n \in N$, the tensor product congruence map $\text{congr}(f,g)$ satisfies $\text{congr}(f,g)(m \otimes n) = f(m) \otimes g(n)$.

TensorProduct.congr_symm_tmul theorem

(f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (p : P) (q : Q) : (congr f g).symm (p ⊗ₜ q) = f.symm p ⊗ₜ g.symm q

Full source

@[simp]
theorem congr_symm_tmul (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (p : P) (q : Q) :
    (congr f g).symm (p ⊗ₜ q) = f.symm p ⊗ₜ g.symm q :=
  rfl

Inverse Tensor Product Congruence Preserves Tensor Product Structure

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, $Q$ be $R$-modules. Given linear equivalences $f: M \simeq P$ and $g: N \simeq Q$, for any elements $p \in P$ and $q \in Q$, the inverse of the tensor product congruence map $(f \otimes g)^{-1}$ applied to $p \otimes q$ equals $f^{-1}(p) \otimes g^{-1}(q)$. In symbols: $$(f \otimes g)^{-1}(p \otimes q) = f^{-1}(p) \otimes g^{-1}(q).$$

TensorProduct.congr_symm theorem

(f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) : (congr f g).symm = congr f.symm g.symm

Full source

theorem congr_symm (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) : (congr f g).symm = congr f.symm g.symm := rfl

Inverse of Tensor Product Equivalence Equals Tensor Product of Inverses

Informal description

Given linear equivalences $f \colon M \simeq P$ and $g \colon N \simeq Q$ over a commutative semiring $R$, the inverse of the tensor product equivalence $\text{congr}(f, g) \colon M \otimes_R N \simeq P \otimes_R Q$ is equal to the tensor product equivalence of the inverses, $\text{congr}(f^{-1}, g^{-1})$.

TensorProduct.congr_refl_refl theorem

: congr (.refl R M) (.refl R N) = .refl R _

Full source

@[simp] theorem congr_refl_refl : congr (.refl R M) (.refl R N) = .refl R _ :=
  LinearEquiv.toLinearMap_injective <| ext' fun _ _ ↦ rfl

Tensor Product of Identity Maps is Identity

Informal description

The tensor product of the identity linear equivalences on $M$ and $N$ over a commutative semiring $R$ is equal to the identity linear equivalence on $M \otimes_R N$. That is, $\text{congr}(\text{refl}_R M, \text{refl}_R N) = \text{refl}_R (M \otimes_R N)$.

TensorProduct.congr_trans theorem

 (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (f' : P ≃ₗ[R] S) (g' : Q ≃ₗ[R] T) :
  congr (f ≪≫ₗ f') (g ≪≫ₗ g') = congr f g ≪≫ₗ congr f' g'

Full source

theorem congr_trans (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (f' : P ≃ₗ[R] S) (g' : Q ≃ₗ[R] T) :
    congr (f ≪≫ₗ f') (g ≪≫ₗ g') = congrcongr f g ≪≫ₗ congr f' g' :=
  LinearEquiv.toLinearMap_injective <| map_comp _ _ _ _

Composition of Tensor Product Isomorphisms

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, $Q$, $S$, $T$ be $R$-modules. Given linear isomorphisms $f: M \simeq P$, $g: N \simeq Q$, $f': P \simeq S$, and $g': Q \simeq T$, the following equality holds for the tensor product of composed isomorphisms: \[ \text{congr}(f \circ f', g \circ g') = \text{congr}(f, g) \circ \text{congr}(f', g') \] where $\text{congr}$ denotes the induced isomorphism on tensor product spaces and $\circ$ denotes composition of isomorphisms.

TensorProduct.congr_mul theorem

 (f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (f' : M ≃ₗ[R] M) (g' : N ≃ₗ[R] N) : congr (f * f') (g * g') = congr f g * congr f' g'

Full source

theorem congr_mul (f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (f' : M ≃ₗ[R] M) (g' : N ≃ₗ[R] N) :
    congr (f * f') (g * g') = congr f g * congr f' g' := congr_trans _ _ _ _

Composition of Tensor Product Automorphisms: $\text{congr}(f \circ f', g \circ g') = \text{congr}(f, g) \circ \text{congr}(f', g')$

Informal description

Let $R$ be a commutative semiring, and let $M$ and $N$ be $R$-modules. Given linear automorphisms $f, f'$ of $M$ and $g, g'$ of $N$, the following equality holds for the tensor product of composed automorphisms: \[ \text{congr}(f \circ f', g \circ g') = \text{congr}(f, g) \circ \text{congr}(f', g') \] where $\text{congr}$ denotes the induced automorphism on the tensor product space $M \otimes_R N$ and $\circ$ denotes composition of automorphisms.

TensorProduct.congr_pow theorem

(f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (n : ℕ) : congr f g ^ n = congr (f ^ n) (g ^ n)

Full source

@[simp] theorem congr_pow (f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (n : ℕ) :
    congr f g ^ n = congr (f ^ n) (g ^ n) := by
  induction n with
  | zero => exact congr_refl_refl.symm
  | succ n ih => simp_rw [pow_succ, ih, congr_mul]

Power of Tensor Product Automorphism: $(\text{congr}(f, g))^n = \text{congr}(f^n, g^n)$

Informal description

Let $R$ be a commutative semiring, and let $M$ and $N$ be $R$-modules. For any linear automorphisms $f$ of $M$ and $g$ of $N$, and any natural number $n$, the $n$-th power of the induced automorphism $\text{congr}(f, g)$ on $M \otimes_R N$ equals the induced automorphism of the $n$-th powers of $f$ and $g$. That is, \[ (\text{congr}(f, g))^n = \text{congr}(f^n, g^n). \]

TensorProduct.congr_zpow theorem

(f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (n : ℤ) : congr f g ^ n = congr (f ^ n) (g ^ n)

Full source

@[simp] theorem congr_zpow (f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (n : ℤ) :
    congr f g ^ n = congr (f ^ n) (g ^ n) := by
  cases n with
  | ofNat n => exact congr_pow _ _ _
  | negSucc n => simp_rw [zpow_negSucc, congr_pow]; exact congr_symm _ _

Integer Power of Tensor Product Automorphism: $(\text{congr}(f, g))^n = \text{congr}(f^n, g^n)$

Informal description

Let $R$ be a commutative semiring, and let $M$ and $N$ be $R$-modules. For any linear automorphisms $f$ of $M$ and $g$ of $N$, and any integer $n$, the $n$-th power of the induced automorphism $\text{congr}(f, g)$ on $M \otimes_R N$ equals the induced automorphism of the $n$-th powers of $f$ and $g$. That is, \[ (\text{congr}(f, g))^n = \text{congr}(f^n, g^n). \]

LinearMap.lTensor_def theorem

: f.lTensor M = TensorProduct.map LinearMap.id f

Full source

theorem lTensor_def : f.lTensor M = TensorProduct.map LinearMap.id f := rfl

Definition of Left Tensor Product of Linear Map

Informal description

For any linear map $f$ and module $M$, the left tensor product of $f$ with $M$ is equal to the tensor product map of the identity linear map on $M$ with $f$. That is, $f \otimes_{\text{left}} M = \text{id}_M \otimes f$.

LinearMap.rTensor_def theorem

: f.rTensor M = TensorProduct.map f LinearMap.id

Full source

theorem rTensor_def : f.rTensor M = TensorProduct.map f LinearMap.id := rfl

Definition of Right Tensor Product of Linear Map

Informal description

For any linear map $f \colon N \to P$ and module $M$, the right tensor product of $f$ with $M$ is equal to the tensor product map of $f$ with the identity linear map on $M$. That is, $f \otimes_{\text{right}} M = f \otimes \text{id}_M$.

LinearMap.lTensor_tmul theorem

(m : M) (n : N) : f.lTensor M (m ⊗ₜ n) = m ⊗ₜ f n

Full source

@[simp]
theorem lTensor_tmul (m : M) (n : N) : f.lTensor M (m ⊗ₜ n) = m ⊗ₜ f n :=
  rfl

Left Tensor Product Action on Elementary Tensors

Informal description

For any linear map $f \colon N \to P$ and elements $m \in M$, $n \in N$, the left tensor product map $f \otimes \mathrm{id}_M$ applied to the tensor product $m \otimes n$ equals $m \otimes f(n)$, i.e., $$(f \otimes \mathrm{id}_M)(m \otimes n) = m \otimes f(n).$$

LinearMap.rTensor_tmul theorem

(m : M) (n : N) : f.rTensor M (n ⊗ₜ m) = f n ⊗ₜ m

Full source

@[simp]
theorem rTensor_tmul (m : M) (n : N) : f.rTensor M (n ⊗ₜ m) = f n ⊗ₜ m :=
  rfl

Right Tensor Product Action on Elementary Tensors

Informal description

For any linear map $f \colon N \to P$ and elements $m \in M$, $n \in N$, the right tensor product map $\mathrm{id}_M \otimes f$ applied to the tensor product $n \otimes m$ equals $f(n) \otimes m$, i.e., $$(\mathrm{id}_M \otimes f)(n \otimes m) = f(n) \otimes m.$$

LinearMap.lTensor_comp_mk theorem

(m : M) : f.lTensor M ∘ₗ TensorProduct.mk R M N m = TensorProduct.mk R M P m ∘ₗ f

Full source

@[simp]
theorem lTensor_comp_mk (m : M) :
    f.lTensor M ∘ₗ TensorProduct.mk R M N m = TensorProduct.mkTensorProduct.mk R M P m ∘ₗ f :=
  rfl

Commutativity of Left Tensor Product with Canonical Bilinear Map

Informal description

For any linear map $f \colon N \to P$ and element $m \in M$, the composition of the left tensor product map $f \otimes \mathrm{id}_M$ with the canonical bilinear map $\mathrm{mk}_R \colon M \to N \to M \otimes_R N$ evaluated at $m$ equals the composition of the canonical bilinear map $\mathrm{mk}_R \colon M \to P \to M \otimes_R P$ evaluated at $m$ with $f$. In other words, the following diagram commutes: $$(f \otimes \mathrm{id}_M) \circ \mathrm{mk}_R(m) = \mathrm{mk}_R(m) \circ f.$$

LinearMap.rTensor_comp_flip_mk theorem

(m : M) : f.rTensor M ∘ₗ (TensorProduct.mk R N M).flip m = (TensorProduct.mk R P M).flip m ∘ₗ f

Full source

@[simp]
theorem rTensor_comp_flip_mk (m : M) :
    f.rTensor M ∘ₗ (TensorProduct.mk R N M).flip m = (TensorProduct.mk R P M).flip m ∘ₗ f :=
  rfl

Commutativity of Right Tensor Product with Flipped Tensor Map

Informal description

For any element $m \in M$, the composition of the right tensor product map $f \otimes_R M$ with the flipped tensor product map $(N \otimes_R M \to M \otimes_R N).flip$ applied to $m$ is equal to the composition of the flipped tensor product map $(P \otimes_R M \to M \otimes_R P).flip$ applied to $m$ with the linear map $f$. In other words, the following diagram commutes: $$(f \otimes_R M) \circ (\text{flip} \circ \text{mk}_{N,M})(m) = (\text{flip} \circ \text{mk}_{P,M})(m) \circ f$$

LinearMap.comm_comp_rTensor_comp_comm_eq theorem

(g : N →ₗ[R] P) : TensorProduct.comm R P Q ∘ₗ rTensor Q g ∘ₗ TensorProduct.comm R Q N = lTensor Q g

Full source

lemma comm_comp_rTensor_comp_comm_eq (g : N →ₗ[R] P) :
    TensorProduct.commTensorProduct.comm R P Q ∘ₗ rTensor Q g ∘ₗ TensorProduct.comm R Q N =
      lTensor Q g :=
  TensorProduct.ext rfl

Commutativity of Tensor Product with Right Tensor Map via Commutativity Isomorphism

Informal description

For any linear map $g \colon N \to P$ between modules over a commutative semiring $R$, the composition of the tensor product commutativity map $\text{comm}_{R,P,Q} \colon P \otimes_R Q \to Q \otimes_R P$, the right tensor product map $g \otimes_R Q$, and the tensor product commutativity map $\text{comm}_{R,Q,N} \colon Q \otimes_R N \to N \otimes_R Q$ equals the left tensor product map $Q \otimes_R g$. In other words, the following diagram commutes: $$\text{comm}_{R,P,Q} \circ (g \otimes_R Q) \circ \text{comm}_{R,Q,N} = Q \otimes_R g.$$

LinearMap.comm_comp_lTensor_comp_comm_eq theorem

(g : N →ₗ[R] P) : TensorProduct.comm R Q P ∘ₗ lTensor Q g ∘ₗ TensorProduct.comm R N Q = rTensor Q g

Full source

lemma comm_comp_lTensor_comp_comm_eq (g : N →ₗ[R] P) :
    TensorProduct.commTensorProduct.comm R Q P ∘ₗ lTensor Q g ∘ₗ TensorProduct.comm R N Q =
      rTensor Q g :=
  TensorProduct.ext rfl

Commutativity of Left Tensor Product with Commutativity Isomorphisms

Informal description

Let $R$ be a commutative semiring, and let $N$, $P$, and $Q$ be $R$-modules. For any $R$-linear map $g \colon N \to P$, the following composition of linear maps equals the right tensor product map $g \otimes Q$: $$\text{comm}_{Q,P} \circ (Q \otimes g) \circ \text{comm}_{N,Q} = g \otimes Q$$ where $\text{comm}_{A,B} \colon A \otimes_R B \to B \otimes_R A$ is the tensor product commutativity isomorphism.

LinearMap.lTensor_inj_iff_rTensor_inj theorem

: Function.Injective (lTensor M f) ↔ Function.Injective (rTensor M f)

Full source

/-- Given a linear map `f : N → P`, `f ⊗ M` is injective if and only if `M ⊗ f` is injective. -/
theorem lTensor_inj_iff_rTensor_inj :
    Function.InjectiveFunction.Injective (lTensor M f) ↔ Function.Injective (rTensor M f) := by
  simp [← comm_comp_rTensor_comp_comm_eq]

Injectivity Equivalence of Left and Right Tensor Product Maps

Informal description

Given a linear map $f : N \to P$ between modules over a commutative semiring $R$, the left tensor product map $M \otimes f$ is injective if and only if the right tensor product map $f \otimes M$ is injective.

LinearMap.lTensor_surj_iff_rTensor_surj theorem

: Function.Surjective (lTensor M f) ↔ Function.Surjective (rTensor M f)

Full source

/-- Given a linear map `f : N → P`, `f ⊗ M` is surjective if and only if `M ⊗ f` is surjective. -/
theorem lTensor_surj_iff_rTensor_surj :
    Function.SurjectiveFunction.Surjective (lTensor M f) ↔ Function.Surjective (rTensor M f) := by
  simp [← comm_comp_rTensor_comp_comm_eq]

Surjectivity Equivalence of Left and Right Tensor Product Maps

Informal description

For a linear map $f : N \to P$ between modules over a commutative semiring $R$, the left tensor product map $f \otimes M$ is surjective if and only if the right tensor product map $M \otimes f$ is surjective.

LinearMap.lTensor_bij_iff_rTensor_bij theorem

: Function.Bijective (lTensor M f) ↔ Function.Bijective (rTensor M f)

Full source

/-- Given a linear map `f : N → P`, `f ⊗ M` is bijective if and only if `M ⊗ f` is bijective. -/
theorem lTensor_bij_iff_rTensor_bij :
    Function.BijectiveFunction.Bijective (lTensor M f) ↔ Function.Bijective (rTensor M f) := by
  simp [← comm_comp_rTensor_comp_comm_eq]

Bijectivity of Left and Right Tensor Product Maps

Informal description

Let $R$ be a commutative semiring, $M$, $N$, and $P$ be $R$-modules, and $f : N \to P$ be a linear map. The left tensor product map $f \otimes \mathrm{id}_M : N \otimes_R M \to P \otimes_R M$ is bijective if and only if the right tensor product map $\mathrm{id}_M \otimes f : M \otimes_R N \to M \otimes_R P$ is bijective.

LinearMap.coe_lTensorHom theorem

: (lTensorHom M : (N →ₗ[R] P) → M ⊗[R] N →ₗ[R] M ⊗[R] P) = lTensor M

Full source

@[simp]
theorem coe_lTensorHom : (lTensorHom M : (N →ₗ[R] P) → M ⊗[R] NM ⊗[R] N →ₗ[R] M ⊗[R] P) = lTensor M :=
  rfl

Coefficient Equality of Left Tensor Homomorphism and Left Tensor Operation

Informal description

The linear map `lTensorHom M`, which maps a linear map $f : N \to P$ to the induced linear map $M \otimes_R N \to M \otimes_R P$, is equal to the left tensor product operation `lTensor M` when viewed as a function.

LinearMap.coe_rTensorHom theorem

: (rTensorHom M : (N →ₗ[R] P) → N ⊗[R] M →ₗ[R] P ⊗[R] M) = rTensor M

Full source

@[simp]
theorem coe_rTensorHom : (rTensorHom M : (N →ₗ[R] P) → N ⊗[R] MN ⊗[R] M →ₗ[R] P ⊗[R] M) = rTensor M :=
  rfl

Right Tensor Homomorphism Coincides with Right Tensor Map

Informal description

The right tensor product homomorphism `rTensorHom M` from the space of linear maps $N \to_R P$ to the space of linear maps $N \otimes_R M \to_R P \otimes_R M$ is equal to the right tensor product map `rTensor M` when viewed as a function.

LinearMap.lTensor_add theorem

(f g : N →ₗ[R] P) : (f + g).lTensor M = f.lTensor M + g.lTensor M

Full source

@[simp]
theorem lTensor_add (f g : N →ₗ[R] P) : (f + g).lTensor M = f.lTensor M + g.lTensor M :=
  (lTensorHom M).map_add f g

Additivity of Left Tensor Product of Linear Maps

Informal description

For any linear maps $f, g : N \to_R P$ over a commutative semiring $R$, the left tensor product of their sum with a module $M$ satisfies $(f + g) \otimes_R M = f \otimes_R M + g \otimes_R M$.

LinearMap.rTensor_add theorem

(f g : N →ₗ[R] P) : (f + g).rTensor M = f.rTensor M + g.rTensor M

Full source

@[simp]
theorem rTensor_add (f g : N →ₗ[R] P) : (f + g).rTensor M = f.rTensor M + g.rTensor M :=
  (rTensorHom M).map_add f g

Right Tensor Product Distributes Over Addition of Linear Maps

Informal description

For any linear maps $f, g : N \to_R P$ over a commutative semiring $R$, the right tensor product of their sum with a module $M$ satisfies $(f + g) \otimes_R M = f \otimes_R M + g \otimes_R M$.

LinearMap.lTensor_zero theorem

: lTensor M (0 : N →ₗ[R] P) = 0

Full source

@[simp]
theorem lTensor_zero : lTensor M (0 : N →ₗ[R] P) = 0 :=
  (lTensorHom M).map_zero

Left Tensor Product of Zero Map is Zero

Informal description

For any module $M$ over a commutative semiring $R$, the left tensor product of the zero linear map from $N$ to $P$ with $M$ is equal to the zero linear map from $M \otimes_R N$ to $M \otimes_R P$, i.e., $(0 : N \to_R P) \otimes^l M = 0$.

LinearMap.rTensor_zero theorem

: rTensor M (0 : N →ₗ[R] P) = 0

Full source

@[simp]
theorem rTensor_zero : rTensor M (0 : N →ₗ[R] P) = 0 :=
  (rTensorHom M).map_zero

Right Tensor Product of Zero Map is Zero

Informal description

For any module $M$ over a commutative semiring $R$, the right tensor product with $M$ of the zero linear map from $N$ to $P$ is equal to the zero linear map from $M \otimes_R N$ to $M \otimes_R P$.

LinearMap.lTensor_smul theorem

(r : R) (f : N →ₗ[R] P) : (r • f).lTensor M = r • f.lTensor M

Full source

@[simp]
theorem lTensor_smul (r : R) (f : N →ₗ[R] P) : (r • f).lTensor M = r • f.lTensor M :=
  (lTensorHom M).map_smul r f

Scalar Multiplication Commutes with Left Tensor Product: $(r \cdot f) \otimes^L M = r \cdot (f \otimes^L M)$

Informal description

For any scalar $r$ in a commutative semiring $R$ and any linear map $f : N \to P$ over $R$, the left tensor product of the scalar multiple $r \cdot f$ with a module $M$ is equal to the scalar multiple $r$ applied to the left tensor product of $f$ with $M$, i.e., $(r \cdot f) \otimes^L M = r \cdot (f \otimes^L M)$.

LinearMap.rTensor_smul theorem

(r : R) (f : N →ₗ[R] P) : (r • f).rTensor M = r • f.rTensor M

Full source

@[simp]
theorem rTensor_smul (r : R) (f : N →ₗ[R] P) : (r • f).rTensor M = r • f.rTensor M :=
  (rTensorHom M).map_smul r f

Scalar Multiplication Commutes with Right Tensor Product of Linear Maps

Informal description

For any scalar $r$ in a commutative semiring $R$ and any linear map $f : N \to_{R} P$, the right tensor product of the scalar multiple $r \cdot f$ with a module $M$ is equal to the scalar multiple $r$ applied to the right tensor product of $f$ with $M$, i.e., $(r \cdot f) \otimes_R M = r \cdot (f \otimes_R M)$.

LinearMap.lTensor_comp theorem

: (g.comp f).lTensor M = (g.lTensor M).comp (f.lTensor M)

Full source

theorem lTensor_comp : (g.comp f).lTensor M = (g.lTensor M).comp (f.lTensor M) := by
  ext m n
  simp only [compr₂_apply, mk_apply, comp_apply, lTensor_tmul]

Composition Commutes with Left Tensor Product: $(g \circ f) \otimes^L M = (g \otimes^L M) \circ (f \otimes^L M)$

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, $Q$ be $R$-modules. For any linear maps $f \colon N \to P$ and $g \colon P \to Q$, the left tensor product of the composition $g \circ f$ with $M$ is equal to the composition of the left tensor products of $g$ and $f$ with $M$, i.e., $(g \circ f) \otimes^L M = (g \otimes^L M) \circ (f \otimes^L M)$.

LinearMap.lTensor_comp_apply theorem

(x : M ⊗[R] N) : (g.comp f).lTensor M x = (g.lTensor M) ((f.lTensor M) x)

Full source

theorem lTensor_comp_apply (x : M ⊗[R] N) :
    (g.comp f).lTensor M x = (g.lTensor M) ((f.lTensor M) x) := by rw [lTensor_comp, coe_comp]; rfl

Evaluation of Composition Commutes with Left Tensor Product

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, $Q$ be $R$-modules. For any linear maps $f \colon N \to P$ and $g \colon P \to Q$, and any element $x \in M \otimes_R N$, we have $$(g \circ f) \otimes^L M (x) = (g \otimes^L M) \big((f \otimes^L M)(x)\big).$$

LinearMap.rTensor_comp theorem

: (g.comp f).rTensor M = (g.rTensor M).comp (f.rTensor M)

Full source

theorem rTensor_comp : (g.comp f).rTensor M = (g.rTensor M).comp (f.rTensor M) := by
  ext m n
  simp only [compr₂_apply, mk_apply, comp_apply, rTensor_tmul]

Composition of Right Tensor Products of Linear Maps

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, $Q$ be $R$-modules. For any linear maps $f \colon N \to P$ and $g \colon P \to Q$, the composition of their right tensor products with $M$ satisfies $(g \circ f) \otimes_R \text{id}_M = (g \otimes_R \text{id}_M) \circ (f \otimes_R \text{id}_M)$.

LinearMap.rTensor_comp_apply theorem

(x : N ⊗[R] M) : (g.comp f).rTensor M x = (g.rTensor M) ((f.rTensor M) x)

Full source

theorem rTensor_comp_apply (x : N ⊗[R] M) :
    (g.comp f).rTensor M x = (g.rTensor M) ((f.rTensor M) x) := by rw [rTensor_comp, coe_comp]; rfl

Right Tensor Product of Composition of Linear Maps Applied to Element

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, $Q$ be $R$-modules. For any linear maps $f \colon N \to P$ and $g \colon P \to Q$, and for any element $x \in N \otimes_R M$, the composition of their right tensor products with $M$ satisfies: \[ (g \circ f) \otimes_R \text{id}_M (x) = (g \otimes_R \text{id}_M) \circ (f \otimes_R \text{id}_M) (x). \]

LinearMap.lTensor_mul theorem

(f g : Module.End R N) : (f * g).lTensor M = f.lTensor M * g.lTensor M

Full source

theorem lTensor_mul (f g : Module.End R N) : (f * g).lTensor M = f.lTensor M * g.lTensor M :=
  lTensor_comp M f g

Composition of Left Tensor Products of Endomorphisms: $(f \circ g) \otimes^L M = (f \otimes^L M) \circ (g \otimes^L M)$

Informal description

Let $R$ be a commutative semiring, $M$ and $N$ be $R$-modules, and $f, g$ be endomorphisms of $N$. Then the left tensor product of the composition $f \circ g$ with $M$ equals the composition of the left tensor products of $f$ and $g$ with $M$, i.e., $(f \circ g) \otimes^L M = (f \otimes^L M) \circ (g \otimes^L M)$.

LinearMap.rTensor_mul theorem

(f g : Module.End R N) : (f * g).rTensor M = f.rTensor M * g.rTensor M

Full source

theorem rTensor_mul (f g : Module.End R N) : (f * g).rTensor M = f.rTensor M * g.rTensor M :=
  rTensor_comp M f g

Composition of Endomorphisms Commutes with Right Tensor Product

Informal description

Let $R$ be a commutative semiring, $M$ and $N$ be $R$-modules, and $f, g \colon N \to N$ be $R$-linear endomorphisms. Then the right tensor product of the composition $f \circ g$ with $M$ equals the composition of the right tensor products of $f$ and $g$ with $M$, i.e., $(f \circ g) \otimes_R \text{id}_M = (f \otimes_R \text{id}_M) \circ (g \otimes_R \text{id}_M)$.

LinearMap.lTensor_id theorem

: (id : N →ₗ[R] N).lTensor M = id

Full source

@[simp]
theorem lTensor_id : (id : N →ₗ[R] N).lTensor M = id :=
  map_id

Left Tensor Product of Identity Map is Identity

Informal description

Let $R$ be a commutative semiring, $M$ and $N$ be $R$-modules. The left tensor product of the identity linear map $\text{id}_N \colon N \to N$ with $M$ is equal to the identity map on $M \otimes_R N$. In symbols: \[ \text{id}_N \otimes_R M = \text{id}_{M \otimes_R N} \]

LinearMap.lTensor_id_apply theorem

(x : M ⊗[R] N) : (LinearMap.id : N →ₗ[R] N).lTensor M x = x

Full source

theorem lTensor_id_apply (x : M ⊗[R] N) : (LinearMap.id : N →ₗ[R] N).lTensor M x = x := by
  rw [lTensor_id, id_coe, _root_.id]

Identity Action of Left Tensor Product on Tensor Elements

Informal description

For any element $x$ in the tensor product $M \otimes_R N$ of $R$-modules $M$ and $N$, the action of the left tensor product of the identity map $\text{id}_N$ with $M$ on $x$ is equal to $x$ itself. In symbols: \[ (\text{id}_N \otimes_R M)(x) = x \]

LinearMap.rTensor_id theorem

: (id : N →ₗ[R] N).rTensor M = id

Full source

@[simp]
theorem rTensor_id : (id : N →ₗ[R] N).rTensor M = id :=
  map_id

Right Tensor Product of Identity Map is Identity

Informal description

Let $R$ be a commutative semiring and $M, N$ be $R$-modules. The right tensor product of the identity linear map $\text{id}_N \colon N \to N$ with $M$ is equal to the identity map on $N \otimes_R M$. In symbols: \[ \text{id}_N \otimes_R M = \text{id}_{N \otimes_R M} \]

LinearMap.rTensor_id_apply theorem

(x : N ⊗[R] M) : (LinearMap.id : N →ₗ[R] N).rTensor M x = x

Full source

theorem rTensor_id_apply (x : N ⊗[R] M) : (LinearMap.id : N →ₗ[R] N).rTensor M x = x := by
  rw [rTensor_id, id_coe, _root_.id]

Right Tensor Product of Identity Map Acts as Identity on Elements

Informal description

For any element $x$ in the tensor product $N \otimes_R M$, the right tensor product of the identity linear map $\text{id}_N \colon N \to N$ with $M$ applied to $x$ is equal to $x$ itself. In symbols: \[ (\text{id}_N \otimes_R M)(x) = x \]

LinearMap.lTensor_smul_action theorem

(r : R) : (DistribMulAction.toLinearMap R N r).lTensor M = DistribMulAction.toLinearMap R (M ⊗[R] N) r

Full source

@[simp]
theorem lTensor_smul_action (r : R) :
    (DistribMulAction.toLinearMap R N r).lTensor M =
      DistribMulAction.toLinearMap R (M ⊗[R] N) r :=
  (lTensor_smul M r LinearMap.id).trans (congrArg _ (lTensor_id M N))

Scalar Multiplication Action Commutes with Left Tensor Product

Informal description

For any scalar $r$ in a commutative semiring $R$, the left tensor product of the scalar multiplication map $r \cdot (-) \colon N \to N$ with an $R$-module $M$ is equal to the scalar multiplication map $r \cdot (-) \colon M \otimes_R N \to M \otimes_R N$. In symbols: \[ (r \cdot (-)) \otimes^L M = r \cdot (-) \quad \text{on} \quad M \otimes_R N \]

LinearMap.rTensor_smul_action theorem

(r : R) : (DistribMulAction.toLinearMap R N r).rTensor M = DistribMulAction.toLinearMap R (N ⊗[R] M) r

Full source

@[simp]
theorem rTensor_smul_action (r : R) :
    (DistribMulAction.toLinearMap R N r).rTensor M =
      DistribMulAction.toLinearMap R (N ⊗[R] M) r :=
  (rTensor_smul M r LinearMap.id).trans (congrArg _ (rTensor_id M N))

Right Tensor Product of Scalar Multiplication Map Equals Scalar Multiplication on Tensor Product

Informal description

For any scalar $r$ in a commutative semiring $R$, the right tensor product of the scalar multiplication map $r \cdot \text{id}_N \colon N \to N$ with an $R$-module $M$ is equal to the scalar multiplication map $r \cdot \text{id}_{N \otimes_R M} \colon N \otimes_R M \to N \otimes_R M$. In symbols: \[ (r \cdot \text{id}_N) \otimes_R M = r \cdot \text{id}_{N \otimes_R M} \]

LinearMap.lTensor_comp_rTensor theorem

(f : M →ₗ[R] P) (g : N →ₗ[R] Q) : (g.lTensor P).comp (f.rTensor N) = map f g

Full source

@[simp]
theorem lTensor_comp_rTensor (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
    (g.lTensor P).comp (f.rTensor N) = map f g := by
  simp only [lTensor, rTensor, ← map_comp, id_comp, comp_id]

Composition of Left and Right Tensor Product Maps Equals Tensor Product Map

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, and $Q$ be $R$-modules. Given $R$-linear maps $f \colon M \to P$ and $g \colon N \to Q$, the composition of the left tensor product map $g \otimes_R \mathrm{id}_P \colon N \otimes_R P \to Q \otimes_R P$ with the right tensor product map $\mathrm{id}_M \otimes_R f \colon M \otimes_R N \to M \otimes_R P$ is equal to the tensor product map $f \otimes g \colon M \otimes_R N \to P \otimes_R Q$.

LinearMap.rTensor_comp_lTensor theorem

(f : M →ₗ[R] P) (g : N →ₗ[R] Q) : (f.rTensor Q).comp (g.lTensor M) = map f g

Full source

@[simp]
theorem rTensor_comp_lTensor (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
    (f.rTensor Q).comp (g.lTensor M) = map f g := by
  simp only [lTensor, rTensor, ← map_comp, id_comp, comp_id]

Composition of Right and Left Tensor Product Maps Equals Tensor Product Map

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, $Q$ be $R$-modules. For any $R$-linear maps $f \colon M \to P$ and $g \colon N \to Q$, the composition of the right tensor product map $f \otimes_R \mathrm{id}_Q \colon M \otimes_R Q \to P \otimes_R Q$ with the left tensor product map $\mathrm{id}_M \otimes_R g \colon M \otimes_R N \to M \otimes_R Q$ equals the tensor product map $\mathrm{map}(f, g) \colon M \otimes_R N \to P \otimes_R Q$.

LinearMap.map_comp_rTensor theorem

(f : M →ₗ[R] P) (g : N →ₗ[R] Q) (f' : S →ₗ[R] M) : (map f g).comp (f'.rTensor _) = map (f.comp f') g

Full source

@[simp]
theorem map_comp_rTensor (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (f' : S →ₗ[R] M) :
    (map f g).comp (f'.rTensor _) = map (f.comp f') g := by
  simp only [lTensor, rTensor, ← map_comp, id_comp, comp_id]

Composition of Tensor Product Map with Right Tensor Product Map

Informal description

Let $R$ be a commutative semiring, and let $M, N, P, Q, S$ be $R$-modules. Given $R$-linear maps $f \colon M \to P$, $g \colon N \to Q$, and $f' \colon S \to M$, the composition of the tensor product map $\mathrm{map}(f, g) \colon M \otimes_R N \to P \otimes_R Q$ with the right tensor product map $f' \otimes_R \mathrm{id}_N \colon S \otimes_R N \to M \otimes_R N$ is equal to the tensor product map $\mathrm{map}(f \circ f', g) \colon S \otimes_R N \to P \otimes_R Q$.

LinearMap.map_comp_lTensor theorem

(f : M →ₗ[R] P) (g : N →ₗ[R] Q) (g' : S →ₗ[R] N) : (map f g).comp (g'.lTensor _) = map f (g.comp g')

Full source

@[simp]
theorem map_comp_lTensor (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (g' : S →ₗ[R] N) :
    (map f g).comp (g'.lTensor _) = map f (g.comp g') := by
  simp only [lTensor, rTensor, ← map_comp, id_comp, comp_id]

Composition of Tensor Product Maps with Left Tensor Product

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, $Q$, $S$ be $R$-modules. For any $R$-linear maps $f \colon M \to P$, $g \colon N \to Q$, and $g' \colon S \to N$, the composition of the tensor product map $\mathrm{map}(f, g) \colon M \otimes_R N \to P \otimes_R Q$ with the left tensor product map $g' \otimes_R \mathrm{id}_M \colon S \otimes_R M \to N \otimes_R M$ equals the tensor product map $\mathrm{map}(f, g \circ g') \colon S \otimes_R M \to P \otimes_R Q$.

LinearMap.rTensor_comp_map theorem

(f' : P →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : (f'.rTensor _).comp (map f g) = map (f'.comp f) g

Full source

@[simp]
theorem rTensor_comp_map (f' : P →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
    (f'.rTensor _).comp (map f g) = map (f'.comp f) g := by
  simp only [lTensor, rTensor, ← map_comp, id_comp, comp_id]

Composition of Right Tensor Product with Tensor Product Map

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, $Q$, and $S$ be $R$-modules. For any $R$-linear maps $f' : P \to S$, $f : M \to P$, and $g : N \to Q$, the composition of the right tensor product map $f' \otimes \mathrm{id}_N$ with the tensor product map $f \otimes g$ equals the tensor product map $(f' \circ f) \otimes g$. In other words, $(f' \otimes \mathrm{id}_N) \circ (f \otimes g) = (f' \circ f) \otimes g$.

LinearMap.lTensor_comp_map theorem

(g' : Q →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : (g'.lTensor _).comp (map f g) = map f (g'.comp g)

Full source

@[simp]
theorem lTensor_comp_map (g' : Q →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
    (g'.lTensor _).comp (map f g) = map f (g'.comp g) := by
  simp only [lTensor, rTensor, ← map_comp, id_comp, comp_id]

Composition of Left Tensor Product with Tensor Product Map

Informal description

Let $R$ be a commutative semiring, and let $M, N, P, Q, S$ be modules over $R$. For any linear maps $f \colon M \to P$, $g \colon N \to Q$, and $g' \colon Q \to S$, the composition of the left tensor product of $g'$ with the tensor product map of $f$ and $g$ is equal to the tensor product map of $f$ with the composition of $g'$ and $g$. That is, \[ (g' \otimes_{\text{left}} \text{id}_P) \circ (f \otimes g) = f \otimes (g' \circ g). \]

LinearMap.rTensor_pow theorem

(f : M →ₗ[R] M) (n : ℕ) : f.rTensor N ^ n = (f ^ n).rTensor N

Full source

@[simp]
theorem rTensor_pow (f : M →ₗ[R] M) (n : ℕ) : f.rTensor N ^ n = (f ^ n).rTensor N := by
  have h := TensorProduct.map_pow f (id : N →ₗ[R] N) n
  rwa [Module.End.id_pow] at h

Power of Right Tensor Product Equals Right Tensor Product of Power: $(f \otimes \mathrm{id}_N)^n = f^n \otimes \mathrm{id}_N$

Informal description

Let $R$ be a commutative semiring, and let $M$ and $N$ be $R$-modules. For any $R$-linear map $f \colon M \to M$ and any natural number $n$, the $n$-th power of the right tensor product map $f \otimes \mathrm{id}_N$ equals the right tensor product of the $n$-th power of $f$. That is, \[ (f \otimes \mathrm{id}_N)^n = f^n \otimes \mathrm{id}_N. \]

LinearMap.lTensor_pow theorem

(f : N →ₗ[R] N) (n : ℕ) : f.lTensor M ^ n = (f ^ n).lTensor M

Full source

@[simp]
theorem lTensor_pow (f : N →ₗ[R] N) (n : ℕ) : f.lTensor M ^ n = (f ^ n).lTensor M := by
  have h := TensorProduct.map_pow (id : M →ₗ[R] M) f n
  rwa [Module.End.id_pow] at h

Power of Left Tensor Product Equals Left Tensor Product of Power: $(f \otimes \text{id}_M)^n = f^n \otimes \text{id}_M$

Informal description

Let $R$ be a commutative semiring, and let $M$ and $N$ be $R$-modules. For any linear map $f \colon N \to N$ and any natural number $n$, the $n$-th power of the left tensor product map $f \otimes \text{id}_M$ equals the left tensor product of the $n$-th power of $f$ with the identity map on $M$. That is, \[ (f \otimes \text{id}_M)^n = f^n \otimes \text{id}_M. \]

LinearEquiv.coe_lTensor theorem

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

Full source

@[simp] theorem coe_lTensor : lTensor M f = (f : N →ₗ[R] P).lTensor M := rfl

Left Tensor Product of Linear Equivalence Equals Tensor Product of Underlying Map

Informal description

For a commutative semiring $R$ and $R$-modules $M, N, P$, and a linear equivalence $f : N \to P$, the left tensor product of $f$ with $M$ is equal to the left tensor product of the underlying linear map of $f$ with $M$. That is, $lTensor_M f = (f : N \to_{R} P).lTensor M$.

LinearEquiv.coe_lTensor_symm theorem

: (lTensor M f).symm = (f.symm : P →ₗ[R] N).lTensor M

Full source

@[simp] theorem coe_lTensor_symm : (lTensor M f).symm = (f.symm : P →ₗ[R] N).lTensor M := rfl

Inverse of Left Tensor Product Equals Left Tensor Product of Inverse

Informal description

For any linear equivalence $f : N \to P$ of $R$-modules, the inverse of the left tensor product with $M$ of $f$ is equal to the left tensor product with $M$ of the inverse of $f$, i.e., $(M \otimes_R f)^{-1} = M \otimes_R f^{-1}$.

LinearEquiv.coe_rTensor theorem

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

Full source

@[simp] theorem coe_rTensor : rTensor M f = (f : N →ₗ[R] P).rTensor M := rfl

Right Tensor Product of Linear Equivalence Equals Tensor Product of Underlying Map

Informal description

The right tensor product of a linear equivalence $f : N \to P$ with a module $M$ is equal to the right tensor product of the underlying linear map of $f$ with $M$.

LinearEquiv.coe_rTensor_symm theorem

: (rTensor M f).symm = (f.symm : P →ₗ[R] N).rTensor M

Full source

@[simp] theorem coe_rTensor_symm : (rTensor M f).symm = (f.symm : P →ₗ[R] N).rTensor M := rfl

Inverse of Right Tensor Product Equals Right Tensor Product of Inverse

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$ be modules over $R$. Given a linear equivalence $f : N \to P$, the inverse of the right tensor product of $f$ with $M$ is equal to the right tensor product of the inverse of $f$ with $M$. In other words, $(f \otimes_R M)^{-1} = f^{-1} \otimes_R M$.

LinearEquiv.lTensor_tmul theorem

: f.lTensor M (m ⊗ₜ n) = m ⊗ₜ f n

Full source

@[simp] theorem lTensor_tmul : f.lTensor M (m ⊗ₜ n) = m ⊗ₜ f n := rfl

Left Tensor Product Action on Elementary Tensors: $(f \otimes \mathrm{id}_M)(m \otimes n) = m \otimes f(n)$

Informal description

For any linear equivalence $f \colon N \to P$ and any elements $m \in M$, $n \in N$, the action of the left tensor product of $f$ with $M$ on the tensor product $m \otimes n$ is given by $m \otimes f(n)$. That is, $(f \otimes \mathrm{id}_M)(m \otimes n) = m \otimes f(n)$.

LinearEquiv.lTensor_symm_tmul theorem

: (f.lTensor M).symm (m ⊗ₜ p) = m ⊗ₜ f.symm p

Full source

@[simp] theorem lTensor_symm_tmul : (f.lTensor M).symm (m ⊗ₜ p) = m ⊗ₜ f.symm p := rfl

Inverse of Left Tensor Product Maps Tensor Element to Tensor of Inverse Image

Informal description

For a linear equivalence $f : N \to P$ and an element $m \otimes p$ in the tensor product $M \otimes P$, the inverse of the left tensor product of $f$ with $M$ maps $m \otimes p$ to $m \otimes f^{-1}(p)$.

LinearEquiv.rTensor_tmul theorem

: f.rTensor M (n ⊗ₜ m) = f n ⊗ₜ m

Full source

@[simp] theorem rTensor_tmul : f.rTensor M (n ⊗ₜ m) = f n ⊗ₜ m := rfl

Right Tensor Product Action on Pure Tensors

Informal description

For a linear equivalence $f \colon N \to P$ and elements $n \in N$, $m \in M$, the right tensor product of $f$ with $M$ applied to the tensor product $n \otimes m$ equals the tensor product of $f(n)$ with $m$, i.e., $(f \otimes_R M)(n \otimes m) = f(n) \otimes m$.

LinearEquiv.rTensor_symm_tmul theorem

: (f.rTensor M).symm (p ⊗ₜ m) = f.symm p ⊗ₜ m

Full source

@[simp] theorem rTensor_symm_tmul : (f.rTensor M).symm (p ⊗ₜ m) = f.symm p ⊗ₜ m := rfl

Inverse of Right Tensor Product Map on Simple Tensors

Informal description

Let $R$ be a commutative semiring, $M$ and $N$ be $R$-modules, and $f : N \simeqₗ[R] P$ be a linear equivalence. Then for any $p \in P$ and $m \in M$, the inverse of the right tensor product map $f \otimes_R M$ satisfies $(f \otimes_R M)^{-1}(p \otimes m) = f^{-1}(p) \otimes m$.

LinearEquiv.comm_trans_rTensor_trans_comm_eq theorem

(g : N ≃ₗ[R] P) : TensorProduct.comm R Q N ≪≫ₗ rTensor Q g ≪≫ₗ TensorProduct.comm R P Q = lTensor Q g

Full source

lemma comm_trans_rTensor_trans_comm_eq (g : N ≃ₗ[R] P) :
    TensorProduct.commTensorProduct.comm R Q N ≪≫ₗ rTensor Q gTensorProduct.comm R Q N ≪≫ₗ rTensor Q g ≪≫ₗ TensorProduct.comm R P Q = lTensor Q g :=
  toLinearMap_injective <| TensorProduct.ext rfl

Composition of Commutativity and Right Tensor Product Equivalences Equals Left Tensor Product Equivalence

Informal description

Let $R$ be a commutative semiring, and let $N$, $P$, and $Q$ be $R$-modules. Given a linear equivalence $g \colon N \simeq_{[R]} P$, the composition of the following three linear equivalences: 1. The commutativity equivalence $Q \otimes_R N \simeq N \otimes_R Q$, 2. The right tensor product equivalence $N \otimes_R Q \simeq P \otimes_R Q$ induced by $g$, 3. The commutativity equivalence $P \otimes_R Q \simeq Q \otimes_R P$, is equal to the left tensor product equivalence $Q \otimes_R N \simeq Q \otimes_R P$ induced by $g$.

LinearEquiv.comm_trans_lTensor_trans_comm_eq theorem

(g : N ≃ₗ[R] P) : TensorProduct.comm R N Q ≪≫ₗ lTensor Q g ≪≫ₗ TensorProduct.comm R Q P = rTensor Q g

Full source

lemma comm_trans_lTensor_trans_comm_eq (g : N ≃ₗ[R] P) :
    TensorProduct.commTensorProduct.comm R N Q ≪≫ₗ lTensor Q gTensorProduct.comm R N Q ≪≫ₗ lTensor Q g ≪≫ₗ TensorProduct.comm R Q P = rTensor Q g :=
  toLinearMap_injective <| TensorProduct.ext rfl

Commutativity of Tensor Product with Linear Equivalence via Left and Right Tensor Products

Informal description

Let $R$ be a commutative semiring, $N$, $P$, and $Q$ be $R$-modules, and $g : N \simeq_{[R]} P$ be a linear equivalence. Then the composition of the following three linear isomorphisms: 1. The tensor product commutativity isomorphism $N \otimes_R Q \simeq Q \otimes_R N$, 2. The left tensor product with $Q$ of $g$, $Q \otimes_R N \simeq Q \otimes_R P$, 3. The tensor product commutativity isomorphism $Q \otimes_R P \simeq P \otimes_R Q$, is equal to the right tensor product with $Q$ of $g$, viewed as an isomorphism $N \otimes_R Q \simeq P \otimes_R Q$. In symbols: $\text{comm}_{R}^{N,Q} \circ (\text{lTensor}_Q g) \circ \text{comm}_{R}^{Q,P} = \text{rTensor}_Q g$

LinearEquiv.lTensor_trans theorem

: (f ≪≫ₗ g).lTensor M = f.lTensor M ≪≫ₗ g.lTensor M

Full source

theorem lTensor_trans : (f ≪≫ₗ g).lTensor M = f.lTensor M ≪≫ₗ g.lTensor M :=
  toLinearMap_injective <| LinearMap.lTensor_comp M _ _

Composition of Linear Equivalences Commutes with Left Tensor Product: $(f \circ g) \otimes^L M = (f \otimes^L M) \circ (g \otimes^L M)$

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, $Q$ be $R$-modules. Given linear equivalences $f \colon N \simeq_{[R]} P$ and $g \colon P \simeq_{[R]} Q$, the left tensor product of the composition $f \circ g$ with $M$ is equal to the composition of the left tensor products of $f$ and $g$ with $M$, i.e., $(f \circ g) \otimes^L M = (f \otimes^L M) \circ (g \otimes^L M)$.

LinearEquiv.lTensor_trans_apply theorem

: (f ≪≫ₗ g).lTensor M x = g.lTensor M (f.lTensor M x)

Full source

theorem lTensor_trans_apply : (f ≪≫ₗ g).lTensor M x = g.lTensor M (f.lTensor M x) :=
  LinearMap.lTensor_comp_apply M _ _ x

Evaluation of Composition Commutes with Left Tensor Product: $(f \circ g) \otimes^L M (x) = (g \otimes^L M) \circ (f \otimes^L M)(x)$

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, $Q$ be $R$-modules. Given linear equivalences $f \colon N \simeq_{[R]} P$ and $g \colon P \simeq_{[R]} Q$, and an element $x \in M \otimes_R N$, we have $$(f \circ g) \otimes^L M (x) = (g \otimes^L M) \big((f \otimes^L M)(x)\big).$$

LinearEquiv.rTensor_trans theorem

: (f ≪≫ₗ g).rTensor M = f.rTensor M ≪≫ₗ g.rTensor M

Full source

theorem rTensor_trans : (f ≪≫ₗ g).rTensor M = f.rTensor M ≪≫ₗ g.rTensor M :=
  toLinearMap_injective <| LinearMap.rTensor_comp M _ _

Composition of Right Tensor Products of Linear Equivalences

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, $Q$ be $R$-modules. For any linear equivalences $f \colon N \to P$ and $g \colon P \to Q$, the right tensor product of their composition with $M$ is equal to the composition of their right tensor products with $M$, i.e., $(f \circ g) \otimes_R \text{id}_M = (f \otimes_R \text{id}_M) \circ (g \otimes_R \text{id}_M)$.

LinearEquiv.rTensor_trans_apply theorem

: (f ≪≫ₗ g).rTensor M y = g.rTensor M (f.rTensor M y)

Full source

theorem rTensor_trans_apply : (f ≪≫ₗ g).rTensor M y = g.rTensor M (f.rTensor M y) :=
  LinearMap.rTensor_comp_apply M _ _ y

Composition of Right Tensor Products of Linear Equivalences Applied to Element

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, $Q$ be $R$-modules. For any linear equivalences $f \colon N \to P$ and $g \colon P \to Q$, and for any element $y \in N \otimes_R M$, the composition of their right tensor products with $M$ satisfies: \[ (f \circ g) \otimes_R \text{id}_M (y) = (g \otimes_R \text{id}_M) \circ (f \otimes_R \text{id}_M) (y). \]

LinearEquiv.rTensor_mul theorem

(f g : N ≃ₗ[R] N) : (f * g).rTensor M = f.rTensor M * g.rTensor M

Full source

theorem rTensor_mul (f g : N ≃ₗ[R] N) : (f * g).rTensor M = f.rTensor M * g.rTensor M :=
  rTensor_trans M f g

Composition of Right Tensor Products of Linear Equivalences

Informal description

Let $R$ be a commutative semiring, $M$ and $N$ be $R$-modules, and $f, g \colon N \to N$ be linear equivalences. Then the right tensor product of the composition $f \circ g$ with $M$ is equal to the composition of the right tensor products of $f$ and $g$ with $M$, i.e., $(f \circ g) \otimes_R M = (f \otimes_R M) \circ (g \otimes_R M)$.

LinearEquiv.lTensor_refl theorem

: (refl R N).lTensor M = refl R _

Full source

@[simp] theorem lTensor_refl : (refl R N).lTensor M = refl R _ := TensorProduct.congr_refl_refl

Left Tensor Product of Identity Equivalence is Identity

Informal description

Given a commutative semiring $R$ and modules $M$ and $N$ over $R$, the left tensor product of the identity linear equivalence $\text{refl}_R N$ with $M$ is equal to the identity linear equivalence on $M \otimes_R N$. That is, $(\text{refl}_R N) \otimes_R M = \text{refl}_R (M \otimes_R N)$.

LinearEquiv.lTensor_refl_apply theorem

: (refl R N).lTensor M x = x

Full source

theorem lTensor_refl_apply : (refl R N).lTensor M x = x := by rw [lTensor_refl, refl_apply]

Identity Action of Left Tensor Product with Identity Equivalence

Informal description

For any commutative semiring $R$ and $R$-modules $M$ and $N$, the left tensor product of the identity linear equivalence $\text{refl}_R N$ with $M$ acts as the identity on any element $x$ of $M \otimes_R N$. That is, $(\text{refl}_R N) \otimes_R M (x) = x$.

LinearEquiv.rTensor_refl theorem

: (refl R N).rTensor M = refl R _

Full source

@[simp] theorem rTensor_refl : (refl R N).rTensor M = refl R _ := TensorProduct.congr_refl_refl

Right Tensor Product of Identity Equivalence is Identity

Informal description

For any commutative semiring $R$ and any $R$-module $M$, the right tensor product of the identity linear equivalence on $N$ with $M$ is equal to the identity linear equivalence on $M \otimes_R N$. That is, $(\text{refl}_R N) \otimes_R M = \text{refl}_R (M \otimes_R N)$.

LinearEquiv.rTensor_refl_apply theorem

: (refl R N).rTensor M y = y

Full source

theorem rTensor_refl_apply : (refl R N).rTensor M y = y := by rw [rTensor_refl, refl_apply]

Right Tensor Product of Identity Equivalence Acts as Identity

Informal description

For any commutative semiring $R$ and $R$-modules $M$ and $N$, the right tensor product of the identity linear equivalence $\text{refl}_R N$ with $M$ acts as the identity on any element $y$ of $M \otimes_R N$. That is, $(\text{refl}_R N) \otimes_R M (y) = y$.

LinearEquiv.rTensor_trans_lTensor theorem

(f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) : f.rTensor N ≪≫ₗ g.lTensor P = TensorProduct.congr f g

Full source

@[simp] theorem rTensor_trans_lTensor (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) :
    f.rTensor N ≪≫ₗ g.lTensor P = TensorProduct.congr f g :=
  toLinearMap_injective <| LinearMap.lTensor_comp_rTensor M _ _

Composition of Right and Left Tensor Product Isomorphisms Equals Tensor Product Isomorphism

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, and $Q$ be $R$-modules. Given $R$-linear isomorphisms $f \colon M \to P$ and $g \colon N \to Q$, the composition of the right tensor product map $f \otimes_R \mathrm{id}_N \colon M \otimes_R N \to P \otimes_R N$ with the left tensor product map $\mathrm{id}_P \otimes_R g \colon P \otimes_R N \to P \otimes_R Q$ is equal to the tensor product isomorphism $f \otimes g \colon M \otimes_R N \to P \otimes_R Q$.

LinearEquiv.lTensor_trans_rTensor theorem

(f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) : g.lTensor M ≪≫ₗ f.rTensor Q = TensorProduct.congr f g

Full source

@[simp] theorem lTensor_trans_rTensor (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) :
    g.lTensor M ≪≫ₗ f.rTensor Q = TensorProduct.congr f g :=
  toLinearMap_injective <| LinearMap.rTensor_comp_lTensor M _ _

Composition of Left and Right Tensor Product Isomorphisms Equals Tensor Product Congruence

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, $Q$ be $R$-modules. For any $R$-linear isomorphisms $f \colon M \simeq P$ and $g \colon N \simeq Q$, the composition of the left tensor product isomorphism $\mathrm{id}_M \otimes_R g \colon M \otimes_R N \simeq M \otimes_R Q$ with the right tensor product isomorphism $f \otimes_R \mathrm{id}_Q \colon M \otimes_R Q \simeq P \otimes_R Q$ equals the tensor product isomorphism $\mathrm{congr}(f, g) \colon M \otimes_R N \simeq P \otimes_R Q$.

LinearEquiv.rTensor_trans_congr theorem

 (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (f' : S ≃ₗ[R] M) :
  f'.rTensor _ ≪≫ₗ TensorProduct.congr f g = TensorProduct.congr (f' ≪≫ₗ f) g

Full source

@[simp] theorem rTensor_trans_congr (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (f' : S ≃ₗ[R] M) :
    f'.rTensor _ ≪≫ₗ TensorProduct.congr f g = TensorProduct.congr (f' ≪≫ₗ f) g :=
  toLinearMap_injective <| LinearMap.map_comp_rTensor M _ _ _

Composition of Right Tensor Product with Tensor Product Congruence

Informal description

Let $R$ be a commutative semiring, and let $M, N, P, Q, S$ be $R$-modules. Given $R$-linear isomorphisms $f \colon M \to P$, $g \colon N \to Q$, and $f' \colon S \to M$, the composition of the right tensor product map $f' \otimes_R \mathrm{id}_N \colon S \otimes_R N \to M \otimes_R N$ with the tensor product congruence map $\mathrm{congr}(f, g) \colon M \otimes_R N \to P \otimes_R Q$ is equal to the tensor product congruence map $\mathrm{congr}(f' \circ f, g) \colon S \otimes_R N \to P \otimes_R Q$.

LinearEquiv.lTensor_trans_congr theorem

 (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (g' : S ≃ₗ[R] N) :
  g'.lTensor _ ≪≫ₗ TensorProduct.congr f g = TensorProduct.congr f (g' ≪≫ₗ g)

Full source

@[simp] theorem lTensor_trans_congr (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (g' : S ≃ₗ[R] N) :
    g'.lTensor _ ≪≫ₗ TensorProduct.congr f g = TensorProduct.congr f (g' ≪≫ₗ g) :=
  toLinearMap_injective <| LinearMap.map_comp_lTensor M _ _ _

Composition of Left Tensor Product with Tensor Product Isomorphism Equals Tensor Product of Composed Isomorphisms

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, $Q$, $S$ be $R$-modules. For any $R$-linear isomorphisms $f \colon M \to P$, $g \colon N \to Q$, and $g' \colon S \to N$, the composition of the left tensor product map $g' \otimes_R \mathrm{id}_M \colon S \otimes_R M \to N \otimes_R M$ with the tensor product isomorphism $\mathrm{congr}(f, g) \colon N \otimes_R M \to Q \otimes_R P$ equals the tensor product isomorphism $\mathrm{congr}(f, g' \circ g) \colon S \otimes_R M \to Q \otimes_R P$.

LinearEquiv.congr_trans_rTensor theorem

 (f' : P ≃ₗ[R] S) (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) :
  TensorProduct.congr f g ≪≫ₗ f'.rTensor _ = TensorProduct.congr (f ≪≫ₗ f') g

Full source

@[simp] theorem congr_trans_rTensor (f' : P ≃ₗ[R] S) (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) :
    TensorProduct.congrTensorProduct.congr f g ≪≫ₗ f'.rTensor _ = TensorProduct.congr (f ≪≫ₗ f') g :=
  toLinearMap_injective <| LinearMap.rTensor_comp_map M _ _ _

Composition of Tensor Product Isomorphism with Right Tensor Product Isomorphism

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$, $Q$, and $S$ be $R$-modules. For any $R$-linear isomorphisms $f' : P \simeq S$, $f : M \simeq P$, and $g : N \simeq Q$, the composition of the tensor product isomorphism $f \otimes g$ with the right tensor product isomorphism $f' \otimes \mathrm{id}_Q$ equals the tensor product isomorphism $(f \circ f') \otimes g$. In other words, $(f \otimes g) \circ (f' \otimes \mathrm{id}_Q) = (f \circ f') \otimes g$.

LinearEquiv.congr_trans_lTensor theorem

 (g' : Q ≃ₗ[R] S) (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) :
  TensorProduct.congr f g ≪≫ₗ g'.lTensor _ = TensorProduct.congr f (g ≪≫ₗ g')

Full source

@[simp] theorem congr_trans_lTensor (g' : Q ≃ₗ[R] S) (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) :
    TensorProduct.congrTensorProduct.congr f g ≪≫ₗ g'.lTensor _ = TensorProduct.congr f (g ≪≫ₗ g') :=
  toLinearMap_injective <| LinearMap.lTensor_comp_map M _ _ _

Composition of Tensor Product Isomorphism with Left Tensor Product Isomorphism

Informal description

Let $R$ be a commutative semiring, and let $M, N, P, Q, S$ be modules over $R$. For any linear isomorphisms $f \colon M \to P$, $g \colon N \to Q$, and $g' \colon Q \to S$, the composition of the tensor product isomorphism $f \otimes g$ with the left tensor product isomorphism $g' \otimes \text{id}_P$ is equal to the tensor product isomorphism $f \otimes (g' \circ g)$. That is, \[ (f \otimes g) \circ (g' \otimes \text{id}_P) = f \otimes (g' \circ g). \]

LinearEquiv.rTensor_pow theorem

(f : M ≃ₗ[R] M) (n : ℕ) : f.rTensor N ^ n = (f ^ n).rTensor N

Full source

@[simp] theorem rTensor_pow (f : M ≃ₗ[R] M) (n : ℕ) : f.rTensor N ^ n = (f ^ n).rTensor N := by
  simpa only [one_pow] using TensorProduct.congr_pow f (1 : N ≃ₗ[R] N) n

Power of Right Tensor Product Automorphism: $(f \otimes \mathrm{id}_N)^n = f^n \otimes \mathrm{id}_N$

Informal description

Let $R$ be a commutative semiring, and let $M$ and $N$ be $R$-modules. For any linear automorphism $f$ of $M$ and any natural number $n$, the $n$-th power of the right tensor product automorphism $f \otimes \mathrm{id}_N$ on $M \otimes_R N$ equals the right tensor product of the $n$-th power of $f$ with the identity on $N$. That is, \[ (f \otimes \mathrm{id}_N)^n = f^n \otimes \mathrm{id}_N. \]

LinearEquiv.rTensor_zpow theorem

(f : M ≃ₗ[R] M) (n : ℤ) : f.rTensor N ^ n = (f ^ n).rTensor N

Full source

@[simp] theorem rTensor_zpow (f : M ≃ₗ[R] M) (n : ℤ) : f.rTensor N ^ n = (f ^ n).rTensor N := by
  simpa only [one_zpow] using TensorProduct.congr_zpow f (1 : N ≃ₗ[R] N) n

Integer Power of Right Tensor Product Automorphism: $(f \otimes \mathrm{id}_N)^n = f^n \otimes \mathrm{id}_N$

Informal description

Let $R$ be a commutative semiring, and let $M$ and $N$ be $R$-modules. For any linear automorphism $f$ of $M$ and any integer $n$, the $n$-th power of the right tensor product automorphism $f \otimes \mathrm{id}_N$ on $M \otimes_R N$ equals the right tensor product of the $n$-th power of $f$ with the identity on $N$. That is, \[ (f \otimes \mathrm{id}_N)^n = f^n \otimes \mathrm{id}_N. \]

LinearEquiv.lTensor_pow theorem

(f : N ≃ₗ[R] N) (n : ℕ) : f.lTensor M ^ n = (f ^ n).lTensor M

Full source

@[simp] theorem lTensor_pow (f : N ≃ₗ[R] N) (n : ℕ) : f.lTensor M ^ n = (f ^ n).lTensor M := by
  simpa only [one_pow] using TensorProduct.congr_pow (1 : M ≃ₗ[R] M) f n

Power of Left Tensor Product Automorphism: $(f.lTensor M)^n = (f^n).lTensor M$

Informal description

Let $R$ be a commutative semiring, $M$ and $N$ be $R$-modules, and $f : N \to N$ be a linear automorphism. For any natural number $n$, the $n$-th power of the induced automorphism $f.lTensor M$ on $M \otimes_R N$ equals the induced automorphism of the $n$-th power of $f$. That is, \[ (f.lTensor M)^n = (f^n).lTensor M. \]

LinearEquiv.lTensor_zpow theorem

(f : N ≃ₗ[R] N) (n : ℤ) : f.lTensor M ^ n = (f ^ n).lTensor M

Full source

@[simp] theorem lTensor_zpow (f : N ≃ₗ[R] N) (n : ℤ) : f.lTensor M ^ n = (f ^ n).lTensor M := by
  simpa only [one_zpow] using TensorProduct.congr_zpow (1 : M ≃ₗ[R] M) f n

Integer Power of Left Tensor Product Automorphism: $(f.lTensor M)^n = (f^n).lTensor M$

Informal description

Let $R$ be a commutative semiring, and let $M$ and $N$ be $R$-modules. For any linear automorphism $f$ of $N$ and any integer $n$, the $n$-th power of the induced automorphism $f.lTensor M$ on $M \otimes_R N$ equals the induced automorphism of the $n$-th power of $f$. That is, \[ (f.lTensor M)^n = (f^n).lTensor M. \]

TensorProduct.neg_add_cancel theorem

(x : M ⊗[R] N) : -x + x = 0

Full source

protected theorem neg_add_cancel (x : M ⊗[R] N) : -x + x = 0 :=
  x.induction_on
    (by rw [add_zero]; apply (Neg.aux R).map_zero)
    (fun x y => by convert (add_tmul (R := R) (-x) x y).symm; rw [neg_add_cancel, zero_tmul])
    fun x y hx hy => by
    suffices -x + x + (-y + y) = 0 by
      rw [← this]
      unfold Neg.neg neg
      simp only
      rw [map_add]
      abel
    rw [hx, hy, add_zero]

Additive Inverse Cancellation in Tensor Product: $-x + x = 0$

Informal description

For any element $x$ in the tensor product $M \otimes_R N$ of modules $M$ and $N$ over a commutative semiring $R$, the sum of $-x$ and $x$ is equal to zero, i.e., $-x + x = 0$.

TensorProduct.neg_tmul theorem

(m : M) (n : N) : (-m) ⊗ₜ n = -m ⊗ₜ[R] n

Full source

theorem neg_tmul (m : M) (n : N) : (-m) ⊗ₜ n = -m ⊗ₜ[R] n :=
  rfl

Negation in First Argument of Tensor Product Equals Negation of Tensor Product

Informal description

For any elements $m$ in an $R$-module $M$ and $n$ in an $R$-module $N$, the tensor product of $-m$ and $n$ equals the negation of the tensor product of $m$ and $n$, i.e., $(-m) \otimes_R n = -(m \otimes_R n)$.

TensorProduct.tmul_neg theorem

(m : M) (n : N) : m ⊗ₜ (-n) = -m ⊗ₜ[R] n

Full source

theorem tmul_neg (m : M) (n : N) : m ⊗ₜ (-n) = -m ⊗ₜ[R] n :=
  (mk R M N _).map_neg _

Tensor Product with Negated Second Argument Equals Negation of Tensor Product

Informal description

For any elements $m$ in an $R$-module $M$ and $n$ in an $R$-module $N$, the tensor product of $m$ and $-n$ equals the negation of the tensor product of $m$ and $n$, i.e., $m \otimes_R (-n) = -(m \otimes_R n)$.

TensorProduct.tmul_sub theorem

(m : M) (n₁ n₂ : N) : m ⊗ₜ (n₁ - n₂) = m ⊗ₜ[R] n₁ - m ⊗ₜ[R] n₂

Full source

theorem tmul_sub (m : M) (n₁ n₂ : N) : m ⊗ₜ (n₁ - n₂) = m ⊗ₜ[R] n₁ - m ⊗ₜ[R] n₂ :=
  (mk R M N _).map_sub _ _

Tensor Product Distributes Over Subtraction in Second Argument

Informal description

For any element $m$ in an $R$-module $M$ and any elements $n_1, n_2$ in an $R$-module $N$, the tensor product of $m$ with the difference $n_1 - n_2$ is equal to the difference of the tensor products $m \otimes_R n_1$ and $m \otimes_R n_2$, i.e., $m \otimes_R (n_1 - n_2) = m \otimes_R n_1 - m \otimes_R n_2$.

TensorProduct.sub_tmul theorem

(m₁ m₂ : M) (n : N) : (m₁ - m₂) ⊗ₜ n = m₁ ⊗ₜ[R] n - m₂ ⊗ₜ[R] n

Full source

theorem sub_tmul (m₁ m₂ : M) (n : N) : (m₁ - m₂) ⊗ₜ n = m₁ ⊗ₜ[R] n - m₂ ⊗ₜ[R] n :=
  (mk R M N).map_sub₂ _ _ _

Tensor product distributes over subtraction in the first argument: $(m_1 - m_2) \otimes n = m_1 \otimes n - m_2 \otimes n$

Informal description

Let $R$ be a commutative semiring, and let $M$ and $N$ be modules over $R$. For any elements $m_1, m_2 \in M$ and $n \in N$, the tensor product satisfies the following identity: $$(m_1 - m_2) \otimes n = m_1 \otimes n - m_2 \otimes n.$$

LinearMap.lTensor_sub theorem

(f g : N →ₗ[R] P) : (f - g).lTensor M = f.lTensor M - g.lTensor M

Full source

@[simp]
theorem lTensor_sub (f g : N →ₗ[R] P) : (f - g).lTensor M = f.lTensor M - g.lTensor M := by
  simp_rw [← coe_lTensorHom]
  exact (lTensorHom (R := R) (N := N) (P := P) M).map_sub f g

Left Tensor Product Preserves Subtraction of Linear Maps

Informal description

Let $R$ be a commutative semiring, and let $M$, $N$, $P$ be modules over $R$. For any two linear maps $f, g : N \to P$, the left tensor product of their difference $(f - g) \otimes_R M$ equals the difference of their left tensor products $f \otimes_R M - g \otimes_R M$.

LinearMap.rTensor_sub theorem

(f g : N →ₗ[R] P) : (f - g).rTensor M = f.rTensor M - g.rTensor M

Full source

@[simp]
theorem rTensor_sub (f g : N →ₗ[R] P) : (f - g).rTensor M = f.rTensor M - g.rTensor M := by
  simp only [← coe_rTensorHom]
  exact (rTensorHom (R := R) (N := N) (P := P) M).map_sub f g

Right Tensor Product Distributes Over Subtraction of Linear Maps

Informal description

For any $R$-linear maps $f, g : N \to P$, the right tensor product of their difference $(f - g)$ with $M$ is equal to the difference of their right tensor products with $M$, i.e., $(f - g) \otimes_R M = f \otimes_R M - g \otimes_R M$.

LinearMap.lTensor_neg theorem

(f : N →ₗ[R] P) : (-f).lTensor M = -f.lTensor M

Full source

@[simp]
theorem lTensor_neg (f : N →ₗ[R] P) : (-f).lTensor M = -f.lTensor M := by
  simp only [← coe_lTensorHom]
  exact (lTensorHom (R := R) (N := N) (P := P) M).map_neg f

Negation Commutes with Left Tensor Product of Linear Maps

Informal description

For any linear map $f : N \to P$ over a commutative semiring $R$, the left tensor product of the negation $-f$ with a module $M$ equals the negation of the left tensor product of $f$ with $M$, i.e., $(-f) \otimes^l M = -(f \otimes^l M)$.

LinearMap.rTensor_neg theorem

(f : N →ₗ[R] P) : (-f).rTensor M = -f.rTensor M

Full source

@[simp]
theorem rTensor_neg (f : N →ₗ[R] P) : (-f).rTensor M = -f.rTensor M := by
  simp only [← coe_rTensorHom]
  exact (rTensorHom (R := R) (N := N) (P := P) M).map_neg f

Negation Commutes with Right Tensor Product of Linear Maps

Informal description

For any linear map $f \colon N \to P$ over a commutative semiring $R$, the right tensor product of the negation $-f$ with a module $M$ equals the negation of the right tensor product of $f$ with $M$. That is, $(-f) \otimes_R M = -(f \otimes_R M)$.

Mathlib.LinearAlgebra.TensorProduct.Basic

Notation

Tags