Mathlib.RingTheory.TensorProduct.Basic

LinearMap.baseChange_tmul theorem

(a : A) (x : M) : f.baseChange A (a ⊗ₜ x) = a ⊗ₜ f x

Full source

@[simp]
theorem baseChange_tmul (a : A) (x : M) : f.baseChange A (a ⊗ₜ x) = a ⊗ₜ f x :=
  rfl

Base Change Action on Tensor Product: $f.\text{baseChange}_A(a \otimes x) = a \otimes f(x)$

Informal description

For any element $a \in A$ and any $x \in M$, the base change of an $R$-linear map $f \colon M \to N$ applied to the tensor product $a \otimes x$ is equal to the tensor product $a \otimes f(x)$, i.e., $f.\text{baseChange}_A(a \otimes x) = a \otimes f(x)$.

LinearMap.baseChange_eq_ltensor theorem

: (f.baseChange A : A ⊗ M → A ⊗ N) = f.lTensor A

Full source

theorem baseChange_eq_ltensor : (f.baseChange A : A ⊗ M → A ⊗ N) = f.lTensor A :=
  rfl

Base Change Equals Left Tensor Product: $f.\text{baseChange}_A = f.\text{lTensor}_A$

Informal description

The base change of an $R$-linear map $f \colon M \to N$ to an $A$-module is equal to the left tensor product map $f$ with $A$, i.e., $(f.\text{baseChange}_A \colon A \otimes M \to A \otimes N) = (f.\text{lTensor}_A \colon A \otimes M \to A \otimes N)$.

LinearMap.baseChange_add theorem

: (f + g).baseChange A = f.baseChange A + g.baseChange A

Full source

@[simp]
theorem baseChange_add : (f + g).baseChange A = f.baseChange A + g.baseChange A := by
  ext
  -- Porting note: added `-baseChange_tmul`
  simp [baseChange_eq_ltensor, -baseChange_tmul]

Base Change Preserves Addition: $(f + g).\text{baseChange}_A = f.\text{baseChange}_A + g.\text{baseChange}_A$

Informal description

For any two $R$-linear maps $f, g \colon M \to N$, the base change of their sum to an $A$-module is equal to the sum of their base changes, i.e., $(f + g).\text{baseChange}_A = f.\text{baseChange}_A + g.\text{baseChange}_A$.

LinearMap.baseChange_zero theorem

: baseChange A (0 : M →ₗ[R] N) = 0

Full source

@[simp]
theorem baseChange_zero : baseChange A (0 : M →ₗ[R] N) = 0 := by
  ext
  simp [baseChange_eq_ltensor]

Base Change of Zero Map is Zero

Informal description

The base change of the zero linear map $0 \colon M \to N$ to an $A$-module is the zero map, i.e., $(0 \colon M \to N).\text{baseChange}_A = 0 \colon A \otimes M \to A \otimes N$.

LinearMap.baseChange_smul theorem

: (r • f).baseChange A = r • f.baseChange A

Full source

@[simp]
theorem baseChange_smul : (r • f).baseChange A = r • f.baseChange A := by
  ext
  simp [baseChange_tmul]

Base Change Preserves Scalar Multiplication: $(r \cdot f).\text{baseChange}_A = r \cdot (f.\text{baseChange}_A)$

Informal description

For any scalar $r$ in the base ring $R$ and any $R$-linear map $f \colon M \to N$, the base change of the scalar multiple $r \cdot f$ to an $A$-module is equal to the scalar multiple $r$ applied to the base change of $f$, i.e., $(r \cdot f).\text{baseChange}_A = r \cdot (f.\text{baseChange}_A)$.

LinearMap.baseChange_id theorem

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

Full source

@[simp]
lemma baseChange_id : (.id : M →ₗ[R] M).baseChange A = .id := by
  ext; simp

Base Change of Identity Map is Identity

Informal description

The base change of the identity linear map $\text{id} \colon M \to M$ to an $A$-module is the identity map, i.e., $\text{id}.\text{baseChange}_A = \text{id} \colon A \otimes M \to A \otimes M$.

LinearMap.baseChange_comp theorem

(g : N →ₗ[R] P) : (g ∘ₗ f).baseChange A = g.baseChange A ∘ₗ f.baseChange A

Full source

lemma baseChange_comp (g : N →ₗ[R] P) :
    (g ∘ₗ f).baseChange A = g.baseChange A ∘ₗ f.baseChange A := by
  ext; simp

Base Change Preserves Composition: $(g \circ f).\text{baseChange}_A = g.\text{baseChange}_A \circ f.\text{baseChange}_A$

Informal description

For any $R$-linear maps $f \colon M \to N$ and $g \colon N \to P$, the base change of the composition $g \circ f$ to an $A$-module is equal to the composition of the base changes of $g$ and $f$, i.e., $(g \circ f).\text{baseChange}_A = g.\text{baseChange}_A \circ f.\text{baseChange}_A$.

LinearMap.baseChange_one theorem

: (1 : Module.End R M).baseChange A = 1

Full source

@[simp]
lemma baseChange_one : (1 : Module.End R M).baseChange A = 1 := baseChange_id

Base Change of Identity Endomorphism is Identity

Informal description

The base change of the identity endomorphism $1 \colon M \to M$ to an $A$-module is the identity endomorphism, i.e., $1.\text{baseChange}_A = 1 \colon A \otimes M \to A \otimes M$.

LinearMap.baseChange_mul theorem

(f g : Module.End R M) : (f * g).baseChange A = f.baseChange A * g.baseChange A

Full source

lemma baseChange_mul (f g : Module.End R M) :
    (f * g).baseChange A = f.baseChange A * g.baseChange A := by
  ext; simp

Base Change Preserves Multiplication of Linear Endomorphisms

Informal description

For any two $R$-linear endomorphisms $f$ and $g$ of an $R$-module $M$, and for any $R$-algebra $A$, the base change of the product $f * g$ is equal to the product of the base changes, i.e., $(f * g)_{\text{baseChange } A} = f_{\text{baseChange } A} * g_{\text{baseChange } A}$.

LinearMap.baseChange_pow theorem

(f : Module.End R M) (n : ℕ) : (f ^ n).baseChange A = f.baseChange A ^ n

Full source

lemma baseChange_pow (f : Module.End R M) (n : ℕ) :
    (f ^ n).baseChange A = f.baseChange A ^ n :=
  map_pow (Module.End.baseChangeHom _ _ _) f n

Power Preservation under Base Change of Linear Endomorphisms

Informal description

Let $M$ be an $R$-module and $A$ be an $R$-algebra. For any $R$-linear endomorphism $f$ of $M$ and any natural number $n$, the base change of $f^n$ to $A$ equals the $n$-th power of the base change of $f$, i.e., $(f^n)_{\text{baseChange } A} = (f_{\text{baseChange } A})^n$.

LinearMap.baseChange_sub theorem

: (f - g).baseChange A = f.baseChange A - g.baseChange A

Full source

@[simp]
theorem baseChange_sub : (f - g).baseChange A = f.baseChange A - g.baseChange A := by
  ext
  simp [baseChange_eq_ltensor, tmul_sub]

Base Change Preserves Subtraction of Linear Maps

Informal description

For any two $R$-linear maps $f$ and $g$ and any $R$-algebra $A$, the base change of the difference $f - g$ is equal to the difference of the base changes, i.e., $(f - g)_{\text{baseChange } A} = f_{\text{baseChange } A} - g_{\text{baseChange } A}$.

LinearMap.baseChange_neg theorem

: (-f).baseChange A = -f.baseChange A

Full source

@[simp]
theorem baseChange_neg : (-f).baseChange A = -f.baseChange A := by
  ext
  simp [baseChange_eq_ltensor, tmul_neg]

Negation Commutes with Base Change of Linear Maps

Informal description

For any $R$-linear map $f$ and any $R$-algebra $A$, the base change of the negation of $f$ is equal to the negation of the base change of $f$, i.e., $(-f)_{\text{baseChange } A} = - (f_{\text{baseChange } A})$.

LinearMap.liftBaseChange_tmul theorem

(l : M →ₗ[R] N) (x y) : l.liftBaseChange A (x ⊗ₜ y) = x • l y

Full source

@[simp]
lemma liftBaseChange_tmul (l : M →ₗ[R] N) (x y) : l.liftBaseChange A (x ⊗ₜ y) = x • l y := rfl

Base Change Lift Formula: $l_{\text{lift}}(x \otimes y) = x \cdot l(y)$

Informal description

For any $R$-linear map $l \colon M \to N$, any elements $x \in A$ and $y \in M$, the base change lift of $l$ evaluated at the tensor product $x \otimes y$ equals the scalar multiplication of $x$ with $l(y)$, i.e., $l_{\text{liftBaseChange } A}(x \otimes y) = x \cdot l(y)$.

LinearMap.liftBaseChange_one_tmul theorem

(l : M →ₗ[R] N) (y) : l.liftBaseChange A (1 ⊗ₜ y) = l y

Full source

lemma liftBaseChange_one_tmul (l : M →ₗ[R] N) (y) : l.liftBaseChange A (1 ⊗ₜ y) = l y := by simp

Base Change Lift Identity: $l_{\text{lift}}(1 \otimes y) = l(y)$

Informal description

For any $R$-linear map $l \colon M \to N$ and any element $y \in M$, the base change lift of $l$ evaluated at $1 \otimes y$ equals $l(y)$, i.e., $l_{\text{liftBaseChange } A}(1 \otimes y) = l(y)$.

LinearMap.liftBaseChangeEquiv_symm_apply theorem

(l : A ⊗[R] M →ₗ[A] N) (x) : (liftBaseChangeEquiv A).symm l x = l (1 ⊗ₜ x)

Full source

@[simp]
lemma liftBaseChangeEquiv_symm_apply (l : A ⊗[R] MA ⊗[R] M →ₗ[A] N) (x) :
    (liftBaseChangeEquiv A).symm l x = l (1 ⊗ₜ x) := rfl

Inverse Base Change Equivalence Formula: $(liftBaseChangeEquiv\, A)^{-1}(l)(x) = l(1 \otimes x)$

Informal description

For any $R$-linear map $l \colon A \otimes_R M \to N$ of $A$-modules and any element $x \in M$, the inverse of the base change equivalence evaluated at $l$ and $x$ satisfies $(liftBaseChangeEquiv\, A)^{-1}(l)(x) = l(1 \otimes x)$.

LinearMap.liftBaseChange_comp theorem

 {P} [AddCommMonoid P] [Module A P] [Module R P] [IsScalarTower R A P] (l : M →ₗ[R] N) (l' : N →ₗ[A] P) :
  l' ∘ₗ l.liftBaseChange A = (l'.restrictScalars R ∘ₗ l).liftBaseChange A

Full source

lemma liftBaseChange_comp {P} [AddCommMonoid P] [Module A P] [Module R P] [IsScalarTower R A P]
    (l : M →ₗ[R] N) (l' : N →ₗ[A] P) :
      l' ∘ₗ l.liftBaseChange A = (l'.restrictScalars R ∘ₗ l).liftBaseChange A := by
  ext
  simp

Composition of Base Change Lifts: $l' \circ l_{\text{lift}} = (l'|_R \circ l)_{\text{lift}}$

Informal description

Let $R$ be a commutative (semi)ring, and let $A$ be an $R$-algebra. Let $M$, $N$, and $P$ be $R$-modules, with $P$ also an $A$-module such that the scalar multiplication is compatible via $R \to A$. For any $R$-linear map $l \colon M \to N$ and any $A$-linear map $l' \colon N \to P$, the composition $l' \circ l_{\text{liftBaseChange } A}$ equals the base change lift of the composition $(l'_{\text{restrictScalars } R}) \circ l$, i.e., $$ l' \circ l_{\text{liftBaseChange } A} = (l'_{\text{restrictScalars } R} \circ l)_{\text{liftBaseChange } A}. $$

LinearMap.range_liftBaseChange theorem

(l : M →ₗ[R] N) : LinearMap.range (l.liftBaseChange A) = Submodule.span A (LinearMap.range l)

Full source

@[simp]
lemma range_liftBaseChange (l : M →ₗ[R] N) :
    LinearMap.range (l.liftBaseChange A) = Submodule.span A (LinearMap.range l) := by
  apply le_antisymm
  · rintro _ ⟨x, rfl⟩
    induction x using TensorProduct.induction_on
    · simp
    · rw [LinearMap.liftBaseChange_tmul]
      exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨_, rfl⟩)
    · rw [map_add]
      exact add_mem ‹_› ‹_›
  · rw [Submodule.span_le]
    rintro _ ⟨x, rfl⟩
    exact ⟨1 ⊗ₜ x, by simp⟩

Range of Base Change Lift Equals Span of Original Range

Informal description

For any $R$-linear map $l \colon M \to N$, the range of the base change lift $l_{\text{liftBaseChange } A} \colon A \otimes_R M \to A \otimes_R N$ is equal to the $A$-submodule spanned by the range of $l$, i.e., $$\text{range}(l_{\text{liftBaseChange } A}) = \text{span}_A(\text{range}(l)).$$

Algebra.TensorProduct.one_def theorem

: (1 : A ⊗[R] B) = (1 : A) ⊗ₜ (1 : B)

Full source

theorem one_def : (1 : A ⊗[R] B) = (1 : A) ⊗ₜ (1 : B) :=
  rfl

Tensor Product of Algebra Units: $1_{A \otimes_R B} = 1_A \otimes 1_B$

Informal description

The multiplicative identity in the tensor product $A \otimes_R B$ of two $R$-algebras $A$ and $B$ is given by the tensor product of the multiplicative identities in $A$ and $B$, i.e., $$ 1_{A \otimes_R B} = 1_A \otimes 1_B. $$

Algebra.TensorProduct.natCast_def theorem

(n : ℕ) : (n : A ⊗[R] B) = (n : A) ⊗ₜ (1 : B)

Full source

theorem natCast_def (n : ℕ) : (n : A ⊗[R] B) = (n : A) ⊗ₜ (1 : B) := rfl

Natural Number Cast in Tensor Product Algebra: $n_{A \otimes_R B} = n_A \otimes 1_B$

Informal description

For any natural number $n$ and $R$-algebras $A$ and $B$, the natural number $n$ interpreted in the tensor product algebra $A \otimes_R B$ is equal to the tensor product of $n$ interpreted in $A$ with the multiplicative identity $1$ of $B$, i.e., $$ n_{A \otimes_R B} = n_A \otimes 1_B. $$

Algebra.TensorProduct.natCast_def' theorem

(n : ℕ) : (n : A ⊗[R] B) = (1 : A) ⊗ₜ (n : B)

Full source

theorem natCast_def' (n : ℕ) : (n : A ⊗[R] B) = (1 : A) ⊗ₜ (n : B) := by
  rw [natCast_def, ← nsmul_one, smul_tmul, nsmul_one]

Alternative Natural Number Cast in Tensor Product Algebra: $n_{A \otimes_R B} = 1_A \otimes n_B$

Informal description

For any natural number $n$ and $R$-algebras $A$ and $B$, the natural number $n$ interpreted in the tensor product algebra $A \otimes_R B$ is equal to the tensor product of the multiplicative identity $1$ of $A$ with $n$ interpreted in $B$, i.e., $$ n_{A \otimes_R B} = 1_A \otimes n_B. $$

Algebra.TensorProduct.mul_apply theorem

 (a₁ a₂ : A) (b₁ b₂ : B) : mul (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂) = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)

Full source

@[simp]
theorem mul_apply (a₁ a₂ : A) (b₁ b₂ : B) :
    mul (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂) = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) :=
  rfl

Multiplication Rule in Tensor Product Algebra: $(a_1 \otimes b_1)(a_2 \otimes b_2) = (a_1a_2) \otimes (b_1b_2)$

Informal description

For any elements $a_1, a_2$ of an $R$-algebra $A$ and any elements $b_1, b_2$ of an $R$-algebra $B$, the multiplication operation in the tensor product algebra $A \otimes_R B$ satisfies: $$(a_1 \otimes b_1) \cdot (a_2 \otimes b_2) = (a_1 \cdot a_2) \otimes (b_1 \cdot b_2)$$

Algebra.TensorProduct.tmul_mul_tmul theorem

(a₁ a₂ : A) (b₁ b₂ : B) : a₁ ⊗ₜ[R] b₁ * a₂ ⊗ₜ[R] b₂ = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)

Full source

@[simp]
theorem tmul_mul_tmul (a₁ a₂ : A) (b₁ b₂ : B) :
    a₁ ⊗ₜ[R] b₁ * a₂ ⊗ₜ[R] b₂ = (a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) :=
  rfl

Multiplication Rule in Tensor Product Algebra: $(a_1 \otimes b_1)(a_2 \otimes b_2) = (a_1a_2) \otimes (b_1b_2)$

Informal description

For any elements $a_1, a_2$ of an $R$-algebra $A$ and any elements $b_1, b_2$ of an $R$-algebra $B$, the multiplication in the tensor product algebra $A \otimes_R B$ satisfies: $$(a_1 \otimes b_1) \cdot (a_2 \otimes b_2) = (a_1 \cdot a_2) \otimes (b_1 \cdot b_2)$$

SemiconjBy.tmul theorem

 {a₁ a₂ a₃ : A} {b₁ b₂ b₃ : B} (ha : SemiconjBy a₁ a₂ a₃) (hb : SemiconjBy b₁ b₂ b₃) :
  SemiconjBy (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂) (a₃ ⊗ₜ[R] b₃)

Full source

theorem _root_.SemiconjBy.tmul {a₁ a₂ a₃ : A} {b₁ b₂ b₃ : B}
    (ha : SemiconjBy a₁ a₂ a₃) (hb : SemiconjBy b₁ b₂ b₃) :
    SemiconjBy (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂) (a₃ ⊗ₜ[R] b₃) :=
  congr_arg₂ (· ⊗ₜ[R] ·) ha.eq hb.eq

Tensor Product Preserves Semiconjugacy: $(a_1 \otimes b_1)(a_2 \otimes b_2) = (a_3 \otimes b_3)(a_1 \otimes b_1)$

Informal description

Let $A$ and $B$ be $R$-algebras. For any elements $a_1, a_2, a_3 \in A$ and $b_1, b_2, b_3 \in B$ such that $a_1$ semiconjugates $a_2$ to $a_3$ (i.e., $a_1 a_2 = a_3 a_1$) and $b_1$ semiconjugates $b_2$ to $b_3$ (i.e., $b_1 b_2 = b_3 b_1$), then the tensor product element $a_1 \otimes_R b_1$ semiconjugates $a_2 \otimes_R b_2$ to $a_3 \otimes_R b_3$ in the tensor product algebra $A \otimes_R B$.

Commute.tmul theorem

 {a₁ a₂ : A} {b₁ b₂ : B} (ha : Commute a₁ a₂) (hb : Commute b₁ b₂) : Commute (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂)

Full source

nonrec theorem _root_.Commute.tmul {a₁ a₂ : A} {b₁ b₂ : B}
    (ha : Commute a₁ a₂) (hb : Commute b₁ b₂) :
    Commute (a₁ ⊗ₜ[R] b₁) (a₂ ⊗ₜ[R] b₂) :=
  ha.tmul hb

Tensor Product Preserves Commutativity: $(a_1 \otimes b_1)(a_2 \otimes b_2) = (a_2 \otimes b_2)(a_1 \otimes b_1)$

Informal description

Let $A$ and $B$ be $R$-algebras. For any elements $a_1, a_2 \in A$ such that $a_1$ and $a_2$ commute (i.e., $a_1 a_2 = a_2 a_1$), and any elements $b_1, b_2 \in B$ such that $b_1$ and $b_2$ commute (i.e., $b_1 b_2 = b_2 b_1$), then the tensor product elements $a_1 \otimes_R b_1$ and $a_2 \otimes_R b_2$ commute in the tensor product algebra $A \otimes_R B$.

Algebra.TensorProduct.one_mul theorem

(x : A ⊗[R] B) : mul (1 ⊗ₜ 1) x = x

Full source

protected theorem one_mul (x : A ⊗[R] B) : mul (1 ⊗ₜ 1) x = x := by
  refine TensorProduct.induction_on x ?_ ?_ ?_ <;> simp +contextual

Left Identity Property in Tensor Product Algebra: $(1 \otimes_R 1) \cdot x = x$

Informal description

Let $A$ and $B$ be $R$-algebras. For any element $x$ in the tensor product algebra $A \otimes_R B$, the multiplication by the tensor product of the multiplicative identities $1 \otimes_R 1$ satisfies the left identity property: $(1 \otimes_R 1) \cdot x = x$.

Algebra.TensorProduct.mul_one theorem

(x : A ⊗[R] B) : mul x (1 ⊗ₜ 1) = x

Full source

protected theorem mul_one (x : A ⊗[R] B) : mul x (1 ⊗ₜ 1) = x := by
  refine TensorProduct.induction_on x ?_ ?_ ?_ <;> simp +contextual

Right Multiplicative Identity in Tensor Product Algebra: $x \cdot (1 \otimes 1) = x$

Informal description

For any element $x$ in the tensor product algebra $A \otimes_R B$ of two $R$-algebras $A$ and $B$, the multiplication of $x$ by the tensor product of the multiplicative identities $1 \otimes_R 1$ equals $x$, i.e., $x \cdot (1 \otimes_R 1) = x$.

Algebra.TensorProduct.mul_assoc theorem

(x y z : A ⊗[R] B) : mul (mul x y) z = mul x (mul y z)

Full source

protected theorem mul_assoc (x y z : A ⊗[R] B) : mul (mul x y) z = mul x (mul y z) := by
  -- restate as an equality of morphisms so that we can use `ext`
  suffices LinearMap.llcompLinearMap.llcomp R _ _ _ mul ∘ₗ mul =
      (LinearMap.llcomp R _ _ _ LinearMap.lflip <| LinearMap.llcompLinearMap.llcomp R _ _ _ mul.flip ∘ₗ mul).flip by
    exact DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this x) y) z
  ext xa xb ya yb za zb
  exact congr_arg₂ (· ⊗ₜ ·) (mul_assoc xa ya za) (mul_assoc xb yb zb)

Associativity of Multiplication in Tensor Product Algebra: $(x \cdot y) \cdot z = x \cdot (y \cdot z)$

Informal description

For any elements $x, y, z$ in the tensor product algebra $A \otimes_R B$ of two $R$-algebras $A$ and $B$, the multiplication operation satisfies the associativity property: $(x \cdot y) \cdot z = x \cdot (y \cdot z)$.

Algebra.TensorProduct.tmul_pow theorem

(a : A) (b : B) (k : ℕ) : a ⊗ₜ[R] b ^ k = (a ^ k) ⊗ₜ[R] (b ^ k)

Full source

@[simp]
theorem tmul_pow (a : A) (b : B) (k : ℕ) : a ⊗ₜ[R] b ^ k = (a ^ k) ⊗ₜ[R] (b ^ k) := by
  induction' k with k ih
  · simp [one_def]
  · simp [pow_succ, ih]

Power of Tensor Product: $(a \otimes_R b)^k = a^k \otimes_R b^k$

Informal description

For any elements $a$ in an $R$-algebra $A$ and $b$ in an $R$-algebra $B$, and for any natural number $k$, the $k$-th power of the tensor product $a \otimes_R b$ equals the tensor product of the $k$-th powers of $a$ and $b$, i.e., $(a \otimes_R b)^k = a^k \otimes_R b^k$.

Algebra.TensorProduct.algebraMap_apply theorem

[SMulCommClass R S A] (r : S) : algebraMap S (A ⊗[R] B) r = (algebraMap S A) r ⊗ₜ 1

Full source

@[simp]
theorem algebraMap_apply [SMulCommClass R S A] (r : S) :
    algebraMap S (A ⊗[R] B) r = (algebraMap S A) r ⊗ₜ 1 :=
  rfl

Algebra Map on Tensor Product: $\text{algebraMap}_S (A \otimes_R B)(r) = \text{algebraMap}_S A(r) \otimes_R 1_B$

Informal description

Let $R$ and $S$ be commutative (semi)rings, and let $A$ be an $R$-algebra that is also an $S$-algebra with compatible scalar multiplication (i.e., $R$ and $S$ act commutatively on $A$). For any element $r \in S$, the algebra map from $S$ to the tensor product algebra $A \otimes_R B$ satisfies: \[ \text{algebraMap}_S (A \otimes_R B)(r) = \text{algebraMap}_S A(r) \otimes_R 1_B \] where $1_B$ denotes the multiplicative identity in $B$.

Algebra.TensorProduct.algebraMap_apply' theorem

(r : R) : algebraMap R (A ⊗[R] B) r = 1 ⊗ₜ algebraMap R B r

Full source

theorem algebraMap_apply' (r : R) :
    algebraMap R (A ⊗[R] B) r = 1 ⊗ₜ algebraMap R B r := by
  rw [algebraMap_apply, Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_tmul]

Algebra Map on Tensor Product: $\text{algebraMap}_R (A \otimes_R B)(r) = 1_A \otimes_R \text{algebraMap}_R B(r)$

Informal description

For any element $r$ in a commutative (semi)ring $R$, the algebra map from $R$ to the tensor product algebra $A \otimes_R B$ satisfies: \[ \text{algebraMap}_R (A \otimes_R B)(r) = 1_A \otimes_R \text{algebraMap}_R B(r) \] where $1_A$ denotes the multiplicative identity in $A$.

Algebra.TensorProduct.includeLeft_apply theorem

[SMulCommClass R S A] (a : A) : (includeLeft : A →ₐ[S] A ⊗[R] B) a = a ⊗ₜ 1

Full source

@[simp]
theorem includeLeft_apply [SMulCommClass R S A] (a : A) :
    (includeLeft : A →ₐ[S] A ⊗[R] B) a = a ⊗ₜ 1 :=
  rfl

Left inclusion map in tensor product algebra: $\text{includeLeft}(a) = a \otimes_R 1_B$

Informal description

Let $R$ and $S$ be commutative (semi)rings, and let $A$ be an $R$-algebra that is also an $S$-algebra with compatible scalar multiplication (i.e., $R$ and $S$ act commutatively on $A$). For any element $a \in A$, the left inclusion map $\text{includeLeft} : A \to A \otimes_R B$ of $S$-algebras satisfies: \[ \text{includeLeft}(a) = a \otimes_R 1_B \] where $1_B$ denotes the multiplicative identity in $B$.

Algebra.TensorProduct.includeRight_apply theorem

(b : B) : (includeRight : B →ₐ[R] A ⊗[R] B) b = 1 ⊗ₜ b

Full source

@[simp]
theorem includeRight_apply (b : B) : (includeRight : B →ₐ[R] A ⊗[R] B) b = 1 ⊗ₜ b :=
  rfl

Right inclusion map in tensor product algebra: $\text{includeRight}(b) = 1_A \otimes_R b$

Informal description

For any element $b$ in an $R$-algebra $B$, the right inclusion map $\text{includeRight} : B \to A \otimes_R B$ of $R$-algebras satisfies: \[ \text{includeRight}(b) = 1_A \otimes_R b \] where $1_A$ denotes the multiplicative identity in $A$.

Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap theorem

: (includeLeftRingHom.comp (algebraMap R A) : R →+* A ⊗[R] B) = includeRight.toRingHom.comp (algebraMap R B)

Full source

theorem includeLeftRingHom_comp_algebraMap :
    (includeLeftRingHom.comp (algebraMap R A) : R →+* A ⊗[R] B) =
      includeRight.toRingHom.comp (algebraMap R B) := by
  ext
  simp

Equality of Composed Algebra Maps in Tensor Product Algebra

Informal description

Let $R$ be a commutative (semi)ring, and let $A$ and $B$ be $R$-algebras. The composition of the ring homomorphism $\text{includeLeftRingHom} \circ \text{algebraMap}_R^A$ from $R$ to $A \otimes_R B$ is equal to the composition $\text{includeRight.toRingHom} \circ \text{algebraMap}_R^B$, where: - $\text{algebraMap}_R^A : R \to A$ and $\text{algebraMap}_R^B : R \to B$ are the canonical $R$-algebra structure maps, - $\text{includeLeftRingHom} : A \to A \otimes_R B$ is the left inclusion ring homomorphism, - $\text{includeRight.toRingHom} : B \to A \otimes_R B$ is the right inclusion ring homomorphism.

Algebra.TensorProduct.ext theorem

 ⦃f g : (A ⊗[R] B) →ₐ[S] C⦄ (ha : f.comp includeLeft = g.comp includeLeft)
  (hb : (f.restrictScalars R).comp includeRight = (g.restrictScalars R).comp includeRight) : f = g

Full source

/-- A version of `TensorProduct.ext` for `AlgHom`.

Using this as the `@[ext]` lemma instead of `Algebra.TensorProduct.ext'` allows `ext` to apply
lemmas specific to `A →ₐ[S] _` and `B →ₐ[R] _`; notably this allows recursion into nested tensor
products of algebras.

See note [partially-applied ext lemmas]. -/
@[ext high]
theorem ext ⦃f g : (A ⊗[R] B) →ₐ[S] C⦄
    (ha : f.comp includeLeft = g.comp includeLeft)
    (hb : (f.restrictScalars R).comp includeRight = (g.restrictScalars R).comp includeRight) :
    f = g := by
  apply AlgHom.toLinearMap_injective
  ext a b
  have := congr_arg₂ HMul.hMul (AlgHom.congr_fun ha a) (AlgHom.congr_fun hb b)
  dsimp at *
  rwa [← map_mul, ← map_mul, tmul_mul_tmul, one_mul, mul_one] at this

Extensionality of Algebra Homomorphisms on Tensor Products

Informal description

Let $A$ and $B$ be $R$-algebras, and let $C$ be an $S$-algebra. For two algebra homomorphisms $f, g \colon A \otimes_R B \to C$, if $f$ and $g$ agree on the image of $A$ (i.e., $f \circ \text{includeLeft} = g \circ \text{includeLeft}$) and on the image of $B$ (i.e., $(f|_R) \circ \text{includeRight} = (g|_R) \circ \text{includeRight}$), then $f = g$.

Algebra.TensorProduct.ext' theorem

{g h : A ⊗[R] B →ₐ[S] C} (H : ∀ a b, g (a ⊗ₜ b) = h (a ⊗ₜ b)) : g = h

Full source

theorem ext' {g h : A ⊗[R] BA ⊗[R] B →ₐ[S] C} (H : ∀ a b, g (a ⊗ₜ b) = h (a ⊗ₜ b)) : g = h :=
  ext (AlgHom.ext fun _ => H _ _) (AlgHom.ext fun _ => H _ _)

Extensionality of Algebra Homomorphisms via Tensor Elements

Informal description

Let $A$ and $B$ be $R$-algebras, and let $C$ be an $S$-algebra. For two algebra homomorphisms $g, h \colon A \otimes_R B \to C$, if $g(a \otimes b) = h(a \otimes b)$ for all $a \in A$ and $b \in B$, then $g = h$.

Algebra.TensorProduct.intCast_def theorem

(z : ℤ) : (z : A ⊗[R] B) = (z : A) ⊗ₜ (1 : B)

Full source

theorem intCast_def (z : ℤ) : (z : A ⊗[R] B) = (z : A) ⊗ₜ (1 : B) := rfl

Integer Cast in Tensor Product Algebra: $z = z \otimes_R 1$

Informal description

For any integer $z$ and $R$-algebras $A$ and $B$, the integer $z$ in the tensor product algebra $A \otimes_R B$ is equal to the tensor product of $z$ in $A$ with the multiplicative identity $1$ in $B$, i.e., $z = z \otimes_R 1$.

Algebra.TensorProduct.intCast_def' theorem

(z : ℤ) : (z : A ⊗[R] B) = (1 : A) ⊗ₜ (z : B)

Full source

theorem intCast_def' (z : ℤ) : (z : A ⊗[R] B) = (1 : A) ⊗ₜ (z : B) := by
  rw [intCast_def, ← zsmul_one, smul_tmul, zsmul_one]

Integer Cast in Tensor Product Algebra: $z = 1 \otimes_R z$

Informal description

For any integer $z$ and $R$-algebras $A$ and $B$, the integer $z$ in the tensor product algebra $A \otimes_R B$ is equal to the tensor product of the multiplicative identity $1$ in $A$ with $z$ in $B$, i.e., $z = 1 \otimes_R z$.

LinearMap.map_mul_of_map_mul_tmul theorem

 {f : A ⊗[R] B →ₗ[S] C} (hf : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ (b₁ * b₂)) = f (a₁ ⊗ₜ b₁) * f (a₂ ⊗ₜ b₂))
  (x y : A ⊗[R] B) : f (x * y) = f x * f y

Full source

/-- To check a linear map preserves multiplication, it suffices to check it on pure tensors. See
`algHomOfLinearMapTensorProduct` for a bundled version. -/
lemma _root_.LinearMap.map_mul_of_map_mul_tmul {f : A ⊗[R] BA ⊗[R] B →ₗ[S] C}
    (hf : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ (b₁ * b₂)) = f (a₁ ⊗ₜ b₁) * f (a₂ ⊗ₜ b₂))
    (x y : A ⊗[R] B) : f (x * y) = f x * f y :=
  f.map_mul_iff.2 (by
    -- these instances are needed by the statement of `ext`, but not by the current definition.
    letI : Algebra R C := RestrictScalars.algebra R S C
    letI : IsScalarTower R S C := RestrictScalars.isScalarTower R S C
    ext
    dsimp
    exact hf _ _ _ _) x y

Preservation of Multiplication in Tensor Product Algebras via Pure Tensors

Informal description

Let $A$ and $B$ be $R$-algebras, and let $C$ be an $S$-algebra. Given an $S$-linear map $f \colon A \otimes_R B \to C$ such that for all $a_1, a_2 \in A$ and $b_1, b_2 \in B$, \[ f((a_1a_2) \otimes (b_1b_2)) = f(a_1 \otimes b_1) \cdot f(a_2 \otimes b_2), \] then $f$ preserves multiplication, i.e., for all $x, y \in A \otimes_R B$, \[ f(xy) = f(x)f(y). \]

Algebra.TensorProduct.algHomOfLinearMapTensorProduct_apply theorem

(f h_mul h_one x) : (algHomOfLinearMapTensorProduct f h_mul h_one : A ⊗[R] B →ₐ[S] C) x = f x

Full source

@[simp]
theorem algHomOfLinearMapTensorProduct_apply (f h_mul h_one x) :
    (algHomOfLinearMapTensorProduct f h_mul h_one : A ⊗[R] BA ⊗[R] B →ₐ[S] C) x = f x :=
  rfl

Evaluation of Algebra Homomorphism Constructed from Tensor Product Linear Map

Informal description

Let $A$ and $B$ be $R$-algebras, $C$ be an $S$-algebra, and $f \colon A \otimes_R B \to C$ be an $S$-linear map that preserves multiplication and unit (as specified by `h_mul` and `h_one`). Then for any $x \in A \otimes_R B$, the algebra homomorphism $\text{algHomOfLinearMapTensorProduct}\,f\,h_{mul}\,h_{one}$ evaluated at $x$ equals $f(x)$.

Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct_apply theorem

(f h_mul h_one x) : (algEquivOfLinearEquivTensorProduct f h_mul h_one : A ⊗[R] B ≃ₐ[S] C) x = f x

Full source

@[simp]
theorem algEquivOfLinearEquivTensorProduct_apply (f h_mul h_one x) :
    (algEquivOfLinearEquivTensorProduct f h_mul h_one : A ⊗[R] BA ⊗[R] B ≃ₐ[S] C) x = f x :=
  rfl

Evaluation of Tensor Product Algebra Equivalence via Linear Equivalence

Informal description

Let $R$ be a commutative (semi)ring, $A$ and $B$ be $R$-algebras, and $C$ be an $S$-algebra. Given an $S$-linear equivalence $f : A \otimes_R B \to C$ that preserves multiplication (i.e., $f(x \otimes y) = f(x) \cdot f(y)$ for all $x, y \in A \otimes_R B$) and maps the multiplicative identity to the identity, then the algebra equivalence $\text{algEquivOfLinearEquivTensorProduct}\,f$ satisfies \[ (\text{algEquivOfLinearEquivTensorProduct}\,f)\,x = f(x) \] for all $x \in A \otimes_R B$.

Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct_apply theorem

 (f h_mul h_one x) : (algEquivOfLinearEquivTripleTensorProduct f h_mul h_one : (A ⊗[R] B) ⊗[R] C ≃ₐ[R] D) x = f x

Full source

@[simp]
theorem algEquivOfLinearEquivTripleTensorProduct_apply (f h_mul h_one x) :
    (algEquivOfLinearEquivTripleTensorProduct f h_mul h_one : (A ⊗[R] B) ⊗[R] C(A ⊗[R] B) ⊗[R] C ≃ₐ[R] D) x = f x :=
  rfl

Application of Triple Tensor Product Algebra Equivalence via Linear Equivalence

Informal description

Let $R$ be a commutative (semi)ring and let $A$, $B$, $C$, $D$ be $R$-algebras. Given an $R$-linear equivalence $f : (A \otimes_R B) \otimes_R C \to D$ that preserves multiplication (i.e., $f(x \otimes y) = f(x) \cdot f(y)$ for all $x, y$) and maps the multiplicative identity to the identity, then the algebra equivalence $\text{algEquivOfLinearEquivTripleTensorProduct}\, f$ satisfies $(\text{algEquivOfLinearEquivTripleTensorProduct}\, f)\, x = f x$ for all $x \in (A \otimes_R B) \otimes_R C$.

Algebra.TensorProduct.lift_tmul theorem

 (f : A →ₐ[S] C) (g : B →ₐ[R] C) (hfg : ∀ x y, Commute (f x) (g y)) (a : A) (b : B) : lift f g hfg (a ⊗ₜ b) = f a * g b

Full source

@[simp]
theorem lift_tmul (f : A →ₐ[S] C) (g : B →ₐ[R] C) (hfg : ∀ x y, Commute (f x) (g y))
    (a : A) (b : B) :
    lift f g hfg (a ⊗ₜ b) = f a * g b :=
  rfl

Tensor Product Lift Evaluation on Pure Tensors

Informal description

Let $R$ be a commutative (semi)ring, $S$ be a commutative ring, and let $A$, $B$, $C$ be $R$-algebras with $A$ also an $S$-algebra. Given $S$-algebra homomorphism $f: A \to C$ and $R$-algebra homomorphism $g: B \to C$ such that $f(x)$ and $g(y)$ commute for all $x \in A$ and $y \in B$, then for any $a \in A$ and $b \in B$, the lift of $f$ and $g$ satisfies $\text{lift}(f, g)(a \otimes b) = f(a) \cdot g(b)$.

Algebra.TensorProduct.lift_includeLeft_includeRight theorem

: lift includeLeft includeRight (fun _ _ => (Commute.one_right _).tmul (Commute.one_left _)) = .id S (A ⊗[R] B)

Full source

@[simp]
theorem lift_includeLeft_includeRight :
    lift includeLeft includeRight (fun _ _ => (Commute.one_right _).tmul (Commute.one_left _)) =
      .id S (A ⊗[R] B) := by
  ext <;> simp

Identity Property of Tensor Product Algebra via Inclusion Lifts

Informal description

Let $R$ be a commutative (semi)ring and $S$ an algebra over $R$. For the tensor product algebra $A \otimes_R B$ where $A$ is an $S$-algebra and $B$ is an $R$-algebra, the lift of the inclusion maps $\text{includeLeft}: A \to A \otimes_R B$ and $\text{includeRight}: B \to A \otimes_R B$ (with the commutativity condition given by the tensor product of commuting identity elements) equals the identity algebra homomorphism on $A \otimes_R B$ as an $S$-algebra.

Algebra.TensorProduct.lift_comp_includeLeft theorem

(f : A →ₐ[S] C) (g : B →ₐ[R] C) (hfg : ∀ x y, Commute (f x) (g y)) : (lift f g hfg).comp includeLeft = f

Full source

@[simp]
theorem lift_comp_includeLeft (f : A →ₐ[S] C) (g : B →ₐ[R] C) (hfg : ∀ x y, Commute (f x) (g y)) :
    (lift f g hfg).comp includeLeft = f :=
  AlgHom.ext <| by simp

Compatibility of Lift with Left Inclusion in Tensor Product of Algebras

Informal description

Let $A$ and $B$ be $R$-algebras, and let $C$ be an $S$-algebra. Given algebra homomorphisms $f: A \to C$ and $g: B \to C$ such that $f(x)$ and $g(y)$ commute for all $x \in A$ and $y \in B$, the composition of the lifted homomorphism $\text{lift}(f,g,hfg): A \otimes_R B \to C$ with the inclusion $\text{includeLeft}: A \to A \otimes_R B$ equals $f$.

Algebra.TensorProduct.lift_comp_includeRight theorem

 (f : A →ₐ[S] C) (g : B →ₐ[R] C) (hfg : ∀ x y, Commute (f x) (g y)) :
  ((lift f g hfg).restrictScalars R).comp includeRight = g

Full source

@[simp]
theorem lift_comp_includeRight (f : A →ₐ[S] C) (g : B →ₐ[R] C) (hfg : ∀ x y, Commute (f x) (g y)) :
    ((lift f g hfg).restrictScalars R).comp includeRight = g :=
  AlgHom.ext <| by simp

Compatibility of Tensor Product Lift with Right Inclusion for Algebra Homomorphisms

Informal description

Let $A$ be an $S$-algebra and $B$ be an $R$-algebra, where $R$ is a commutative (semi)ring. Given $S$-algebra homomorphism $f: A \to C$ and $R$-algebra homomorphism $g: B \to C$ such that $f(x)$ and $g(y)$ commute for all $x \in A$ and $y \in B$, then the composition of the restricted scalar map of the tensor product lift $(lift\ f\ g\ hfg)$ with the inclusion map $includeRight$ equals $g$. In mathematical notation: $$(lift\ f\ g\ hfg)|_R \circ includeRight = g$$

Algebra.TensorProduct.lid_toLinearEquiv theorem

: (TensorProduct.lid R A).toLinearEquiv = _root_.TensorProduct.lid R A

Full source

@[simp] theorem lid_toLinearEquiv :
    (TensorProduct.lid R A).toLinearEquiv = _root_.TensorProduct.lid R A := rfl

Equality of Linear Equivalences in Left Identity Tensor Product Isomorphism

Informal description

The underlying linear equivalence of the algebra isomorphism $\text{lid} : R \otimes_R A \simeq A$ is equal to the canonical linear equivalence $\text{lid} : R \otimes_R A \simeq A$.

Algebra.TensorProduct.lid_tmul theorem

(r : R) (a : A) : TensorProduct.lid R A (r ⊗ₜ a) = r • a

Full source

@[simp]
theorem lid_tmul (r : R) (a : A) : TensorProduct.lid R A (r ⊗ₜ a) = r • a := rfl

Left Unit Isomorphism Maps Tensor Product to Scalar Multiplication

Informal description

For any element $r$ in a commutative ring $R$ and any element $a$ in an $R$-algebra $A$, the left unit isomorphism $\text{lid}_R A$ maps the tensor product $r \otimes a$ to the scalar multiplication $r \cdot a$.

Algebra.TensorProduct.lid_symm_apply theorem

(a : A) : (TensorProduct.lid R A).symm a = 1 ⊗ₜ a

Full source

@[simp]
theorem lid_symm_apply (a : A) : (TensorProduct.lid R A).symm a = 1 ⊗ₜ a := rfl

Inverse of Left Identity Isomorphism for Tensor Product of Algebras

Informal description

For any element $a$ in an $R$-algebra $A$, the inverse of the left identity isomorphism $\text{lid}_{R,A}$ maps $a$ to the tensor product $1 \otimes_R a$ in $R \otimes_R A$.

Algebra.TensorProduct.rid_toLinearEquiv theorem

: (TensorProduct.rid R S A).toLinearEquiv = AlgebraTensorModule.rid R S A

Full source

@[simp] theorem rid_toLinearEquiv :
    (TensorProduct.rid R S A).toLinearEquiv = AlgebraTensorModule.rid R S A := rfl

Equality of Underlying Linear Equivalences in Right Identity Tensor Product Isomorphism

Informal description

The underlying linear equivalence of the algebra isomorphism `TensorProduct.rid R S A` is equal to the linear equivalence `AlgebraTensorModule.rid R S A`, where: - $R$ is a commutative (semi)ring - $S$ is another commutative (semi)ring - $A$ is an $R$-algebra that is also an $S$-algebra - `TensorProduct.rid R S A` is the right identity isomorphism $A ⊗_R S ≃ₐ[S] A$ - `AlgebraTensorModule.rid R S A` is the corresponding linear equivalence

Algebra.TensorProduct.rid_tmul theorem

(r : R) (a : A) : TensorProduct.rid R S A (a ⊗ₜ r) = r • a

Full source

@[simp]
theorem rid_tmul (r : R) (a : A) : TensorProduct.rid R S A (a ⊗ₜ r) = r • a := rfl

Right Identity Isomorphism Maps Tensor Product to Scalar Multiplication

Informal description

For any element $r$ in a commutative (semi)ring $R$ and any element $a$ in an $R$-algebra $A$, the right identity isomorphism $\text{rid}_{R,S,A}$ maps the tensor product $a \otimes_R r$ to the scalar multiplication $r \cdot a$ in $A$.

Algebra.TensorProduct.rid_symm_apply theorem

(a : A) : (TensorProduct.rid R S A).symm a = a ⊗ₜ 1

Full source

@[simp]
theorem rid_symm_apply (a : A) : (TensorProduct.rid R S A).symm a = a ⊗ₜ 1 := rfl

Inverse of Right Identity Isomorphism for Tensor Product of Algebras

Informal description

For any element $a$ in an $R$-algebra $A$, the inverse of the right identity isomorphism $\text{rid}_{R,S,A}$ maps $a$ to the tensor product $a \otimes_R 1$, where $1$ is the multiplicative identity in $S$.

Algebra.TensorProduct.mapOfCompatibleSMul_tmul theorem

(m n) : mapOfCompatibleSMul R S A B (m ⊗ₜ n) = m ⊗ₜ n

Full source

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

Tensor Product Preservation under `mapOfCompatibleSMul`

Informal description

For any elements $m$ in an $R$-module $A$ and $n$ in an $R$-module $B$, the map `mapOfCompatibleSMul` applied to the tensor product $m \otimes_R n$ equals $m \otimes_R n$ itself.

Algebra.TensorProduct.mapOfCompatibleSMul_surjective theorem

: Function.Surjective (mapOfCompatibleSMul R S A B)

Full source

theorem mapOfCompatibleSMul_surjective : Function.Surjective (mapOfCompatibleSMul R S A B) :=
  _root_.TensorProduct.mapOfCompatibleSMul_surjective R S A B

Surjectivity of the Compatible Scalar Multiplication Map on Tensor Product of Algebras

Informal description

The linear map `mapOfCompatibleSMul R S A B` from the tensor product of `R`-algebras `A` and `B` is surjective.

Algebra.TensorProduct.lidOfCompatibleSMul_tmul theorem

(s a) : lidOfCompatibleSMul R S A (s ⊗ₜ[R] a) = s • a

Full source

theorem lidOfCompatibleSMul_tmul (s a) : lidOfCompatibleSMul R S A (s ⊗ₜ[R] a) = s • a := rfl

Left Unit Isomorphism for Tensor Product: $\text{lidOfCompatibleSMul}(s \otimes_R a) = s \cdot a$

Informal description

For any element $s$ in an $S$-module and $a$ in an $R$-algebra $A$, the left unit isomorphism $\text{lidOfCompatibleSMul}_{R,S,A}$ maps the tensor product $s \otimes_R a$ to the scalar multiplication $s \cdot a$, i.e., $\text{lidOfCompatibleSMul}_{R,S,A}(s \otimes_R a) = s \cdot a$.

Algebra.TensorProduct.comm_toLinearEquiv theorem

: (Algebra.TensorProduct.comm R A B).toLinearEquiv = _root_.TensorProduct.comm R A B

Full source

@[simp] theorem comm_toLinearEquiv :
    (Algebra.TensorProduct.comm R A B).toLinearEquiv = _root_.TensorProduct.comm R A B := rfl

Equality of Commutativity Isomorphism's Linear Equivalence with Tensor Product Commutativity Map

Informal description

The underlying linear equivalence of the algebra isomorphism `Algebra.TensorProduct.comm R A B` is equal to the tensor product commutativity linear equivalence `TensorProduct.comm R A B`. In other words, the linear equivalence component of the commutative algebra isomorphism between $A \otimes_R B$ and $B \otimes_R A$ coincides with the standard tensor product commutativity map.

Algebra.TensorProduct.comm_tmul theorem

(a : A) (b : B) : TensorProduct.comm R A B (a ⊗ₜ b) = b ⊗ₜ a

Full source

@[simp]
theorem comm_tmul (a : A) (b : B) :
    TensorProduct.comm R A B (a ⊗ₜ b) = b ⊗ₜ a :=
  rfl

Commutativity Isomorphism for Tensor Product of Algebras

Informal description

For any elements $a$ in an $R$-algebra $A$ and $b$ in an $R$-algebra $B$, the commutativity isomorphism $\text{comm}_{R,A,B}$ maps the tensor product $a \otimes b$ to $b \otimes a$, i.e., $\text{comm}_{R,A,B}(a \otimes b) = b \otimes a$.

Algebra.TensorProduct.comm_symm_tmul theorem

(a : A) (b : B) : (TensorProduct.comm R A B).symm (b ⊗ₜ a) = a ⊗ₜ b

Full source

@[simp]
theorem comm_symm_tmul (a : A) (b : B) :
    (TensorProduct.comm R A B).symm (b ⊗ₜ a) = a ⊗ₜ b :=
  rfl

Inverse of Tensor Product Commutativity Map Swaps Elements

Informal description

For any elements $a \in A$ and $b \in B$, the inverse of the commutativity isomorphism applied to the tensor product $b \otimes a$ equals $a \otimes b$, i.e., $\text{comm}_{R}(A,B)^{-1}(b \otimes a) = a \otimes b$.

Algebra.TensorProduct.comm_symm theorem

: (TensorProduct.comm R A B).symm = TensorProduct.comm R B A

Full source

theorem comm_symm :
    (TensorProduct.comm R A B).symm = TensorProduct.comm R B A := by
  ext; rfl

Symmetry of Tensor Product of Algebras: $(A \otimes_R B)^{\text{symm}} \cong B \otimes_R A$

Informal description

The symmetry isomorphism for the tensor product of $R$-algebras satisfies $(A \otimes_R B)^{\text{symm}} = B \otimes_R A$, where $\text{symm}$ denotes the inverse of the canonical isomorphism $A \otimes_R B \cong B \otimes_R A$.

Algebra.TensorProduct.comm_comp_includeLeft theorem

: (TensorProduct.comm R A B : A ⊗[R] B →ₐ[R] B ⊗[R] A).comp includeLeft = includeRight

Full source

@[simp]
lemma comm_comp_includeLeft :
    (TensorProduct.comm R A B : A ⊗[R] BA ⊗[R] B →ₐ[R] B ⊗[R] A).comp includeLeft = includeRight := rfl

Commutativity of Tensor Product Preserves Left Inclusion

Informal description

Let $R$ be a commutative (semi)ring and $A$, $B$ be $R$-algebras. The composition of the tensor product commutativity isomorphism $\text{comm}_{R,A,B}: A \otimes_R B \to B \otimes_R A$ with the left inclusion map $\text{includeLeft}: A \to A \otimes_R B$ equals the right inclusion map $\text{includeRight}: B \to B \otimes_R A$. In other words, for any $a \in A$, we have $\text{comm}_{R,A,B}(\text{includeLeft}(a)) = \text{includeRight}(a)$.

Algebra.TensorProduct.comm_comp_includeRight theorem

: (TensorProduct.comm R A B : A ⊗[R] B →ₐ[R] B ⊗[R] A).comp includeRight = includeLeft

Full source

@[simp]
lemma comm_comp_includeRight :
    (TensorProduct.comm R A B : A ⊗[R] BA ⊗[R] B →ₐ[R] B ⊗[R] A).comp includeRight = includeLeft := rfl

Commutativity Isomorphism Interchanges Inclusion Maps in Tensor Product of Algebras

Informal description

Let $R$ be a commutative (semi)ring and $A$, $B$ be $R$-algebras. The composition of the commutativity isomorphism $\text{comm}_R : A \otimes_R B \to B \otimes_R A$ with the right inclusion map $\text{includeRight} : B \to A \otimes_R B$ equals the left inclusion map $\text{includeLeft} : A \to B \otimes_R A$. In other words, the following diagram commutes: \[ \text{comm}_R \circ \text{includeRight} = \text{includeLeft} \]

Algebra.TensorProduct.adjoin_tmul_eq_top theorem

: adjoin R {t : A ⊗[R] B | ∃ a b, a ⊗ₜ[R] b = t} = ⊤

Full source

theorem adjoin_tmul_eq_top : adjoin R { t : A ⊗[R] B | ∃ a b, a ⊗ₜ[R] b = t } = ⊤ :=
  top_le_iff.mp <| (top_le_iff.mpr <| span_tmul_eq_top R A B).trans (span_le_adjoin R _)

Tensor Product Algebra Generated by Pure Tensors

Informal description

Let $R$ be a commutative (semi)ring and $A$, $B$ be $R$-algebras. The subalgebra generated by all pure tensors $a \otimes_R b$ in the tensor product $A \otimes_R B$ is equal to the entire algebra, i.e., $\text{adjoin}_R \{ t \in A \otimes_R B \mid \exists a \in A, b \in B, a \otimes_R b = t \} = \top$.

Algebra.TensorProduct.assoc_aux_1 theorem

 (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C) :
  (TensorProduct.assoc R A B C) (((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) ⊗ₜ[R] (c₁ * c₂)) =
    (TensorProduct.assoc R A B C) ((a₁ ⊗ₜ[R] b₁) ⊗ₜ[R] c₁) * (TensorProduct.assoc R A B C) ((a₂ ⊗ₜ[R] b₂) ⊗ₜ[R] c₂)

Full source

theorem assoc_aux_1 (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C) :
    (TensorProduct.assoc R A B C) (((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) ⊗ₜ[R] (c₁ * c₂)) =
      (TensorProduct.assoc R A B C) ((a₁ ⊗ₜ[R] b₁) ⊗ₜ[R] c₁) *
        (TensorProduct.assoc R A B C) ((a₂ ⊗ₜ[R] b₂) ⊗ₜ[R] c₂) :=
  rfl

Associator Preserves Multiplication in Tensor Product of Algebras

Informal description

Let $R$ be a commutative (semi)ring and $A$, $B$, $C$ be $R$-algebras. For any elements $a₁, a₂ \in A$, $b₁, b₂ \in B$, and $c₁, c₂ \in C$, the associator isomorphism satisfies: \[ \text{assoc}_R \big( (a₁a₂ \otimes_R b₁b₂) \otimes_R c₁c₂ \big) = \text{assoc}_R (a₁ \otimes_R b₁ \otimes_R c₁) \cdot \text{assoc}_R (a₂ \otimes_R b₂ \otimes_R c₂) \] where $\text{assoc}_R$ denotes the associator isomorphism $(A \otimes_R B) \otimes_R C \cong A \otimes_R (B \otimes_R C)$.

Algebra.TensorProduct.assoc_aux_2 theorem

: (TensorProduct.assoc R A B C) ((1 ⊗ₜ[R] 1) ⊗ₜ[R] 1) = 1

Full source

theorem assoc_aux_2 : (TensorProduct.assoc R A B C) ((1 ⊗ₜ[R] 1) ⊗ₜ[R] 1) = 1 :=
  rfl

Associator Preserves Multiplicative Identity in Tensor Product of Algebras

Informal description

The associator isomorphism for tensor products of algebras maps the tensor product of multiplicative identities $(1 \otimes_{R} 1) \otimes_{R} 1$ to the multiplicative identity $1$ in the algebra $A \otimes_{R} (B \otimes_{R} C)$.

Algebra.TensorProduct.assoc_toLinearEquiv theorem

: (Algebra.TensorProduct.assoc R A B C).toLinearEquiv = _root_.TensorProduct.assoc R A B C

Full source

@[simp] theorem assoc_toLinearEquiv :
  (Algebra.TensorProduct.assoc R A B C).toLinearEquiv = _root_.TensorProduct.assoc R A B C := rfl

Associator Algebra Isomorphism as Linear Equivalence

Informal description

The underlying linear equivalence of the associator algebra isomorphism $\text{assoc}_R : (A \otimes_R B) \otimes_R C \cong A \otimes_R (B \otimes_R C)$ is equal to the standard tensor product associator linear equivalence.

Algebra.TensorProduct.assoc_tmul theorem

(a : A) (b : B) (c : C) : Algebra.TensorProduct.assoc R A B C ((a ⊗ₜ b) ⊗ₜ c) = a ⊗ₜ (b ⊗ₜ c)

Full source

@[simp]
theorem assoc_tmul (a : A) (b : B) (c : C) :
    Algebra.TensorProduct.assoc R A B C ((a ⊗ₜ b) ⊗ₜ c) = a ⊗ₜ (b ⊗ₜ c) :=
  rfl

Associator Isomorphism for Tensor Product of Algebras

Informal description

For any elements $a \in A$, $b \in B$, and $c \in C$ of $R$-algebras $A$, $B$, and $C$ respectively, the associator isomorphism maps the tensor product $(a \otimes_R b) \otimes_R c$ to $a \otimes_R (b \otimes_R c)$.

Algebra.TensorProduct.assoc_symm_tmul theorem

(a : A) (b : B) (c : C) : (Algebra.TensorProduct.assoc R A B C).symm (a ⊗ₜ (b ⊗ₜ c)) = (a ⊗ₜ b) ⊗ₜ c

Full source

@[simp]
theorem assoc_symm_tmul (a : A) (b : B) (c : C) :
    (Algebra.TensorProduct.assoc R A B C).symm (a ⊗ₜ (b ⊗ₜ c)) = (a ⊗ₜ b) ⊗ₜ c :=
  rfl

Inverse Associativity Isomorphism for Tensor Product of Algebras

Informal description

For any elements $a \in A$, $b \in B$, and $c \in C$, the inverse of the associativity isomorphism for tensor products of algebras satisfies \[ (\text{assoc}_{R,A,B,C})^{-1}(a \otimes (b \otimes c)) = (a \otimes b) \otimes c, \] where $\otimes$ denotes the tensor product over the commutative ring $R$.

Algebra.TensorProduct.cancelBaseChange_tmul theorem

(a : A) (s : S) (b : B) : Algebra.TensorProduct.cancelBaseChange R S T A B (a ⊗ₜ (s ⊗ₜ b)) = (s • a) ⊗ₜ b

Full source

@[simp]
lemma cancelBaseChange_tmul (a : A) (s : S) (b : B) :
    Algebra.TensorProduct.cancelBaseChange R S T A B (a ⊗ₜ (s ⊗ₜ b)) = (s • a) ⊗ₜ b :=
  TensorProduct.AlgebraTensorModule.cancelBaseChange_tmul R S T a b s

Action of Base Change Cancellation on Tensor Products

Informal description

Let $R$, $S$, $T$ be commutative rings, $A$ an $S$-algebra, and $B$ an $R$-algebra. For any $a \in A$, $s \in S$, and $b \in B$, the base change cancellation map satisfies \[ \text{cancelBaseChange}(a \otimes (s \otimes b)) = (s \cdot a) \otimes b \] where $\otimes$ denotes the tensor product over $R$ and $\cdot$ denotes the scalar multiplication of $S$ on $A$.

Algebra.TensorProduct.cancelBaseChange_symm_tmul theorem

(a : A) (b : B) : (Algebra.TensorProduct.cancelBaseChange R S T A B).symm (a ⊗ₜ b) = a ⊗ₜ (1 ⊗ₜ b)

Full source

@[simp]
lemma cancelBaseChange_symm_tmul (a : A) (b : B) :
    (Algebra.TensorProduct.cancelBaseChange R S T A B).symm (a ⊗ₜ b) = a ⊗ₜ (1 ⊗ₜ b) :=
  TensorProduct.AlgebraTensorModule.cancelBaseChange_symm_tmul R S T a b

Inverse Base Change Isomorphism on Tensor Product Elements

Informal description

For any elements $a \in A$ and $b \in B$, the inverse of the base change isomorphism applied to the tensor product $a \otimes b$ equals $a \otimes (1 \otimes b)$, where $1$ is the multiplicative identity in $S$.

Algebra.TensorProduct.map_tmul theorem

(f : A →ₐ[S] C) (g : B →ₐ[R] D) (a : A) (b : B) : map f g (a ⊗ₜ b) = f a ⊗ₜ g b

Full source

@[simp]
theorem map_tmul (f : A →ₐ[S] C) (g : B →ₐ[R] D) (a : A) (b : B) : map f g (a ⊗ₜ b) = f a ⊗ₜ g b :=
  rfl

Tensor Product of Algebra Homomorphisms Preserves Tensor Product Elements

Informal description

For any algebra homomorphisms $f \colon A \to C$ over $S$ and $g \colon B \to D$ over $R$, and any elements $a \in A$ and $b \in B$, the tensor product map $f \otimes g$ satisfies $(f \otimes g)(a \otimes b) = f(a) \otimes g(b)$.

Algebra.TensorProduct.map_id theorem

: map (.id S A) (.id R B) = .id S _

Full source

@[simp]
theorem map_id : map (.id S A) (.id R B) = .id S _ :=
  ext (AlgHom.ext fun _ => rfl) (AlgHom.ext fun _ => rfl)

Identity Mapping on Tensor Product of Algebras Preserves Identity

Informal description

The algebra homomorphism `map` applied to the identity homomorphism on $A$ as an $S$-algebra and the identity homomorphism on $B$ as an $R$-algebra is equal to the identity homomorphism on $A \otimes_R B$ as an $S$-algebra.

Algebra.TensorProduct.map_comp theorem

 (f₂ : C →ₐ[S] E) (f₁ : A →ₐ[S] C) (g₂ : D →ₐ[R] F) (g₁ : B →ₐ[R] D) :
  map (f₂.comp f₁) (g₂.comp g₁) = (map f₂ g₂).comp (map f₁ g₁)

Full source

theorem map_comp
    (f₂ : C →ₐ[S] E) (f₁ : A →ₐ[S] C) (g₂ : D →ₐ[R] F) (g₁ : B →ₐ[R] D) :
    map (f₂.comp f₁) (g₂.comp g₁) = (map f₂ g₂).comp (map f₁ g₁) :=
  ext (AlgHom.ext fun _ => rfl) (AlgHom.ext fun _ => rfl)

Composition of Tensor Product Maps of Algebra Homomorphisms

Informal description

Let $A$, $C$, $E$ be $S$-algebras and $B$, $D$, $F$ be $R$-algebras. For algebra homomorphisms $f_1 \colon A \to C$, $f_2 \colon C \to E$, $g_1 \colon B \to D$, and $g_2 \colon D \to F$, 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 algebra homomorphism $A \otimes_R B \to C \otimes_R D$ given by $a \otimes b \mapsto f(a) \otimes g(b)$.

Algebra.TensorProduct.map_id_comp theorem

 (g₂ : D →ₐ[R] F) (g₁ : B →ₐ[R] D) :
  map (AlgHom.id S A) (g₂.comp g₁) = (map (AlgHom.id S A) g₂).comp (map (AlgHom.id S A) g₁)

Full source

lemma map_id_comp (g₂ : D →ₐ[R] F) (g₁ : B →ₐ[R] D) :
    map (AlgHom.id S A) (g₂.comp g₁) = (map (AlgHom.id S A) g₂).comp (map (AlgHom.id S A) g₁) :=
  ext (AlgHom.ext fun _ => rfl) (AlgHom.ext fun _ => rfl)

Tensor Product Map with Identity Preserves Composition on Right Factor

Informal description

Let $A$ be an $S$-algebra, and let $B$, $D$, $F$ be $R$-algebras. For algebra homomorphisms $g_1 \colon B \to D$ and $g_2 \colon D \to F$, the tensor product map with the identity homomorphism on $A$ satisfies: \[ \text{map}(\text{id}_A, g_2 \circ g_1) = \text{map}(\text{id}_A, g_2) \circ \text{map}(\text{id}_A, g_1) \] where $\text{map}(\text{id}_A, g)$ denotes the induced algebra homomorphism $A \otimes_R B \to A \otimes_R F$ given by $a \otimes b \mapsto a \otimes g(b)$.

Algebra.TensorProduct.map_comp_id theorem

 (f₂ : C →ₐ[S] E) (f₁ : A →ₐ[S] C) :
  map (f₂.comp f₁) (AlgHom.id R E) = (map f₂ (AlgHom.id R E)).comp (map f₁ (AlgHom.id R E))

Full source

lemma map_comp_id
    (f₂ : C →ₐ[S] E) (f₁ : A →ₐ[S] C) :
    map (f₂.comp f₁) (AlgHom.id R E) = (map f₂ (AlgHom.id R E)).comp (map f₁ (AlgHom.id R E)) :=
  ext (AlgHom.ext fun _ => rfl) (AlgHom.ext fun _ => rfl)

Composition of Tensor Product Maps with Identity on the Right

Informal description

Let $A$, $C$, and $E$ be $S$-algebras, and let $E$ also be an $R$-algebra. For algebra homomorphisms $f_1 \colon A \to C$ and $f_2 \colon C \to E$, the tensor product map satisfies: \[ \text{map}(f_2 \circ f_1, \text{id}_E) = \text{map}(f_2, \text{id}_E) \circ \text{map}(f_1, \text{id}_E) \] where $\text{map}(f, \text{id}_E)$ denotes the induced algebra homomorphism $A \otimes_R E \to C \otimes_R E$ given by $a \otimes e \mapsto f(a) \otimes e$.

Algebra.TensorProduct.map_comp_includeLeft theorem

(f : A →ₐ[S] C) (g : B →ₐ[R] D) : (map f g).comp includeLeft = includeLeft.comp f

Full source

@[simp]
theorem map_comp_includeLeft (f : A →ₐ[S] C) (g : B →ₐ[R] D) :
    (map f g).comp includeLeft = includeLeft.comp f :=
  AlgHom.ext <| by simp

Compatibility of Tensor Product Map with Left Inclusion for Algebra Homomorphisms

Informal description

Let $A$, $B$, $C$, $D$ be $R$-algebras, with $A$ and $C$ additionally being $S$-algebras. Given algebra homomorphisms $f \colon A \to C$ (as $S$-algebras) and $g \colon B \to D$ (as $R$-algebras), the composition of the tensor product map $f \otimes g$ with the left inclusion map $\text{includeLeft} \colon A \to A \otimes_R B$ equals the composition of $f$ with $\text{includeLeft} \colon C \to C \otimes_R D$.

Algebra.TensorProduct.map_restrictScalars_comp_includeRight theorem

(f : A →ₐ[S] C) (g : B →ₐ[R] D) : ((map f g).restrictScalars R).comp includeRight = includeRight.comp g

Full source

@[simp]
theorem map_restrictScalars_comp_includeRight (f : A →ₐ[S] C) (g : B →ₐ[R] D) :
    ((map f g).restrictScalars R).comp includeRight = includeRight.comp g :=
  AlgHom.ext <| by simp

Compatibility of Tensor Product Map Restriction with Right Inclusion

Informal description

Let $R$ and $S$ be commutative (semi)rings, and let $A$ be an $S$-algebra, $B$ and $D$ be $R$-algebras, and $C$ be an $S$-algebra. Given $S$-algebra homomorphisms $f: A \to C$ and $R$-algebra homomorphisms $g: B \to D$, the composition of the restriction of scalars of the tensor product map $\text{map}(f, g)$ with the right inclusion $\text{includeRight}$ is equal to the composition of $g$ with $\text{includeRight}$. In symbols: $$(\text{map}(f, g)|_R) \circ \text{includeRight} = \text{includeRight} \circ g$$

Algebra.TensorProduct.map_comp_includeRight theorem

(f : A →ₐ[R] C) (g : B →ₐ[R] D) : (map f g).comp includeRight = includeRight.comp g

Full source

@[simp]
theorem map_comp_includeRight (f : A →ₐ[R] C) (g : B →ₐ[R] D) :
    (map f g).comp includeRight = includeRight.comp g :=
  map_restrictScalars_comp_includeRight f g

Compatibility of Tensor Product Map with Right Inclusion for Algebra Homomorphisms

Informal description

Let $A$, $B$, $C$, $D$ be $R$-algebras, and let $f \colon A \to C$ and $g \colon B \to D$ be $R$-algebra homomorphisms. Then the composition of the tensor product map $f \otimes g \colon A \otimes_R B \to C \otimes_R D$ with the right inclusion $\text{includeRight} \colon D \to C \otimes_R D$ is equal to the composition of $g$ with $\text{includeRight} \colon B \to A \otimes_R B$. In symbols: $$(f \otimes g) \circ \text{includeRight} = \text{includeRight} \circ g$$

Algebra.TensorProduct.map_range theorem

(f : A →ₐ[R] C) (g : B →ₐ[R] D) : (map f g).range = (includeLeft.comp f).range ⊔ (includeRight.comp g).range

Full source

theorem map_range (f : A →ₐ[R] C) (g : B →ₐ[R] D) :
    (map f g).range = (includeLeft.comp f).range ⊔ (includeRight.comp g).range := by
  apply le_antisymm
  · rw [← map_top, ← adjoin_tmul_eq_top, ← adjoin_image, adjoin_le_iff]
    rintro _ ⟨_, ⟨a, b, rfl⟩, rfl⟩
    rw [map_tmul, ← mul_one (f a), ← one_mul (g b), ← tmul_mul_tmul]
    exact mul_mem_sup (AlgHom.mem_range_self _ a) (AlgHom.mem_range_self _ b)
  · rw [← map_comp_includeLeft f g, ← map_comp_includeRight f g]
    exact sup_le (AlgHom.range_comp_le_range _ _) (AlgHom.range_comp_le_range _ _)

Range of Tensor Product Map as Supremum of Component Ranges

Informal description

Let $A$, $B$, $C$, and $D$ be $R$-algebras, and let $f \colon A \to C$ and $g \colon B \to D$ be $R$-algebra homomorphisms. The range of the tensor product map $f \otimes g \colon A \otimes_R B \to C \otimes_R D$ is equal to the supremum of the ranges of the compositions $\text{includeLeft} \circ f$ and $\text{includeRight} \circ g$. In symbols: $$\text{range}(f \otimes g) = \text{range}(\text{includeLeft} \circ f) \sqcup \text{range}(\text{includeRight} \circ g)$$

Algebra.TensorProduct.comm_comp_map theorem

 (f : A →ₐ[R] C) (g : B →ₐ[R] D) :
  (TensorProduct.comm R C D : C ⊗[R] D →ₐ[R] D ⊗[R] C).comp (Algebra.TensorProduct.map f g) =
    (Algebra.TensorProduct.map g f).comp (TensorProduct.comm R A B).toAlgHom

Full source

lemma comm_comp_map (f : A →ₐ[R] C) (g : B →ₐ[R] D) :
    (TensorProduct.comm R C D : C ⊗[R] DC ⊗[R] D →ₐ[R] D ⊗[R] C).comp (Algebra.TensorProduct.map f g) =
    (Algebra.TensorProduct.map g f).comp (TensorProduct.comm R A B).toAlgHom := by
  ext <;> rfl

Commutativity of Tensor Product of Algebra Homomorphisms with Commutativity Isomorphism

Informal description

Let $A$, $B$, $C$, and $D$ be $R$-algebras, and let $f \colon A \to C$ and $g \colon B \to D$ be $R$-algebra homomorphisms. Then the following diagram commutes: \[ \begin{CD} A \otimes_R B @>{\text{comm}_R(A,B)}>> B \otimes_R A \\ @V{\text{map}(f,g)}VV @VV{\text{map}(g,f)}V \\ C \otimes_R D @>>{\text{comm}_R(C,D)}> D \otimes_R C \end{CD} \] where $\text{comm}_R(X,Y)$ denotes the canonical commutativity isomorphism $X \otimes_R Y \cong Y \otimes_R X$ for $R$-algebras $X$ and $Y$, and $\text{map}(f,g)$ denotes the tensor product of algebra homomorphisms $f$ and $g$.

Algebra.TensorProduct.comm_comp_map_apply theorem

 (f : A →ₐ[R] C) (g : B →ₐ[R] D) (x) :
  TensorProduct.comm R C D (Algebra.TensorProduct.map f g x) =
    (Algebra.TensorProduct.map g f) (TensorProduct.comm R A B x)

Full source

lemma comm_comp_map_apply (f : A →ₐ[R] C) (g : B →ₐ[R] D) (x) :
    TensorProduct.comm R C D (Algebra.TensorProduct.map f g x) =
    (Algebra.TensorProduct.map g f) (TensorProduct.comm R A B x) :=
  congr($(comm_comp_map f g) x)

Commutativity of Tensor Product of Algebra Homomorphisms Applied to Elements

Informal description

Let $R$ be a commutative (semi)ring, and let $A$, $B$, $C$, $D$ be $R$-algebras. Given $R$-algebra homomorphisms $f \colon A \to C$ and $g \colon B \to D$, and an element $x \in A \otimes_R B$, the following equality holds: \[ \text{comm}_{R}(C,D) \big( (f \otimes g)(x) \big) = (g \otimes f) \big( \text{comm}_{R}(A,B)(x) \big), \] where $\text{comm}_{R}(X,Y) \colon X \otimes_R Y \to Y \otimes_R X$ denotes the canonical commutativity isomorphism for $R$-algebras $X$ and $Y$, and $f \otimes g$ denotes the tensor product of the algebra homomorphisms $f$ and $g$.

Algebra.TensorProduct.congr_toLinearEquiv theorem

 (f : A ≃ₐ[S] C) (g : B ≃ₐ[R] D) :
  (Algebra.TensorProduct.congr f g).toLinearEquiv =
    TensorProduct.AlgebraTensorModule.congr f.toLinearEquiv g.toLinearEquiv

Full source

@[simp] theorem congr_toLinearEquiv (f : A ≃ₐ[S] C) (g : B ≃ₐ[R] D) :
    (Algebra.TensorProduct.congr f g).toLinearEquiv =
      TensorProduct.AlgebraTensorModule.congr f.toLinearEquiv g.toLinearEquiv := rfl

Tensor Product Congruence Preserves Linear Equivalence Structure

Informal description

Let $A$ and $C$ be $S$-algebras, and $B$ and $D$ be $R$-algebras. Given algebra isomorphisms $f: A \simeq C$ over $S$ and $g: B \simeq D$ over $R$, the underlying linear equivalence of the tensor product congruence $\text{congr}(f,g)$ is equal to the tensor product congruence of the underlying linear equivalences of $f$ and $g$.

Algebra.TensorProduct.congr_apply theorem

(f : A ≃ₐ[S] C) (g : B ≃ₐ[R] D) (x) : congr f g x = (map (f : A →ₐ[S] C) (g : B →ₐ[R] D)) x

Full source

@[simp]
theorem congr_apply (f : A ≃ₐ[S] C) (g : B ≃ₐ[R] D) (x) :
    congr f g x = (map (f : A →ₐ[S] C) (g : B →ₐ[R] D)) x :=
  rfl

Tensor Product Congruence Map Application Formula

Informal description

Let $R$ and $S$ be commutative (semi)rings, and let $A$, $B$, $C$, $D$ be $R$-algebras with $A$ and $C$ additionally being $S$-algebras. Given algebra isomorphisms $f: A \simeq_{S} C$ and $g: B \simeq_{R} D$, and an element $x \in A \otimes_{R} B$, the application of the tensor product congruence map $\text{congr}(f,g)$ to $x$ equals the application of the tensor product map $\text{map}(f,g)$ to $x$.

Algebra.TensorProduct.congr_symm_apply theorem

 (f : A ≃ₐ[S] C) (g : B ≃ₐ[R] D) (x) : (congr f g).symm x = (map (f.symm : C →ₐ[S] A) (g.symm : D →ₐ[R] B)) x

Full source

@[simp]
theorem congr_symm_apply (f : A ≃ₐ[S] C) (g : B ≃ₐ[R] D) (x) :
    (congr f g).symm x = (map (f.symm : C →ₐ[S] A) (g.symm : D →ₐ[R] B)) x :=
  rfl

Inverse of Tensor Product Algebra Isomorphism Equals Tensor Product of Inverses

Informal description

Let $A$ and $C$ be $S$-algebras, $B$ and $D$ be $R$-algebras, and let $f: A \simeq C$ and $g: B \simeq D$ be algebra isomorphisms. For any element $x$ in the tensor product $C \otimes_R D$, the inverse of the tensor product isomorphism $\text{congr}(f,g)$ applied to $x$ equals the tensor product of the inverses $f^{-1}$ and $g^{-1}$ applied to $x$, i.e., $$(\text{congr}(f,g))^{-1}(x) = (f^{-1} \otimes g^{-1})(x).$$

Algebra.TensorProduct.congr_refl theorem

: congr (.refl : A ≃ₐ[S] A) (.refl : B ≃ₐ[R] B) = .refl

Full source

@[simp]
theorem congr_refl : congr (.refl : A ≃ₐ[S] A) (.refl : B ≃ₐ[R] B) = .refl :=
  AlgEquiv.coe_algHom_injective <| map_id

Identity Isomorphism Mapping on Tensor Product of Algebras Preserves Identity

Informal description

The algebra isomorphism `congr` applied to the identity isomorphism on $A$ as an $S$-algebra and the identity isomorphism on $B$ as an $R$-algebra is equal to the identity isomorphism on $A \otimes_R B$ as an $S$-algebra.

Algebra.TensorProduct.congr_trans theorem

 (f₁ : A ≃ₐ[S] C) (f₂ : C ≃ₐ[S] E) (g₁ : B ≃ₐ[R] D) (g₂ : D ≃ₐ[R] F) :
  congr (f₁.trans f₂) (g₁.trans g₂) = (congr f₁ g₁).trans (congr f₂ g₂)

Full source

theorem congr_trans
    (f₁ : A ≃ₐ[S] C) (f₂ : C ≃ₐ[S] E) (g₁ : B ≃ₐ[R] D) (g₂ : D ≃ₐ[R] F) :
    congr (f₁.trans f₂) (g₁.trans g₂) = (congr f₁ g₁).trans (congr f₂ g₂) :=
  AlgEquiv.coe_algHom_injective <| map_comp f₂.toAlgHom f₁.toAlgHom g₂.toAlgHom g₁.toAlgHom

Composition of Tensor Product Isomorphisms of Algebra Isomorphisms

Informal description

Let $A$, $C$, $E$ be $S$-algebras and $B$, $D$, $F$ be $R$-algebras. Given algebra isomorphisms $f_1 \colon A \to C$, $f_2 \colon C \to E$, $g_1 \colon B \to D$, and $g_2 \colon D \to F$, the tensor product isomorphism satisfies: \[ \text{congr}(f_1 \circ f_2, g_1 \circ g_2) = \text{congr}(f_1, g_1) \circ \text{congr}(f_2, g_2) \] where $\text{congr}(f, g)$ denotes the induced algebra isomorphism $A \otimes_R B \to C \otimes_R D$ given by $a \otimes b \mapsto f(a) \otimes g(b)$.

Algebra.TensorProduct.congr_symm theorem

(f : A ≃ₐ[S] C) (g : B ≃ₐ[R] D) : congr f.symm g.symm = (congr f g).symm

Full source

theorem congr_symm (f : A ≃ₐ[S] C) (g : B ≃ₐ[R] D) : congr f.symm g.symm = (congr f g).symm := rfl

Inverse of Tensor Product of Algebra Isomorphisms

Informal description

For any $S$-algebra isomorphisms $f: A \simeq C$ and $R$-algebra isomorphisms $g: B \simeq D$, the tensor product of the inverse isomorphisms $f^{-1}$ and $g^{-1}$ is equal to the inverse of the tensor product isomorphism $f \otimes g$. In other words, $(f \otimes g)^{-1} = f^{-1} \otimes g^{-1}$.

Algebra.TensorProduct.leftComm_tmul theorem

(m : A) (n : B) (p : C) : leftComm R A B C (m ⊗ₜ (n ⊗ₜ p)) = n ⊗ₜ (m ⊗ₜ p)

Full source

@[simp]
theorem leftComm_tmul (m : A) (n : B) (p : C) :
    leftComm R A B C (m ⊗ₜ (n ⊗ₜ p)) = n ⊗ₜ (m ⊗ₜ p) :=
  rfl

Left Commutativity Isomorphism for Tensor Product of Algebras

Informal description

Let $R$ be a commutative (semi)ring, and let $A$, $B$, $C$ be $R$-algebras. For any elements $m \in A$, $n \in B$, and $p \in C$, the left commutativity isomorphism $\text{leftComm}_{R,A,B,C}$ satisfies: \[ \text{leftComm}_{R,A,B,C}(m \otimes (n \otimes p)) = n \otimes (m \otimes p) \] where $\otimes$ denotes the tensor product over $R$.

Algebra.TensorProduct.leftComm_symm_tmul theorem

(m : A) (n : B) (p : C) : (leftComm R A B C).symm (n ⊗ₜ (m ⊗ₜ p)) = m ⊗ₜ (n ⊗ₜ p)

Full source

@[simp]
theorem leftComm_symm_tmul (m : A) (n : B) (p : C) :
    (leftComm R A B C).symm (n ⊗ₜ (m ⊗ₜ p)) = m ⊗ₜ (n ⊗ₜ p) :=
  rfl

Inverse Left Commutation of Tensor Products: $n \otimes (m \otimes p) \mapsto m \otimes (n \otimes p)$

Informal description

Let $R$ be a commutative (semi)ring, and let $A$, $B$, $C$ be $R$-algebras. For any elements $m \in A$, $n \in B$, $p \in C$, the inverse of the left commutation isomorphism satisfies: \[ \text{leftComm}_{R,A,B,C}^{-1}(n \otimes (m \otimes p)) = m \otimes (n \otimes p) \]

Algebra.TensorProduct.leftComm_toLinearEquiv theorem

: (leftComm R A B C : _ ≃ₗ[R] _) = _root_.TensorProduct.leftComm R A B C

Full source

@[simp]
theorem leftComm_toLinearEquiv :
    (leftComm R A B C : _ ≃ₗ[R] _) = _root_.TensorProduct.leftComm R A B C := rfl

Equality of Left Commutation Linear Equivalences for Tensor Products

Informal description

The linear equivalence `leftComm R A B C` between the tensor products `(A ⊗[R] B) ⊗[R] C` and `(B ⊗[R] A) ⊗[R] C` as `R`-modules is equal to the underlying linear equivalence of the tensor product left commutation isomorphism `TensorProduct.leftComm R A B C`.

Algebra.TensorProduct.tensorTensorTensorComm_tmul theorem

 (m : A) (n : B) (p : C) (q : D) : tensorTensorTensorComm R S A B C D (m ⊗ₜ n ⊗ₜ (p ⊗ₜ q)) = m ⊗ₜ p ⊗ₜ (n ⊗ₜ q)

Full source

@[simp]
theorem tensorTensorTensorComm_tmul (m : A) (n : B) (p : C) (q : D) :
    tensorTensorTensorComm R S A B C D (m ⊗ₜ n ⊗ₜ (p ⊗ₜ q)) = m ⊗ₜ pm ⊗ₜ p ⊗ₜ (n ⊗ₜ q) :=
  rfl

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

Informal description

Let $R$ and $S$ be commutative (semi)rings, and let $A$, $B$, $C$, $D$ be $R$-algebras. For any elements $m \in A$, $n \in B$, $p \in C$, $q \in D$, the tensor tensor tensor commutation map satisfies: \[ \text{tensorTensorTensorComm}_{R,S,A,B,C,D}(m \otimes n \otimes (p \otimes q)) = m \otimes p \otimes (n \otimes q) \]

Algebra.TensorProduct.tensorTensorTensorComm_symm_tmul theorem

 (m : A) (n : C) (p : B) (q : D) : (tensorTensorTensorComm R S A B C D).symm (m ⊗ₜ n ⊗ₜ (p ⊗ₜ q)) = m ⊗ₜ p ⊗ₜ (n ⊗ₜ q)

Full source

@[simp]
theorem tensorTensorTensorComm_symm_tmul (m : A) (n : C) (p : B) (q : D) :
    (tensorTensorTensorComm R S A B C D).symm (m ⊗ₜ n ⊗ₜ (p ⊗ₜ q)) = m ⊗ₜ pm ⊗ₜ p ⊗ₜ (n ⊗ₜ q) :=
  rfl

Inverse Tensor Commutation Isomorphism Action on Pure Tensors

Informal description

Let $R$ and $S$ be commutative (semi)rings, and let $A$, $B$, $C$, $D$ be $R$-algebras. For any elements $m \in A$, $n \in C$, $p \in B$, $q \in D$, the inverse of the tensor tensor tensor commutation isomorphism satisfies: $$(\text{tensorTensorTensorComm}_{R,S,A,B,C,D})^{-1}(m \otimes n \otimes (p \otimes q)) = m \otimes p \otimes (n \otimes q)$$ where $\otimes$ denotes the tensor product over $R$.

Algebra.TensorProduct.tensorTensorTensorComm_symm theorem

: (tensorTensorTensorComm R R A B C D).symm = tensorTensorTensorComm R R A C B D

Full source

theorem tensorTensorTensorComm_symm :
    (tensorTensorTensorComm R R A B C D).symm = tensorTensorTensorComm R R A C B D := by
  ext; rfl

Symmetry of Tensor Reordering Isomorphism

Informal description

Let $R$ be a commutative (semi)ring and let $A, B, C, D$ be $R$-algebras. The symmetry isomorphism of the tensor tensor tensor commutation map satisfies: $$(\text{tensorTensorTensorComm}_{R,R}^{A,B,C,D})^{-1} = \text{tensorTensorTensorComm}_{R,R}^{A,C,B,D}$$ where $\text{tensorTensorTensorComm}$ is the natural isomorphism $(A ⊗_R B) ⊗_R (C ⊗_R D) ≅ (A ⊗_R C) ⊗_R (B ⊗_R D)$ of $R$-algebras.

Algebra.TensorProduct.tensorTensorTensorComm_toLinearEquiv theorem

 :
  (tensorTensorTensorComm R S A B C D).toLinearEquiv =
    TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R S A B C D

Full source

theorem tensorTensorTensorComm_toLinearEquiv :
    (tensorTensorTensorComm R S A B C D).toLinearEquiv =
      TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R S A B C D := rfl

Linear Equivalence of Tensor Tensor Tensor Commutation Isomorphism

Informal description

The linear equivalence underlying the algebra isomorphism `tensorTensorTensorComm R S A B C D` is equal to the linear equivalence `TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R S A B C D`.

Algebra.TensorProduct.toLinearEquiv_tensorTensorTensorComm theorem

: (tensorTensorTensorComm R R A B C D).toLinearEquiv = _root_.TensorProduct.tensorTensorTensorComm R A B C D

Full source

@[simp]
theorem toLinearEquiv_tensorTensorTensorComm :
    (tensorTensorTensorComm R R A B C D).toLinearEquiv =
      _root_.TensorProduct.tensorTensorTensorComm R A B C D := by
  apply LinearEquiv.toLinearMap_injective
  ext; simp

Equality of Underlying Linear Equivalences for Tensor Product Commutation Isomorphism

Informal description

The linear equivalence underlying the tensor product commutation isomorphism `tensorTensorTensorComm R R A B C D` is equal to the tensor product commutation linear equivalence `_root_.TensorProduct.tensorTensorTensorComm R A B C D`.

Algebra.TensorProduct.tmul_one_eq_one_tmul theorem

(r : R) : algebraMap R A r ⊗ₜ[R] 1 = 1 ⊗ₜ algebraMap R B r

Full source

lemma tmul_one_eq_one_tmul (r : R) : algebraMapalgebraMap R A r ⊗ₜ[R] 1 = 1 ⊗ₜ algebraMap R B r := by
  rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, smul_tmul]

Equality of Tensor Products of Algebra Maps with Identities

Informal description

For any element $r$ in a commutative (semi)ring $R$, and for any two $R$-algebras $A$ and $B$, the tensor product of the algebra map $\text{algebraMap}_R^A(r)$ with the multiplicative identity $1$ in $B$ is equal to the tensor product of the multiplicative identity $1$ in $A$ with the algebra map $\text{algebraMap}_R^B(r)$. That is, \[ \text{algebraMap}_R^A(r) \otimes_R 1_B = 1_A \otimes_R \text{algebraMap}_R^B(r). \]

Algebra.TensorProduct.lmul''_eq_lid_comp_mapOfCompatibleSMul theorem

: lmul'' R = (TensorProduct.lid S S).toAlgHom.comp (mapOfCompatibleSMul' _ _ _ _)

Full source

theorem lmul''_eq_lid_comp_mapOfCompatibleSMul :
    lmul'' R = (TensorProduct.lid S S).toAlgHom.comp (mapOfCompatibleSMul' _ _ _ _) := by
  ext; rfl

Decomposition of Left Multiplication in Tensor Product Algebra

Informal description

The left multiplication map `lmul'' R` on the tensor product algebra $S \otimes_R S$ is equal to the composition of the algebra isomorphism `TensorProduct.lid S S` with the map `mapOfCompatibleSMul'` that accounts for the compatible scalar multiplication structure.

Algebra.TensorProduct.lmul'_toLinearMap theorem

: (lmul' R : _ →ₐ[R] S).toLinearMap = LinearMap.mul' R S

Full source

theorem lmul'_toLinearMap : (lmul' R : _ →ₐ[R] S).toLinearMap = LinearMap.mul' R S :=
  rfl

Equality of Linear Maps: Tensor Product Multiplication and Algebra Multiplication

Informal description

The underlying linear map of the algebra homomorphism `lmul' R` from the tensor product $S \otimes_R S$ to $S$ is equal to the multiplication linear map `mul' R S` on $S$.

Algebra.TensorProduct.lmul'_apply_tmul theorem

(a b : S) : lmul' (S := S) R (a ⊗ₜ[R] b) = a * b

Full source

@[simp]
theorem lmul'_apply_tmul (a b : S) : lmul' (S := S) R (a ⊗ₜ[R] b) = a * b :=
  rfl

Left multiplication on tensor product algebra: $\mathrm{lmul}'(a \otimes b) = ab$

Informal description

For any elements $a, b$ in an $R$-algebra $S$, the left multiplication map $\mathrm{lmul}'$ on the tensor product $S \otimes_R S$ satisfies $\mathrm{lmul}'(a \otimes_R b) = a \cdot b$.

Algebra.TensorProduct.lmul'_comp_includeLeft theorem

: (lmul' R : _ →ₐ[R] S).comp includeLeft = AlgHom.id R S

Full source

@[simp]
theorem lmul'_comp_includeLeft : (lmul' R : _ →ₐ[R] S).comp includeLeft = AlgHom.id R S :=
  AlgHom.ext <| mul_one

Left multiplication composed with left inclusion equals identity for tensor product algebras

Informal description

Let $R$ be a commutative (semi)ring and $S$ an $R$-algebra. The composition of the left multiplication algebra homomorphism $\text{lmul}'_R : S ⊗_R S →ₐ[R] S$ with the left inclusion homomorphism $\text{includeLeft} : S →ₐ[R] S ⊗_R S$ equals the identity algebra homomorphism $\text{id}_R S : S →ₐ[R] S$.

Algebra.TensorProduct.lmul'_comp_includeRight theorem

: (lmul' R : _ →ₐ[R] S).comp includeRight = AlgHom.id R S

Full source

@[simp]
theorem lmul'_comp_includeRight : (lmul' R : _ →ₐ[R] S).comp includeRight = AlgHom.id R S :=
  AlgHom.ext <| one_mul

Right inclusion composed with multiplication equals identity in tensor product algebra

Informal description

For a commutative ring $R$ and an $R$-algebra $S$, the composition of the algebra homomorphism `lmul' R` (which maps $S \otimes_R S$ to $S$ via multiplication) with the inclusion `includeRight` (which maps $S$ to $S \otimes_R S$ as $1 \otimes s$) equals the identity algebra homomorphism on $S$.

Algebra.TensorProduct.lmulEquiv_eq_lidOfCompatibleSMul theorem

[CompatibleSMul R S S S] : lmulEquiv R S = lidOfCompatibleSMul R S S

Full source

theorem lmulEquiv_eq_lidOfCompatibleSMul [CompatibleSMul R S S S] :
    lmulEquiv R S = lidOfCompatibleSMul R S S :=
  AlgEquiv.coe_algHom_injective <| by ext; rfl

Equivalence of Left Multiplication and Left Identity in Tensor Product Algebra

Informal description

Let $R$ be a commutative ring and $S$ an $R$-algebra with a compatible scalar multiplication structure. Then the left multiplication equivalence $\text{lmulEquiv}_R S$ is equal to the left identity equivalence $\text{lidOfCompatibleSMul}_R S S$ for the tensor product algebra structure.

Algebra.TensorProduct.productMap_eq_comp_map theorem

: productMap f g = (lmul' R).comp (TensorProduct.map f g)

Full source

theorem productMap_eq_comp_map : productMap f g = (lmul' R).comp (TensorProduct.map f g) := by
  ext <;> rfl

Product Map Decomposition via Tensor Product and Multiplication

Informal description

Let $R$ be a commutative ring, and let $A$, $B$, and $S$ be $R$-algebras. Given $R$-algebra homomorphisms $f \colon A \to S$ and $g \colon B \to S$, the product map $\text{productMap}(f, g) \colon A \otimes_R B \to S$ is equal to the composition of the multiplication map $\text{lmul}'_R \colon S \otimes_R S \to S$ with the tensor product map $\text{TensorProduct.map}(f, g) \colon A \otimes_R B \to S \otimes_R S$.

Algebra.TensorProduct.productMap_apply_tmul theorem

(a : A) (b : B) : productMap f g (a ⊗ₜ b) = f a * g b

Full source

@[simp]
theorem productMap_apply_tmul (a : A) (b : B) : productMap f g (a ⊗ₜ b) = f a * g b := rfl

Evaluation of Product Map on Tensor Product Elements

Informal description

For any elements $a \in A$ and $b \in B$, the product map $\text{productMap}\, f\, g$ evaluated at the tensor product $a \otimes b$ equals the product of $f(a)$ and $g(b)$, i.e., \[ \text{productMap}\, f\, g\, (a \otimes b) = f(a) \cdot g(b). \]

Algebra.TensorProduct.productMap_left_apply theorem

(a : A) : productMap f g (a ⊗ₜ 1) = f a

Full source

theorem productMap_left_apply (a : A) : productMap f g (a ⊗ₜ 1) = f a := by
  simp

Product Map Evaluation on Pure Tensors with Unit

Informal description

For any element $a$ in an $R$-algebra $A$, the product map $\mathrm{productMap}(f, g)$ evaluated at the tensor product $a \otimes 1$ equals $f(a)$, i.e., \[ \mathrm{productMap}(f, g)(a \otimes 1) = f(a). \]

Algebra.TensorProduct.productMap_left theorem

: (productMap f g).comp includeLeft = f

Full source

@[simp]
theorem productMap_left : (productMap f g).comp includeLeft = f :=
  lift_comp_includeLeft _ _ (fun _ _ => Commute.all _ _)

Left Inclusion Compatibility of Product Map in Tensor Product of Algebras

Informal description

For algebra homomorphisms $f \colon A \to C$ and $g \colon B \to C$, the composition of the product map $\text{productMap}(f,g) \colon A \otimes_R B \to C$ with the left inclusion $\text{includeLeft} \colon A \to A \otimes_R B$ equals $f$.

Algebra.TensorProduct.productMap_right_apply theorem

(b : B) : productMap f g (1 ⊗ₜ b) = g b

Full source

theorem productMap_right_apply (b : B) :
    productMap f g (1 ⊗ₜ b) = g b := by simp

Right Tensor Factor Evaluation in Product Map

Informal description

For any element $b$ in an $R$-algebra $B$, the product map $f \otimes g$ applied to the tensor product $1 \otimes b$ equals $g(b)$, i.e., $(f \otimes g)(1 \otimes b) = g(b)$.

Algebra.TensorProduct.productMap_right theorem

: (productMap f g).comp includeRight = g

Full source

@[simp]
theorem productMap_right : (productMap f g).comp includeRight = g :=
  lift_comp_includeRight _ _ (fun _ _ => Commute.all _ _)

Compatibility of product map with right inclusion

Informal description

Let $A$ and $B$ be $R$-algebras, and let $f: A \to C$ and $g: B \to C$ be $R$-algebra homomorphisms. Then the composition of the product map $\text{productMap}(f, g)$ with the right inclusion map $\text{includeRight}$ equals $g$. In mathematical notation: $$\text{productMap}(f, g) \circ \text{includeRight} = g$$

Algebra.TensorProduct.productMap_range theorem

: (productMap f g).range = f.range ⊔ g.range

Full source

theorem productMap_range : (productMap f g).range = f.range ⊔ g.range := by
  rw [productMap_eq_comp_map, AlgHom.range_comp, map_range, map_sup, ← AlgHom.range_comp,
    ← AlgHom.range_comp,
    ← AlgHom.comp_assoc, ← AlgHom.comp_assoc, lmul'_comp_includeLeft, lmul'_comp_includeRight,
    AlgHom.id_comp, AlgHom.id_comp]

Range of Tensor Product Product Map as Supremum of Component Ranges

Informal description

Let $R$ be a commutative semiring, and let $A$, $B$, and $S$ be $R$-algebras. Given $R$-algebra homomorphisms $f \colon A \to S$ and $g \colon B \to S$, the range of the product map $\text{productMap}(f, g) \colon A \otimes_R B \to S$ is equal to the supremum of the ranges of $f$ and $g$. In symbols: $$\text{range}(\text{productMap}(f, g)) = \text{range}(f) \sqcup \text{range}(g)$$

Algebra.TensorProduct.mk_one_injective_of_isScalarTower theorem

 (M : Type*) [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] :
  Function.Injective (TensorProduct.mk R S M 1)

Full source

/-- If `M` is a `B`-module that is also an `A`-module, the canonical map
`M →ₗ[A] B ⊗[A] M` is injective. -/
lemma mk_one_injective_of_isScalarTower (M : Type*) [AddCommMonoid M]
    [Module R M] [Module S M] [IsScalarTower R S M] :
    Function.Injective (TensorProduct.mk R S M 1) := by
  apply Function.RightInverse.injective (g := LinearMap.liftBaseChange S LinearMap.id)
  intro m
  simp

Injectivity of the canonical map $M \to S \otimes_R M$ for compatible module structures

Informal description

Let $R$ and $S$ be commutative semirings, and let $M$ be an $S$-module that is also an $R$-module with compatible scalar multiplication (i.e., $R$ acts through $S$ via an algebra structure). Then the canonical $S$-linear map $M \to S \otimes_R M$ defined by $m \mapsto 1 \otimes m$ is injective.

Algebra.baseChange_lmul theorem

 {R B : Type*} [CommSemiring R] [Semiring B] [Algebra R B] {A : Type*} [CommSemiring A] [Algebra R A] (f : B) :
  (Algebra.lmul R B f).baseChange A = Algebra.lmul A (A ⊗[R] B) (1 ⊗ₜ f)

Full source

lemma Algebra.baseChange_lmul {R B : Type*} [CommSemiring R] [Semiring B] [Algebra R B]
    {A : Type*} [CommSemiring A] [Algebra R A] (f : B) :
    (Algebra.lmul R B f).baseChange A = Algebra.lmul A (A ⊗[R] B) (1 ⊗ₜ f) := by
  ext i
  simp

Base Change of Left Multiplication Map Equals Left Multiplication of Base Changed Element

Informal description

Let $R$ be a commutative semiring, $B$ a semiring with an $R$-algebra structure, and $A$ a commutative semiring with an $R$-algebra structure. For any element $f \in B$, the base change of the left multiplication map $\text{lmul}_R(f) : B \to B$ to $A$ is equal to the left multiplication map $\text{lmul}_A(1 \otimes_R f) : A \otimes_R B \to A \otimes_R B$.

Module.endTensorEndAlgHom_apply theorem

 (f : End A M) (g : End R N) :
  endTensorEndAlgHom (R := R) (S := S) (A := A) (M := M) (N := N) (f ⊗ₜ[R] g) = AlgebraTensorModule.map f g

Full source

theorem endTensorEndAlgHom_apply (f : End A M) (g : End R N) :
    endTensorEndAlgHom (R := R) (S := S) (A := A) (M := M) (N := N) (f ⊗ₜ[R] g)
      = AlgebraTensorModule.map f g :=
  rfl

Tensor Product of Endomorphisms Equals Tensor Product of Module Maps

Informal description

Let $R$ and $S$ be commutative semirings, $A$ an $S$-algebra, $M$ an $A$-module, and $N$ an $R$-module. For any endomorphism $f$ of $M$ as an $A$-module and any endomorphism $g$ of $N$ as an $R$-module, the algebra homomorphism $\text{endTensorEndAlgHom}$ applied to the tensor product $f \otimes_R g$ equals the tensor product of module maps $\text{AlgebraTensorModule.map}(f, g)$.

TensorProduct.Algebra.moduleAux_apply theorem

(a : A) (b : B) (m : M) : moduleAux (a ⊗ₜ[R] b) m = a • b • m

Full source

theorem moduleAux_apply (a : A) (b : B) (m : M) : moduleAux (a ⊗ₜ[R] b) m = a • b • m :=
  rfl

Tensor product action formula: $(a \otimes_R b) \cdot m = a \cdot (b \cdot m)$

Informal description

For any elements $a \in A$, $b \in B$, and $m \in M$, the action of the tensor product $a \otimes_R b$ on $m$ via the module structure `moduleAux` is given by $a \cdot (b \cdot m)$, where $\cdot$ denotes the respective scalar multiplications in $A$ and $B$.

TensorProduct.Algebra.smul_def theorem

(a : A) (b : B) (m : M) : a ⊗ₜ[R] b • m = a • b • m

Full source

theorem smul_def (a : A) (b : B) (m : M) : a ⊗ₜ[R] b • m = a • b • m :=
  rfl

Tensor product scalar multiplication formula: $(a \otimes_R b) \cdot m = a \cdot (b \cdot m)$

Informal description

For any elements $a \in A$, $b \in B$, and $m \in M$, the scalar multiplication of the tensor product $a \otimes_R b$ acting on $m$ is given by $a \cdot (b \cdot m)$, where $\cdot$ denotes the respective scalar multiplications in $A$ and $B$.

TensorProduct.Algebra.linearMap_comp_mul' theorem

: Algebra.linearMap R (A ⊗[R] B) ∘ₗ LinearMap.mul' R R = map (Algebra.linearMap R A) (Algebra.linearMap R B)

Full source

theorem linearMap_comp_mul' :
    Algebra.linearMapAlgebra.linearMap R (A ⊗[R] B) ∘ₗ LinearMap.mul' R R =
      map (Algebra.linearMap R A) (Algebra.linearMap R B) := by
  ext
  simp only [AlgebraTensorModule.curry_apply, curry_apply, LinearMap.coe_restrictScalars, map_tmul,
    Algebra.linearMap_apply, map_one, LinearMap.coe_comp, Function.comp_apply,
    LinearMap.mul'_apply, mul_one, Algebra.TensorProduct.one_def]

Compatibility of Algebra Linear Map with Multiplication via Tensor Product

Informal description

The composition of the algebra linear map from $R$ to $A \otimes_R B$ with the multiplication linear map on $R$ is equal to the tensor product of the algebra linear maps from $R$ to $A$ and from $R$ to $B$. In symbols: \[ \text{Algebra.linearMap}_R (A \otimes_R B) \circ \text{LinearMap.mul}'_R R = \text{map} (\text{Algebra.linearMap}_R A) (\text{Algebra.linearMap}_R B) \]

TensorProduct.Algebra.mul'_comp_tensorTensorTensorComm theorem

: LinearMap.mul' R (A ⊗[R] B) ∘ₗ tensorTensorTensorComm R A A B B = map (LinearMap.mul' R A) (LinearMap.mul' R B)

Full source

@[simp]
theorem mul'_comp_tensorTensorTensorComm :
    LinearMap.mul'LinearMap.mul' R (A ⊗[R] B) ∘ₗ tensorTensorTensorComm R A A B B =
      map (LinearMap.mul' R A) (LinearMap.mul' R B) := by
  ext
  simp

Compatibility of multiplication with tensor tensor tensor commutation in $A \otimes_R B$

Informal description

Let $R$ be a commutative semiring and $A$, $B$ be $R$-algebras. The composition of the multiplication map on $A \otimes_R B$ with the tensor tensor tensor commutation map is equal to the tensor product of the multiplication maps on $A$ and $B$. In other words, the following diagram commutes: \[ \begin{CD} (A \otimes_R A) \otimes_R (B \otimes_R B) @>{\text{tensorTensorTensorComm}}>> (A \otimes_R B) \otimes_R (A \otimes_R B) \\ @V{\text{mul}'_A \otimes \text{mul}'_B}VV @VV{\text{mul}'_{A \otimes_R B}}V \\ A \otimes_R B @= A \otimes_R B \end{CD} \]

Submodule.map_range_rTensor_subtype_lid theorem

 {R Q} [CommSemiring R] [AddCommMonoid Q] [Module R Q] {I : Submodule R R} :
  (range <| rTensor Q I.subtype).map (TensorProduct.lid R Q) = I • ⊤

Full source

lemma Submodule.map_range_rTensor_subtype_lid {R Q} [CommSemiring R] [AddCommMonoid Q]
    [Module R Q] {I : Submodule R R} :
    (range <| rTensor Q I.subtype).map (TensorProduct.lid R Q) = I • ⊤ := by
  rw [← map_top, ← map_coe_toLinearMap, ← Submodule.map_comp, map_top]
  refine le_antisymm ?_ fun q h ↦ Submodule.smul_induction_on h
    (fun r hr q _ ↦ ⟨⟨r, hr⟩ ⊗ₜ q, by simp⟩) (by simp +contextual [add_mem])
  rintro _ ⟨t, rfl⟩
  exact t.induction_on (by simp) (by simp +contextual [Submodule.smul_mem_smul])
    (by simp +contextual [add_mem])

Image of Right Tensor Product with Submodule under LID Isomorphism Equals Scalar Multiplication

Informal description

Let $R$ be a commutative semiring, $Q$ an additive commutative monoid with an $R$-module structure, and $I$ a submodule of $R$. Then the image of the range of the right tensor product map $Q \otimes_R I \to Q \otimes_R R$ under the canonical isomorphism $Q \otimes_R R \cong Q$ is equal to the scalar multiplication of $I$ on the top submodule of $Q$, i.e., $I \cdot Q$.

TensorProduct.mk_surjective theorem

(h : Function.Surjective (algebraMap R S)) : Function.Surjective (TensorProduct.mk R S M 1)

Full source

theorem TensorProduct.mk_surjective (h : Function.Surjective (algebraMap R S)) :
    Function.Surjective (TensorProduct.mk R S M 1) := by
  rw [← LinearMap.range_eq_top, ← top_le_iff, ← span_tmul_eq_top, Submodule.span_le]
  rintro _ ⟨x, y, rfl⟩
  obtain ⟨x, rfl⟩ := h x
  rw [Algebra.algebraMap_eq_smul_one, smul_tmul]
  exact ⟨x • y, rfl⟩

Surjectivity of Tensor Product Map When Base Algebra Map is Surjective

Informal description

Let $R$ be a commutative semiring and $S$ an $R$-algebra. If the algebra map $R \to S$ is surjective, then for any $R$-module $M$, the tensor product map $S \times M \to S \otimes_R M$ defined by $(s, m) \mapsto s \otimes m$ is surjective when evaluated at $1 \in S$.

TensorProduct.flip_mk_surjective theorem

(h : Function.Surjective (algebraMap R T)) : Function.Surjective ((TensorProduct.mk R S T).flip 1)

Full source

lemma TensorProduct.flip_mk_surjective (h : Function.Surjective (algebraMap R T)) :
    Function.Surjective ((TensorProduct.mk R S T).flip 1) := by
  rw [← LinearMap.range_eq_top, ← top_le_iff, ← span_tmul_eq_top, Submodule.span_le]
  rintro _ ⟨s, t, rfl⟩
  obtain ⟨r, rfl⟩ := h t
  rw [Algebra.algebraMap_eq_smul_one, ← smul_tmul]
  exact ⟨r • s, rfl⟩

Surjectivity of Flipped Tensor Product Map when Base Algebra Map is Surjective

Informal description

Let $R$, $S$, and $T$ be commutative semirings with $R$-algebra structures. If the algebra map $R \to T$ is surjective, then for any $s \in S$, the flipped tensor product map $(x \mapsto s \otimes x) : T \to S \otimes_R T$ is surjective.

Algebra.TensorProduct.includeRight_surjective theorem

(h : Function.Surjective (algebraMap R S)) : Function.Surjective (includeRight : T →ₐ[R] S ⊗[R] T)

Full source

lemma Algebra.TensorProduct.includeRight_surjective (h : Function.Surjective (algebraMap R S)) :
    Function.Surjective (includeRight : T →ₐ[R] S ⊗[R] T) :=
  TensorProduct.mk_surjective _ _ _ h

Surjectivity of Right Inclusion in Tensor Product of Algebras

Informal description

Let $R$, $S$, and $T$ be commutative semirings where $S$ and $T$ are $R$-algebras. If the algebra homomorphism $R \to S$ is surjective, then the right inclusion map $\text{includeRight} : T \to S \otimes_R T$ is surjective as an $R$-algebra homomorphism.

Algebra.TensorProduct.includeLeft_surjective theorem

 (S A : Type*) [CommSemiring S] [Semiring A] [Algebra S A] [Algebra R A] [SMulCommClass R S A]
  (h : Function.Surjective (algebraMap R T)) : Function.Surjective (includeLeft : A →ₐ[S] A ⊗[R] T)

Full source

lemma Algebra.TensorProduct.includeLeft_surjective
    (S A : Type*) [CommSemiring S] [Semiring A] [Algebra S A] [Algebra R A]
    [SMulCommClass R S A] (h : Function.Surjective (algebraMap R T)) :
    Function.Surjective (includeLeft : A →ₐ[S] A ⊗[R] T) :=
  TensorProduct.flip_mk_surjective _ h

Surjectivity of Left Inclusion Map in Tensor Product of Algebras

Informal description

Let $R$, $S$, and $T$ be commutative semirings, where $A$ is an $S$-algebra and also an $R$-algebra with compatible scalar multiplication (i.e., $R$ and $S$ actions commute on $A$). If the algebra map from $R$ to $T$ is surjective, then the left inclusion map $\text{includeLeft} : A \to A \otimes_R T$ is surjective as an $S$-algebra homomorphism.

Mathlib.RingTheory.TensorProduct.Basic

Main declarations

References