Mathlib.LinearAlgebra.TensorProduct.Tower

TensorProduct.AlgebraTensorModule.smul_eq_lsmul_rTensor theorem

(a : A) (x : M ⊗[R] N) : a • x = (lsmul R R M a).rTensor N x

Full source

theorem smul_eq_lsmul_rTensor (a : A) (x : M ⊗[R] N) : a • x = (lsmul R R M a).rTensor N x :=
  rfl

Scalar multiplication as right tensor product of left scalar multiplication

Informal description

For any element $a \in A$ and any tensor $x \in M \otimes_R N$, the scalar multiplication $a \cdot x$ is equal to the right tensor product of the left scalar multiplication map $\text{lsmul}_R^M(a)$ with $N$ applied to $x$.

TensorProduct.AlgebraTensorModule.restrictScalars_curry theorem

(f : M ⊗[R] N →ₗ[A] P) : restrictScalars R (curry f) = TensorProduct.curry (f.restrictScalars R)

Full source

theorem restrictScalars_curry (f : M ⊗[R] NM ⊗[R] N →ₗ[A] P) :
    restrictScalars R (curry f) = TensorProduct.curry (f.restrictScalars R) :=
  rfl

Compatibility of Restriction of Scalars with Currying for Tensor Product Modules

Informal description

For any $A$-linear map $f: M \otimes_R N \to P$, the restriction of scalars of the curried form of $f$ equals the curried form of the restriction of scalars of $f$. In other words, the following diagram commutes: \[ \begin{tikzcd} (M \otimes_R N \to_A P) \arrow[r, "\text{curry}"] \arrow[d, "\text{restrictScalars}"] & (M \to_A N \to_R P) \arrow[d, "\text{restrictScalars}"] \\ (M \otimes_R N \to_R P) \arrow[r, "\text{curry}"] & (M \to_R N \to_R P) \end{tikzcd} \] where $\to_A$ denotes $A$-linear maps and $\to_R$ denotes $R$-linear maps.

TensorProduct.AlgebraTensorModule.curry_injective theorem

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

Full source

/-- Just as `TensorProduct.ext` is marked `ext` instead of `TensorProduct.ext'`, this is
a better `ext` lemma than `TensorProduct.AlgebraTensorModule.ext` below.

See note [partially-applied ext lemmas]. -/
@[ext high]
nonrec theorem curry_injective : Function.Injective (curry : (M ⊗ NM ⊗ N →ₗ[A] P) → M →ₗ[A] N →ₗ[R] P) :=
  fun _ _ h =>
  LinearMap.restrictScalars_injective R <|
    curry_injective <| (congr_arg (LinearMap.restrictScalars R) h :)

Injectivity of Currying for $A$-Linear Tensor Product Maps

Informal description

The currying operation for $A$-linear maps from the tensor product $M \otimes_R N$ to $P$ is injective. That is, if two $A$-linear maps $f, g \colon M \otimes_R N \to P$ induce the same $A$-linear map $M \to \text{Hom}_R(N, P)$ via currying, then $f = g$.

TensorProduct.AlgebraTensorModule.ext theorem

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

Full source

theorem ext {g h : M ⊗[R] NM ⊗[R] N →ₗ[A] P} (H : ∀ x y, g (x ⊗ₜ y) = h (x ⊗ₜ y)) : g = h :=
  curry_injective <| LinearMap.ext₂ H

Extensionality of $A$-Linear Maps on Tensor Products via Simple Tensors

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $M$, $N$, $P$ be $R$-modules with $M$ and $P$ also being $A$-modules. For any two $A$-linear maps $g, h \colon 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.AlgebraTensorModule.lift_apply theorem

 (f : M →ₗ[A] N →ₗ[R] P) (a : M ⊗[R] N) :
  AlgebraTensorModule.lift f a = TensorProduct.lift (LinearMap.restrictScalars R f) a

Full source

@[simp]
theorem lift_apply (f : M →ₗ[A] N →ₗ[R] P) (a : M ⊗[R] N) :
    AlgebraTensorModule.lift f a = TensorProduct.lift (LinearMap.restrictScalars R f) a :=
  rfl

Equality of Lifted Tensor Map and Scalar-Restricted Lift

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $M$, $N$, $P$ be $R$-modules with $M$ and $P$ also being $A$-modules. For any $A$-linear map $f : M \to \text{Hom}_R(N, P)$ and any element $a \in M \otimes_R N$, the action of the lifted map $\text{lift}(f)$ on $a$ equals the action of the $R$-linear extension of $f$ on $a$. That is, \[ \text{lift}(f)(a) = \text{TensorProduct.lift}(\text{LinearMap.restrictScalars}_R f)(a). \]

TensorProduct.AlgebraTensorModule.lift_tmul theorem

(f : M →ₗ[A] N →ₗ[R] P) (x : M) (y : N) : lift f (x ⊗ₜ y) = f x y

Full source

@[simp]
theorem lift_tmul (f : M →ₗ[A] N →ₗ[R] P) (x : M) (y : N) : lift f (x ⊗ₜ y) = f x y :=
  rfl

Action of Lifted Tensor Map on Simple Tensors

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $M$, $N$, $P$ be $R$-modules with $M$ and $P$ also being $A$-modules. For any $A$-linear map $f : M \to \text{Hom}_R(N, P)$ and any elements $x \in M$, $y \in N$, the action of the lifted map $\text{lift}(f)$ on the simple tensor $x \otimes y$ is given by $\text{lift}(f)(x \otimes y) = f(x)(y)$.

TensorProduct.AlgebraTensorModule.map_tmul theorem

(f : M →ₗ[A] 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 →ₗ[A] P) (g : N →ₗ[R] Q) (m : M) (n : N) :
    map f g (m ⊗ₜ n) = f m ⊗ₜ g n :=
  rfl

Tensor product map action on simple tensors: $\text{map}(f,g)(m \otimes n) = f(m) \otimes g(n)$

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $M$, $N$, $P$, $Q$ be $R$-modules with $M$ and $P$ also being $A$-modules. For any $A$-linear map $f : M \to P$ and any $R$-linear map $g : N \to Q$, the tensor product map $\text{map}(f, g)$ acts on a simple tensor $m \otimes n$ as: \[ \text{map}(f, g)(m \otimes n) = f(m) \otimes g(n). \]

TensorProduct.AlgebraTensorModule.map_id theorem

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

Full source

@[simp]
theorem map_id : map (id : M →ₗ[A] M) (id : N →ₗ[R] N) = .id :=
  ext fun _ _ => rfl

Identity Tensor Map is Identity

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $M$, $N$ be $R$-modules with $M$ also being an $A$-module. The tensor product map of the identity $A$-linear map on $M$ and the identity $R$-linear map on $N$ is equal to the identity map on $M \otimes_R N$.

TensorProduct.AlgebraTensorModule.map_comp theorem

 (f₂ : P →ₗ[A] P') (f₁ : M →ₗ[A] 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 →ₗ[A] P') (f₁ : M →ₗ[A] 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 ring, $A$ an $R$-algebra, and $M$, $N$, $P$, $P'$, $Q$, $Q'$ be $R$-modules with $M$, $P$, $P'$ also being $A$-modules. For any $A$-linear maps $f_1 \colon M \to P$ and $f_2 \colon P \to P'$, and any $R$-linear maps $g_1 \colon N \to Q$ and $g_2 \colon Q \to Q'$, the composition of 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). \]

TensorProduct.AlgebraTensorModule.map_one theorem

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

Full source

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

Identity Tensor Map is Identity

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $M$, $N$ be $R$-modules with $M$ also being an $A$-module. The tensor product map of the identity $A$-linear map on $M$ and the identity $R$-linear map on $N$ is equal to the identity map on $M \otimes_R N$.

TensorProduct.AlgebraTensorModule.map_mul theorem

 (f₁ f₂ : M →ₗ[A] 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 →ₗ[A] M) (g₁ g₂ : N →ₗ[R] N) :
    map (f₁ * f₂) (g₁ * g₂) = map f₁ g₁ * map f₂ g₂ := map_comp _ _ _ _

Composition of Tensor Product Maps for Endomorphisms: $\text{map}(f_1 \circ f_2, g_1 \circ g_2) = \text{map}(f_1, g_1) \circ \text{map}(f_2, g_2)$

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $M$, $N$ be $R$-modules with $M$ also being an $A$-module. For any $A$-linear endomorphisms $f_1, f_2$ of $M$ and any $R$-linear endomorphisms $g_1, g_2$ of $N$, the tensor product map satisfies: \[ \text{map}(f_1 \circ f_2, g_1 \circ g_2) = \text{map}(f_1, g_1) \circ \text{map}(f_2, g_2). \]

TensorProduct.AlgebraTensorModule.map_add_left theorem

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

Full source

theorem map_add_left (f₁ f₂ : M →ₗ[A] P) (g : N →ₗ[R] Q) :
    map (f₁ + f₂) g = map f₁ g + map f₂ g := by
  ext
  simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, add_apply, map_tmul,
    add_apply, add_tmul]

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

For any $A$-linear maps $f_1, f_2 \colon M \to P$ and any $R$-linear map $g \colon N \to Q$, the tensor product map satisfies the additive property in the first argument: \[ \text{map}(f_1 + f_2, g) = \text{map}(f_1, g) + \text{map}(f_2, g). \]

TensorProduct.AlgebraTensorModule.map_add_right theorem

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

Full source

theorem map_add_right (f : M →ₗ[A] P) (g₁ g₂ : N →ₗ[R] Q) :
    map f (g₁ + g₂) = map f g₁ + map f g₂ := by
  ext
  simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, add_apply, map_tmul,
    add_apply, tmul_add]

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

Informal description

For any $A$-linear map $f \colon M \to P$ and any $R$-linear maps $g_1, g_2 \colon N \to Q$, 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.AlgebraTensorModule.map_smul_right theorem

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

Full source

theorem map_smul_right (r : R) (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : map f (r • g) = r • map f g := by
  ext
  simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, smul_apply, map_tmul,
    smul_apply, tmul_smul]

Scalar multiplication commutes with tensor product map on the right: $\text{map}(f, r \cdot g) = r \cdot \text{map}(f, g)$

Informal description

Let $R$ be a commutative semiring, $A$ an $R$-algebra, and $M$, $P$ be $A$-modules while $N$, $Q$ are $R$-modules. For any scalar $r \in R$ and linear maps $f \colon M \to P$ (which is $A$-linear) and $g \colon N \to Q$ (which is $R$-linear), the following equality holds in the space of $R$-linear maps from $M \otimes_R N$ to $P \otimes_R Q$: \[ \text{map}(f, r \cdot g) = r \cdot \text{map}(f, g). \]

TensorProduct.AlgebraTensorModule.map_smul_left theorem

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

Full source

theorem map_smul_left (b : B) (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : map (b • f) g = b • map f g := by
  ext
  simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, smul_apply, map_tmul,
    smul_apply, smul_tmul']

Scalar Multiplication Commutes with Tensor Product Map on the Left

Informal description

For any scalar $b \in B$, any $A$-linear map $f \colon M \to P$, and any $R$-linear map $g \colon N \to Q$, the tensor product map satisfies the scalar multiplication property: \[ \text{map}(b \cdot f, g) = b \cdot \text{map}(f, g). \]

TensorProduct.AlgebraTensorModule.coe_lTensor theorem

(f : N →ₗ[R] Q) : (lTensor A M f : M ⊗[R] N → M ⊗[R] Q) = f.lTensor M

Full source

@[simp]
lemma coe_lTensor (f : N →ₗ[R] Q) :
    (lTensor A M f : M ⊗[R] N → M ⊗[R] Q) = f.lTensor M := rfl

Equality of Left Tensor Product Maps

Informal description

For any $R$-linear map $f \colon N \to Q$, the linear map $\mathrm{lTensor}_A M f \colon M \otimes_R N \to M \otimes_R Q$ (where $M$ is an $A$-module and $N,Q$ are $R$-modules) coincides with the standard left tensor product map $f.\mathrm{lTensor} M$.

TensorProduct.AlgebraTensorModule.restrictScalars_lTensor theorem

(f : N →ₗ[R] Q) : (lTensor A M f).restrictScalars R = f.lTensor M

Full source

@[simp]
lemma restrictScalars_lTensor (f : N →ₗ[R] Q) :
    (lTensor A M f).restrictScalars R = f.lTensor M := rfl

Restriction of Scalars Commutes with Left Tensor Product

Informal description

For any $R$-linear map $f : N \to Q$, the restriction of scalars of the left tensor product map $A \otimes M f$ to $R$ is equal to the left tensor product map $f \otimes M$ over $R$.

TensorProduct.AlgebraTensorModule.lTensor_tmul theorem

(f : N →ₗ[R] Q) (m : M) (n : N) : lTensor A M f (m ⊗ₜ[R] n) = m ⊗ₜ f n

Full source

@[simp] lemma lTensor_tmul (f : N →ₗ[R] Q) (m : M) (n : N) :
    lTensor A M f (m ⊗ₜ[R] n) = m ⊗ₜ f n :=
  rfl

Action of Left Tensor Product on Simple Tensors

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $M$ an $A$-module that is also an $R$-module. For any $R$-linear map $f : N \to Q$ between $R$-modules $N$ and $Q$, the action of the linear map $\text{lTensor}_A^M f$ on a simple tensor $m \otimes n \in M \otimes_R N$ is given by $(\text{lTensor}_A^M f)(m \otimes n) = m \otimes f(n)$.

TensorProduct.AlgebraTensorModule.lTensor_id theorem

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

Full source

@[simp] lemma lTensor_id : lTensor A M (id : N →ₗ[R] N) = .id :=
  ext fun _ _ => rfl

Left Tensor Product Preserves Identity Map

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $M$ an $A$-module that is also an $R$-module. The left tensor product map $\text{lTensor}_A^M$ applied to the identity $R$-linear map $\text{id} : N \to N$ is equal to the identity map on $M \otimes_R N$.

TensorProduct.AlgebraTensorModule.lTensor_comp theorem

 (f₂ : Q →ₗ[R] Q') (f₁ : N →ₗ[R] Q) : lTensor A M (f₂.comp f₁) = (lTensor A M f₂).comp (lTensor A M f₁)

Full source

lemma lTensor_comp (f₂ : Q →ₗ[R] Q') (f₁ : N →ₗ[R] Q) :
    lTensor A M (f₂.comp f₁) = (lTensor A M f₂).comp (lTensor A M f₁) :=
  ext fun _ _ => rfl

Composition of Linear Maps Preserved by Left Tensor Product Functor

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $M$ an $A$-module that is also an $R$-module. For any $R$-linear maps $f_1 \colon N \to Q$ and $f_2 \colon Q \to Q'$ between $R$-modules $N$, $Q$, and $Q'$, the left tensor product functor $\text{lTensor}_A^M$ satisfies: \[ \text{lTensor}_A^M (f_2 \circ f_1) = (\text{lTensor}_A^M f_2) \circ (\text{lTensor}_A^M f_1) \]

TensorProduct.AlgebraTensorModule.lTensor_one theorem

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

Full source

@[simp]
lemma lTensor_one : lTensor A M (1 : N →ₗ[R] N) = 1 := map_id

Left Tensor Product Functor Preserves Identity Map

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $M$ an $A$-module that is also an $R$-module. The left tensor product functor $\text{lTensor}_A^M$ applied to the identity $R$-linear map $1 \colon N \to N$ is equal to the identity map on $M \otimes_R N$.

TensorProduct.AlgebraTensorModule.lTensor_mul theorem

(f₁ f₂ : N →ₗ[R] N) : lTensor A M (f₁ * f₂) = lTensor A M f₁ * lTensor A M f₂

Full source

lemma lTensor_mul (f₁ f₂ : N →ₗ[R] N) :
    lTensor A M (f₁ * f₂) = lTensor A M f₁ * lTensor A M f₂ := lTensor_comp _ _

Left Tensor Product Functor Preserves Composition of Linear Endomorphisms

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $M$ an $A$-module that is also an $R$-module. For any $R$-linear endomorphisms $f_1, f_2 \colon N \to N$ of an $R$-module $N$, the left tensor product functor $\text{lTensor}_A^M$ satisfies: \[ \text{lTensor}_A^M (f_1 \circ f_2) = (\text{lTensor}_A^M f_1) \circ (\text{lTensor}_A^M f_2) \]

TensorProduct.AlgebraTensorModule.coe_rTensor theorem

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

Full source

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

Right Tensor Product Map Coincides with Tensor Product of Map and Identity

Informal description

For any $A$-linear map $f \colon M \to P$, the map $\operatorname{rTensor}_R N f \colon M \otimes_R N \to P \otimes_R N$ coincides with the right tensor product map $f \otimes_R \operatorname{id}_N$.

TensorProduct.AlgebraTensorModule.restrictScalars_rTensor theorem

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

Full source

@[simp]
lemma restrictScalars_rTensor (f : M →ₗ[A] P) :
    (rTensor R N f).restrictScalars R = f.rTensor N := rfl

Restriction of Scalars Commutes with Right Tensor Product of Linear Maps

Informal description

Let $R$ be a commutative ring, $A$ be an $R$-algebra, and $M$, $N$, $P$ be $R$-modules where $M$ and $P$ are also $A$-modules. For any $A$-linear map $f : M \to P$, the restriction of scalars of the $R$-linear map $\text{rTensor}_R N f : M \otimes_R N \to P \otimes_R N$ to $R$ is equal to the $R$-linear map $\text{rTensor}_R N f$.

TensorProduct.AlgebraTensorModule.rTensor_tmul theorem

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

Full source

@[simp] lemma rTensor_tmul (f : M →ₗ[A] P) (m : M) (n : N) :
    rTensor R N f (m ⊗ₜ[R] n) = f m ⊗ₜ n :=
  rfl

Right Tensor Product Action on Pure Tensors

Informal description

Let $R$ and $A$ be rings with an algebra structure from $R$ to $A$, and let $M$, $N$, $P$ be $R$-modules where $M$ and $P$ are also $A$-modules. For any $A$-linear map $f : M \to P$, the right tensor product map $\text{rTensor}_R N f : M \otimes_R N \to P \otimes_R N$ satisfies \[ (\text{rTensor}_R N f)(m \otimes n) = f(m) \otimes n \] for all $m \in M$ and $n \in N$.

TensorProduct.AlgebraTensorModule.rTensor_id theorem

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

Full source

@[simp] lemma rTensor_id : rTensor R N (id : M →ₗ[A] M) = .id :=
  ext fun _ _ => rfl

Right Tensor Product of Identity Map is Identity

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $M$, $N$ be $R$-modules with $M$ also being an $A$-module. The right tensor product of the identity $A$-linear map $\text{id} : M \to M$ with $N$ over $R$ is equal to the identity map on $M \otimes_R N$.

TensorProduct.AlgebraTensorModule.rTensor_comp theorem

 (f₂ : P →ₗ[A] P') (f₁ : M →ₗ[A] P) : rTensor R N (f₂.comp f₁) = (rTensor R N f₂).comp (rTensor R N f₁)

Full source

lemma rTensor_comp (f₂ : P →ₗ[A] P') (f₁ : M →ₗ[A] P) :
    rTensor R N (f₂.comp f₁) = (rTensor R N f₂).comp (rTensor R N f₁) :=
  ext fun _ _ => rfl

Composition Law for Right Tensor Product of $A$-Linear Maps

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $M$, $N$, $P$, $P'$ be $R$-modules with $M$, $P$, and $P'$ also being $A$-modules. For any $A$-linear maps $f_1: M \to P$ and $f_2: P \to P'$, the right tensor product map satisfies \[ \text{rTensor}_R N (f_2 \circ f_1) = (\text{rTensor}_R N f_2) \circ (\text{rTensor}_R N f_1) \] where $\circ$ denotes composition of linear maps.

TensorProduct.AlgebraTensorModule.rTensor_one theorem

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

Full source

@[simp]
lemma rTensor_one : rTensor R N (1 : M →ₗ[A] M) = 1 := map_id

Right Tensor Product Preserves Multiplicative Identity

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $M$, $N$ be $R$-modules with $M$ also being an $A$-module. The right tensor product of the multiplicative identity $1 : M \to M$ in the $A$-module endomorphisms with $N$ over $R$ is equal to the multiplicative identity on $M \otimes_R N$.

TensorProduct.AlgebraTensorModule.rTensor_mul theorem

(f₁ f₂ : M →ₗ[A] M) : rTensor R M (f₁ * f₂) = rTensor R M f₁ * rTensor R M f₂

Full source

lemma rTensor_mul (f₁ f₂ : M →ₗ[A] M) :
    rTensor R M (f₁ * f₂) = rTensor R M f₁ * rTensor R M f₂ := rTensor_comp _ _

Multiplicativity of Right Tensor Product for $A$-Linear Endomorphisms

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $M$ an $R$-module that is also an $A$-module. For any two $A$-linear endomorphisms $f_1, f_2: M \to M$, the right tensor product map satisfies \[ \text{rTensor}_R M (f_1 \circ f_2) = (\text{rTensor}_R M f_1) \circ (\text{rTensor}_R M f_2), \] where $\circ$ denotes composition of linear maps (or equivalently, multiplication in the endomorphism algebra).

TensorProduct.AlgebraTensorModule.mapBilinear_apply theorem

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

Full source

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

Bilinear Tensor Product Map Evaluation: $\text{mapBilinear}(f,g) = f \otimes g$

Informal description

For any $A$-linear map $f \colon M \to P$ and $R$-linear map $g \colon N \to Q$, the bilinear map `mapBilinear` applied to $f$ and $g$ equals the tensor product map $f \otimes g$.

TensorProduct.AlgebraTensorModule.homTensorHomMap_apply theorem

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

Full source

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

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

Informal description

For any $A$-linear map $f \colon M \to P$ and $R$-linear map $g \colon N \to Q$, the map $\text{homTensorHomMap}_{R,A,B,M,N,P,Q}$ applied to the tensor product $f \otimes g$ equals the tensor product map $f \otimes g$ from $M \otimes_R N$ to $P \otimes_R Q$.

TensorProduct.AlgebraTensorModule.congr_refl theorem

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

Full source

@[simp]
theorem congr_refl : congr (.refl A M) (.refl R N) = .refl A _ :=
  LinearEquiv.toLinearMap_injective <| map_id

Tensor Product of Identity Equivalences is Identity

Informal description

The tensor product of the identity $A$-linear equivalence on $M$ and the identity $R$-linear equivalence on $N$ is equal to the identity $A$-linear equivalence on $M \otimes_R N$. That is, $\text{congr}(\text{id}_M, \text{id}_N) = \text{id}_{M \otimes_R N}$.

TensorProduct.AlgebraTensorModule.congr_trans theorem

 (f₁ : M ≃ₗ[A] P) (f₂ : P ≃ₗ[A] P') (g₁ : N ≃ₗ[R] Q) (g₂ : Q ≃ₗ[R] Q') :
  congr (f₁.trans f₂) (g₁.trans g₂) = (congr f₁ g₁).trans (congr f₂ g₂)

Full source

theorem congr_trans (f₁ : M ≃ₗ[A] P) (f₂ : P ≃ₗ[A] P') (g₁ : N ≃ₗ[R] Q) (g₂ : Q ≃ₗ[R] Q') :
    congr (f₁.trans f₂) (g₁.trans g₂) = (congr f₁ g₁).trans (congr f₂ g₂) :=
  LinearEquiv.toLinearMap_injective <| map_comp _ _ _ _

Composition of Tensor Product Equivalences

Informal description

Let $R$ be a commutative ring and $A$ an $R$-algebra. Let $M$, $P$, $P'$ be $A$-modules and $N$, $Q$, $Q'$ be $R$-modules. For any $A$-linear equivalences $f_1: M \simeq P$, $f_2: P \simeq P'$ and $R$-linear equivalences $g_1: N \simeq Q$, $g_2: Q \simeq Q'$, the tensor product of the composed equivalences satisfies: \[ \text{congr}(f_2 \circ f_1, g_2 \circ g_1) = \text{congr}(f_1, g_1) \circ \text{congr}(f_2, g_2) \] where $\text{congr}$ denotes the tensor product of equivalences.

TensorProduct.AlgebraTensorModule.congr_symm theorem

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

Full source

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

Inverse of Tensor Product of Equivalences

Informal description

Let $M$ and $P$ be $A$-modules, and $N$ and $Q$ be $R$-modules. For any $A$-linear equivalence $f: M \simeq P$ and $R$-linear equivalence $g: N \simeq Q$, the equivalence obtained by tensoring the inverse equivalences $f^{-1}$ and $g^{-1}$ is equal to the inverse of the tensor product equivalence $f \otimes g$. That is, $(f \otimes g)^{-1} = f^{-1} \otimes g^{-1}$.

TensorProduct.AlgebraTensorModule.congr_one theorem

: congr (1 : M ≃ₗ[A] M) (1 : N ≃ₗ[R] N) = 1

Full source

@[simp]
theorem congr_one : congr (1 : M ≃ₗ[A] M) (1 : N ≃ₗ[R] N) = 1 := congr_refl

Tensor Product of Identity Maps is Identity

Informal description

The tensor product of the identity $A$-linear equivalence on $M$ and the identity $R$-linear equivalence on $N$ is equal to the identity $A$-linear equivalence on $M \otimes_R N$. That is, $\text{congr}(\text{id}_M, \text{id}_N) = \text{id}_{M \otimes_R N}$.

TensorProduct.AlgebraTensorModule.congr_mul theorem

 (f₁ f₂ : M ≃ₗ[A] M) (g₁ g₂ : N ≃ₗ[R] N) : congr (f₁ * f₂) (g₁ * g₂) = congr f₁ g₁ * congr f₂ g₂

Full source

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

Composition of Tensor Product Equivalences Preserves Multiplication

Informal description

Let $M$ be an $A$-module and $N$ be an $R$-module. For any $A$-linear equivalences $f_1, f_2 : M \simeq M$ and $R$-linear equivalences $g_1, g_2 : N \simeq N$, the tensor product of the composed equivalences satisfies: \[ \text{congr}(f_2 \circ f_1, g_2 \circ g_1) = \text{congr}(f_1, g_1) \circ \text{congr}(f_2, g_2) \] where $\text{congr}$ denotes the tensor product of equivalences.

TensorProduct.AlgebraTensorModule.congr_tmul theorem

(f : M ≃ₗ[A] 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 ≃ₗ[A] 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 Action

Informal description

Let $M$ and $P$ be $A$-modules and $R$-modules, and let $N$ and $Q$ be $R$-modules. For any $A$-linear equivalence $f : M \simeq P$ and $R$-linear equivalence $g : N \simeq Q$, the tensor product congruence map $\text{congr}(f, g)$ satisfies $\text{congr}(f, g)(m \otimes n) = f(m) \otimes g(n)$ for all $m \in M$ and $n \in N$.

TensorProduct.AlgebraTensorModule.congr_symm_tmul theorem

(f : M ≃ₗ[A] 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 ≃ₗ[A] P) (g : N ≃ₗ[R] Q) (p : P) (q : Q) :
    (congr f g).symm (p ⊗ₜ q) = f.symm p ⊗ₜ g.symm q :=
  rfl

Inverse Tensor Congruence Map on Pure Tensors

Informal description

Let $f : M \simeq_A P$ and $g : N \simeq_R Q$ be linear equivalences of modules, where $M$ and $P$ are $A$-modules and $N$ and $Q$ are $R$-modules. For any $p \in P$ and $q \in Q$, the inverse of the tensor product congruence map $\text{congr}(f, g)$ satisfies $$(\text{congr}(f, g))^{-1}(p \otimes q) = f^{-1}(p) \otimes g^{-1}(q).$$

TensorProduct.AlgebraTensorModule.rid_eq_rid theorem

: AlgebraTensorModule.rid R R M = TensorProduct.rid R M

Full source

theorem rid_eq_rid : AlgebraTensorModule.rid R R M = TensorProduct.rid R M :=
  LinearEquiv.toLinearMap_injective <| TensorProduct.ext' fun _ _ => rfl

Equality of Right Identity Isomorphisms for Tensor Product Modules

Informal description

The module isomorphism `AlgebraTensorModule.rid R R M` from $M \otimes_R R$ to $M$ is equal to the standard right identity isomorphism `TensorProduct.rid R M`.

TensorProduct.AlgebraTensorModule.rid_tmul theorem

(r : R) (m : M) : AlgebraTensorModule.rid R A M (m ⊗ₜ r) = r • m

Full source

@[simp]
theorem rid_tmul (r : R) (m : M) : AlgebraTensorModule.rid R A M (m ⊗ₜ r) = r • m := rfl

Right identity isomorphism maps tensor product to scalar multiplication

Informal description

For any element $r$ in the ring $R$ and any element $m$ in the $A$-module $M$, the right identity isomorphism $\text{rid}_{R,A,M}$ applied to the tensor product $m \otimes r$ equals the scalar multiplication $r \cdot m$.

TensorProduct.AlgebraTensorModule.rid_symm_apply theorem

(m : M) : (AlgebraTensorModule.rid R A M).symm m = m ⊗ₜ 1

Full source

@[simp]
theorem rid_symm_apply (m : M) : (AlgebraTensorModule.rid R A M).symm m = m ⊗ₜ 1 := rfl

Inverse of Right Identity Isomorphism for Tensor Product Modules

Informal description

For any element $m$ in the $A$-module $M$, the inverse of the right identity isomorphism $\text{rid}_{R,A,M}$ maps $m$ to the tensor product $m \otimes 1$ in $M \otimes_R A$.

TensorProduct.AlgebraTensorModule.assoc_tmul theorem

(m : M) (p : P) (q : Q) : assoc R A B M P Q ((m ⊗ₜ p) ⊗ₜ q) = m ⊗ₜ (p ⊗ₜ q)

Full source

@[simp]
theorem assoc_tmul (m : M) (p : P) (q : Q) :
    assoc R A B M P Q ((m ⊗ₜ p) ⊗ₜ q) = m ⊗ₜ (p ⊗ₜ q) :=
  rfl

Associativity of Tensor Product: $(m \otimes p) \otimes q = m \otimes (p \otimes q)$

Informal description

For any elements $m \in M$, $p \in P$, and $q \in Q$, the associativity isomorphism $\text{assoc}_{R,A,B,M,P,Q}$ maps the tensor product $(m \otimes p) \otimes q$ in $(M \otimes_R P) \otimes_R Q$ to $m \otimes (p \otimes q)$ in $M \otimes_R (P \otimes_R Q)$.

TensorProduct.AlgebraTensorModule.assoc_symm_tmul theorem

(m : M) (p : P) (q : Q) : (assoc R A B M P Q).symm (m ⊗ₜ (p ⊗ₜ q)) = (m ⊗ₜ p) ⊗ₜ q

Full source

@[simp]
theorem assoc_symm_tmul (m : M) (p : P) (q : Q) :
    (assoc R A B M P Q).symm (m ⊗ₜ (p ⊗ₜ q)) = (m ⊗ₜ p) ⊗ₜ q :=
  rfl

Inverse Associator Isomorphism for Tensor Product Modules

Informal description

Let $R$, $A$, and $B$ be rings, and let $M$, $P$, and $Q$ be modules over $R$ where $M$ and $P$ are also $A$-modules. For any elements $m \in M$, $p \in P$, and $q \in Q$, the inverse of the associator isomorphism $\text{assoc}_{R,A,B,M,P,Q}$ maps the tensor product $m \otimes (p \otimes q)$ in $M \otimes_R (P \otimes_R Q)$ to the tensor product $(m \otimes p) \otimes q$ in $(M \otimes_R P) \otimes_R Q$.

TensorProduct.AlgebraTensorModule.rTensor_tensor theorem

 [Module R P'] [IsScalarTower R A P'] (g : P →ₗ[A] P') :
  g.rTensor (M ⊗[R] N) = assoc R A A P' M N ∘ₗ map (g.rTensor M) id ∘ₗ (assoc R A A P M N).symm.toLinearMap

Full source

theorem rTensor_tensor [Module R P'] [IsScalarTower R A P'] (g : P →ₗ[A] P') :
    g.rTensor (M ⊗[R] N) =
      assocassoc R A A P' M N ∘ₗ map (g.rTensor M) id ∘ₗ (assoc R A A P M N).symm.toLinearMap :=
  TensorProduct.ext <| LinearMap.ext fun _ ↦ ext fun _ _ ↦ rfl

Right Tensor Product Map Decomposition via Associator Isomorphisms

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $M$, $N$, $P$, $P'$ be $R$-modules with $P$ and $P'$ also being $A$-modules. Suppose $P'$ is an $R$-module and the scalar multiplication satisfies the compatibility condition $[IsScalarTower R A P']$. For any $A$-linear map $g \colon P \to P'$, the right tensor product map $g \otimes_{R} (M \otimes_{R} N)$ is equal to the composition of the following three maps: 1. The inverse of the associator isomorphism $(P \otimes_{R} M) \otimes_{R} N \to P \otimes_{R} (M \otimes_{R} N)$, 2. The tensor product of the right tensor product map $g \otimes_{R} M$ with the identity map on $N$, 3. The associator isomorphism $P' \otimes_{R} (M \otimes_{R} N) \to (P' \otimes_{R} M) \otimes_{R} N$.

TensorProduct.AlgebraTensorModule.cancelBaseChange_tmul theorem

(m : M) (n : N) (a : A) : cancelBaseChange R A B M N (m ⊗ₜ (a ⊗ₜ n)) = (a • m) ⊗ₜ n

Full source

@[simp]
theorem cancelBaseChange_tmul (m : M) (n : N) (a : A) :
    cancelBaseChange R A B M N (m ⊗ₜ (a ⊗ₜ n)) = (a • m) ⊗ₜ n :=
  rfl

Base Change Cancellation for Tensor Product: $m \otimes (a \otimes n) \mapsto (a \cdot m) \otimes n$

Informal description

Let $R$, $A$, and $B$ be rings, and let $M$ and $N$ be $R$-modules with $M$ also being an $A$-module. For any elements $m \in M$, $n \in N$, and $a \in A$, the map $\text{cancelBaseChange}_{R,A,B,M,N}$ applied to the tensor product $m \otimes (a \otimes n)$ in $M \otimes_R (A \otimes_R N)$ equals the tensor product $(a \cdot m) \otimes n$ in $M \otimes_R N$.

TensorProduct.AlgebraTensorModule.cancelBaseChange_symm_tmul theorem

(m : M) (n : N) : (cancelBaseChange R A B M N).symm (m ⊗ₜ n) = m ⊗ₜ (1 ⊗ₜ n)

Full source

@[simp]
theorem cancelBaseChange_symm_tmul (m : M) (n : N) :
    (cancelBaseChange R A B M N).symm (m ⊗ₜ n) = m ⊗ₜ (1 ⊗ₜ n) :=
  rfl

Inverse Base Change Cancellation on Tensor Product: $(cancelBaseChange)^{-1}(m \otimes n) = m \otimes (1 \otimes n)$

Informal description

For any elements $m \in M$ and $n \in N$, the inverse of the base change cancellation map applied to the tensor product $m \otimes n$ equals the tensor product $m \otimes (1 \otimes n)$, where $1$ is the multiplicative identity in $A$.

TensorProduct.AlgebraTensorModule.lTensor_comp_cancelBaseChange theorem

 (f : N →ₗ[R] Q) :
  lTensor _ _ f ∘ₗ cancelBaseChange R A B M N = (cancelBaseChange R A B M Q).toLinearMap ∘ₗ lTensor _ _ (lTensor _ _ f)

Full source

theorem lTensor_comp_cancelBaseChange (f : N →ₗ[R] Q) :
    lTensorlTensor _ _ f ∘ₗ cancelBaseChange R A B M N =
      (cancelBaseChange R A B M Q).toLinearMap ∘ₗ lTensor _ _ (lTensor _ _ f) := by
  ext; simp

Commutation of Left Tensor Product with Base Change Cancellation

Informal description

Let $R$, $A$, $B$ be rings, and let $M$, $N$, $Q$ be $R$-modules where $M$ is also an $A$-module. For any $R$-linear map $f \colon N \to Q$, the following diagram commutes: \[ \begin{CD} M \otimes_R (A \otimes_R N) @>{f \otimes \text{id}}>> M \otimes_R (A \otimes_R Q) \\ @V{\text{cancelBaseChange}}VV @VV{\text{cancelBaseChange}}V \\ A \otimes_R (M \otimes_R N) @>{f \otimes \text{id}}>> A \otimes_R (M \otimes_R Q) \end{CD} \] where the horizontal maps are the left tensor product of $f$ and the vertical maps are the base change cancellation isomorphisms.

TensorProduct.AlgebraTensorModule.leftComm_tmul theorem

(m : M) (p : P) (q : Q) : leftComm R A M P Q (m ⊗ₜ (p ⊗ₜ q)) = p ⊗ₜ (m ⊗ₜ q)

Full source

@[simp]
theorem leftComm_tmul (m : M) (p : P) (q : Q) :
    leftComm R A M P Q (m ⊗ₜ (p ⊗ₜ q)) = p ⊗ₜ (m ⊗ₜ q) :=
  rfl

Left Commutativity Isomorphism for Tensor Products: $m \otimes (p \otimes q) \mapsto p \otimes (m \otimes q)$

Informal description

For any elements $m \in M$, $p \in P$, and $q \in Q$, the left commutativity isomorphism $\text{leftComm}_{R,A,M,P,Q}$ satisfies \[ \text{leftComm}_{R,A,M,P,Q} (m \otimes (p \otimes q)) = p \otimes (m \otimes q). \]

TensorProduct.AlgebraTensorModule.leftComm_symm_tmul theorem

(m : M) (p : P) (q : Q) : (leftComm R A M P Q).symm (p ⊗ₜ (m ⊗ₜ q)) = m ⊗ₜ (p ⊗ₜ q)

Full source

@[simp]
theorem leftComm_symm_tmul (m : M) (p : P) (q : Q) :
    (leftComm R A M P Q).symm (p ⊗ₜ (m ⊗ₜ q)) = m ⊗ₜ (p ⊗ₜ q) :=
  rfl

Inverse Left Commutativity Isomorphism for Tensor Products: $p \otimes (m \otimes q) \mapsto m \otimes (p \otimes q)$

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $M$, $P$, $Q$ be $R$-modules with $M$ also an $A$-module. For any elements $m \in M$, $p \in P$, and $q \in Q$, the inverse of the left commutativity isomorphism satisfies \[ (\text{leftComm}_{R,A,M,P,Q})^{-1}(p \otimes (m \otimes q)) = m \otimes (p \otimes q). \]

TensorProduct.AlgebraTensorModule.rightComm_tmul theorem

(m : M) (p : P) (q : Q) : rightComm R A M P Q ((m ⊗ₜ p) ⊗ₜ q) = (m ⊗ₜ q) ⊗ₜ p

Full source

@[simp]
theorem rightComm_tmul (m : M) (p : P) (q : Q) :
    rightComm R A M P Q ((m ⊗ₜ p) ⊗ₜ q) = (m ⊗ₜ q) ⊗ₜ p :=
  rfl

Right Commutativity Isomorphism for Tensor Products: $(m \otimes p) \otimes q \mapsto (m \otimes q) \otimes p$

Informal description

For any elements $m \in M$, $p \in P$, and $q \in Q$, the right commutativity isomorphism `rightComm` satisfies \[ \text{rightComm}_{R,A,M,P,Q} ((m \otimes p) \otimes q) = (m \otimes q) \otimes p. \]

TensorProduct.AlgebraTensorModule.rightComm_symm_tmul theorem

(m : M) (p : P) (q : Q) : (rightComm R A M P Q).symm ((m ⊗ₜ q) ⊗ₜ p) = (m ⊗ₜ p) ⊗ₜ q

Full source

@[simp]
theorem rightComm_symm_tmul (m : M) (p : P) (q : Q) :
    (rightComm R A M P Q).symm ((m ⊗ₜ q) ⊗ₜ p) = (m ⊗ₜ p) ⊗ₜ q :=
  rfl

Inverse Right Commutativity Isomorphism for Tensor Products of Modules

Informal description

Let $M$, $P$, and $Q$ be modules over a commutative ring $R$, with $M$ also being a module over an $R$-algebra $A$. For any elements $m \in M$, $p \in P$, and $q \in Q$, the inverse of the right commutativity isomorphism applied to the tensor product $(m \otimes q) \otimes p$ equals $(m \otimes p) \otimes q$.

TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_tmul theorem

 (m : M) (n : N) (p : P) (q : Q) : tensorTensorTensorComm R A M N P Q ((m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q)) = (m ⊗ₜ p) ⊗ₜ (n ⊗ₜ q)

Full source

@[simp]
theorem tensorTensorTensorComm_tmul (m : M) (n : N) (p : P) (q : Q) :
    tensorTensorTensorComm R A M N P Q ((m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q)) = (m ⊗ₜ p) ⊗ₜ (n ⊗ₜ q) :=
  rfl

Tensor Tensor Tensor Commutativity Isomorphism: $(m \otimes n) \otimes (p \otimes q) \mapsto (m \otimes p) \otimes (n \otimes q)$

Informal description

Let $R$ be a commutative ring and $A$ an $R$-algebra. Let $M$, $N$, $P$, $Q$ be $R$-modules, with $M$ and $P$ also being $A$-modules. For any elements $m \in M$, $n \in N$, $p \in P$, and $q \in Q$, the tensor tensor tensor commutativity isomorphism satisfies \[ \text{tensorTensorTensorComm}_{R,A,M,N,P,Q} \big((m \otimes n) \otimes (p \otimes q)\big) = (m \otimes p) \otimes (n \otimes q). \]

TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_symm_tmul theorem

 (m : M) (n : N) (p : P) (q : Q) :
  (tensorTensorTensorComm R A M N P Q).symm ((m ⊗ₜ p) ⊗ₜ (n ⊗ₜ q)) = (m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q)

Full source

@[simp]
theorem tensorTensorTensorComm_symm_tmul (m : M) (n : N) (p : P) (q : Q) :
    (tensorTensorTensorComm R A M N P Q).symm ((m ⊗ₜ p) ⊗ₜ (n ⊗ₜ q)) = (m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q) :=
  rfl

Inverse Tensor Commutativity Isomorphism for Quadruple Tensor Products

Informal description

Let $R$ be a commutative ring and $A$ an $R$-algebra. Let $M$, $N$, $P$, $Q$ be $R$-modules, with $M$ and $P$ also being $A$-modules. For any elements $m \in M$, $n \in N$, $p \in P$, $q \in Q$, the inverse of the tensor tensor tensor commutativity isomorphism satisfies \[ (tensorTensorTensorComm\ R\ A\ M\ N\ P\ Q)^{-1}\big((m \otimes p) \otimes (n \otimes q)\big) = (m \otimes n) \otimes (p \otimes q). \]

Submodule.baseChange_bot theorem

: (⊥ : Submodule R M).baseChange A = ⊥

Full source

@[simp]
lemma baseChange_bot : (⊥ : Submodule R M).baseChange A = ⊥ := by simp [baseChange]

Base Change Preserves Trivial Submodule

Informal description

For any commutative ring $R$ and $R$-algebra $A$, the base change of the trivial submodule $\bot$ of an $R$-module $M$ is equal to the trivial submodule $\bot$ of $M \otimes_R A$. That is, $(\bot : \text{Submodule}_R M).\text{baseChange} A = \bot$.

Submodule.baseChange_top theorem

: (⊤ : Submodule R M).baseChange A = ⊤

Full source

@[simp]
lemma baseChange_top : (⊤ : Submodule R M).baseChange A = ⊤ := by
  rw [baseChange, map_top, eq_top_iff']
  intro x
  refine x.induction_on (by simp) (fun a y ↦ ?_) (fun _ _ ↦ Submodule.add_mem _)
  rw [← mul_one a, ← smul_eq_mul, ← smul_tmul']
  refine smul_mem _ _ (subset_span ?_)
  simp

Base Change Preserves Top Submodule

Informal description

For any $R$-module $M$ and $A$-algebra $R$, the base change of the top submodule of $M$ to $A$ is equal to the top submodule of $M \otimes_R A$. That is, \[ (\top : \text{Submodule } R M).\text{baseChange } A = \top. \]

Submodule.tmul_mem_baseChange_of_mem theorem

(a : A) {m : M} (hm : m ∈ p) : a ⊗ₜ[R] m ∈ p.baseChange A

Full source

lemma tmul_mem_baseChange_of_mem (a : A) {m : M} (hm : m ∈ p) :
    a ⊗ₜ[R] ma ⊗ₜ[R] m ∈ p.baseChange A := by
  rw [← mul_one a, ← smul_eq_mul, ← smul_tmul']
  exact smul_mem (baseChange A p) a (subset_span ⟨m, hm, rfl⟩)

Tensor product element belongs to base change of submodule

Informal description

For any element $a \in A$ and any element $m \in M$ such that $m$ belongs to a submodule $p$ of $M$, the tensor product $a \otimes_R m$ belongs to the base change of $p$ with respect to $A$.

Submodule.baseChange_span theorem

(s : Set M) : (span R s).baseChange A = span A (TensorProduct.mk R A M 1 '' s)

Full source

@[simp]
lemma baseChange_span (s : Set M) :
    (span R s).baseChange A = span A (TensorProduct.mkTensorProduct.mk R A M 1 '' s) := by
  simp only [baseChange, map_coe]
  refine le_antisymm (span_le.mpr ?_) (span_mono <| Set.image_subset _ subset_span)
  rintro - ⟨m : M, hm : m ∈ span R s, rfl⟩
  apply span_induction (p := fun m' _ ↦ (1 : A) ⊗ₜ[R] m'(1 : A) ⊗ₜ[R] m' ∈ span A (TensorProduct.mk R A M 1 '' s))
    (hx := hm)
  · intro m hm
    exact subset_span ⟨m, hm, rfl⟩
  · simp
  · intro m₁ m₂ _ _ hm₁ hm₂
    rw [tmul_add]
    exact Submodule.add_mem _ hm₁ hm₂
  · intro r m' _ hm'
    rw [tmul_smul, ← one_smul A ((1 : A) ⊗ₜ[R] m'), ← smul_assoc]
    exact smul_mem _ (r • 1) hm'

Base Change of Span Equals Span of Base Changed Generators

Informal description

Let $R$ be a commutative semiring, $A$ an $R$-algebra, and $M$ an $R$-module. For any subset $s$ of $M$, the base change of the $R$-linear span of $s$ to $A$ is equal to the $A$-linear span of the image of $s$ under the map $m \mapsto 1 \otimes m$ in $A \otimes_R M$. That is, \[ (\operatorname{span}_R s).\text{baseChange} A = \operatorname{span}_A \{1 \otimes m \mid m \in s\}. \]

Mathlib.LinearAlgebra.TensorProduct.Tower

Main definitions

Implementation notes