Graded tensor products over graded algebras

The graded tensor product $A \hat\otimes_R B$ is imbued with a multiplication defined on homogeneous tensors by:

$$(a \otimes b) \cdot (a' \otimes b') = (-1)^{\deg a' \deg b} (a \cdot a') \otimes (b \cdot b')$$

where $A$ and $B$ are algebras graded by ℕ, ℤ, or ZMod 2 (or more generally, any index that satisfies Module ι (Additive ℤˣ)).

The results for internally-graded algebras (via GradedAlgebra) are elsewhere, as is the type GradedTensorProduct.

Main results

• TensorProduct.gradedComm: the symmetric braiding operator on the tensor product of externally-graded rings.
• TensorProduct.gradedMul: the previously-described multiplication on externally-graded rings, as a bilinear map.

Implementation notes

Rather than implementing the multiplication directly as above, we first implement the canonical non-trivial braiding sending $a \otimes b$ to $(-1)^{\deg a' \deg b} (b \otimes a)$, as the multiplication follows trivially from this after some point-free nonsense.

References

• https://math.stackexchange.com/q/202718/1896
• [Algebra I, Bourbaki : Chapter III, §4.7, example (2)][bourbaki1989]

@[instance_reducible]

instance TensorProduct.instModuleFstSnd {R : Type u_1} {ι : Type u_2} (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] (i : ι × ι) : Module R (TensorProduct R (𝒜 i.1) (ℬ i.2))

Equations

• TensorProduct.instModuleFstSnd 𝒜 ℬ i = TensorProduct.leftModule

def TensorProduct.gradedCommAux (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] : (DirectSum (ι × ι) fun (i : ι × ι) => TensorProduct R (𝒜 i.1) (ℬ i.2)) →ₗ[R] DirectSum (ι × ι) fun (i : ι × ι) => TensorProduct R (ℬ i.1) (𝒜 i.2)

Auxiliary construction used to build TensorProduct.gradedComm.

This operates on direct sums of tensors instead of tensors of direct sums.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TensorProduct.gradedCommAux_lof_tmul (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] (i j : ι) (a : 𝒜 i) (b : ℬ j) : (gradedCommAux R 𝒜 ℬ) ((DirectSum.lof R (ι × ι) (fun (i : ι × ι) => TensorProduct R (𝒜 i.1) (ℬ i.2)) (i, j)) (a ⊗ₜ[R] b)) = (-1) ^ (j * i) • (DirectSum.lof R (ι × ι) (fun (i : ι × ι) => TensorProduct R (ℬ i.1) (𝒜 i.2)) (j, i)) (b ⊗ₜ[R] a)

@[simp]

theorem TensorProduct.gradedCommAux_comp_gradedCommAux (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] : gradedCommAux R 𝒜 ℬ ∘ₗ gradedCommAux R ℬ 𝒜 = LinearMap.id

def TensorProduct.gradedComm (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] : TensorProduct R (DirectSum ι fun (i : ι) => 𝒜 i) (DirectSum ι fun (i : ι) => ℬ i) ≃ₗ[R] TensorProduct R (DirectSum ι fun (i : ι) => ℬ i) (DirectSum ι fun (i : ι) => 𝒜 i)

The braiding operation for tensor products of externally ι-graded algebras.

This sends $a ⊗ b$ to $(-1)^{\deg a' \deg b} (b ⊗ a)$.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TensorProduct.gradedComm_symm (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] : (gradedComm R 𝒜 ℬ).symm = gradedComm R ℬ 𝒜

The braiding is symmetric.

theorem TensorProduct.gradedComm_of_tmul_of (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] (i j : ι) (a : 𝒜 i) (b : ℬ j) : (gradedComm R 𝒜 ℬ) ((DirectSum.lof R ι 𝒜 i) a ⊗ₜ[R] (DirectSum.lof R ι ℬ j) b) = (-1) ^ (j * i) • (DirectSum.lof R ι ℬ j) b ⊗ₜ[R] (DirectSum.lof R ι 𝒜 i) a

theorem TensorProduct.gradedComm_tmul_of_zero (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] (a : DirectSum ι fun (i : ι) => 𝒜 i) (b : ℬ 0) : (gradedComm R 𝒜 ℬ) (a ⊗ₜ[R] (DirectSum.lof R ι ℬ 0) b) = (DirectSum.lof R ι ℬ 0) b ⊗ₜ[R] a

theorem TensorProduct.gradedComm_of_zero_tmul (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] (a : 𝒜 0) (b : DirectSum ι fun (i : ι) => ℬ i) : (gradedComm R 𝒜 ℬ) ((DirectSum.lof R ι 𝒜 0) a ⊗ₜ[R] b) = b ⊗ₜ[R] (DirectSum.lof R ι 𝒜 0) a

theorem TensorProduct.gradedComm_tmul_one (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] [GradedMonoid.GOne ℬ] (a : DirectSum ι fun (i : ι) => 𝒜 i) : (gradedComm R 𝒜 ℬ) (a ⊗ₜ[R] 1) = 1 ⊗ₜ[R] a

theorem TensorProduct.gradedComm_one_tmul (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] [GradedMonoid.GOne 𝒜] (b : DirectSum ι fun (i : ι) => ℬ i) : (gradedComm R 𝒜 ℬ) (1 ⊗ₜ[R] b) = b ⊗ₜ[R] 1

@[simp]

theorem TensorProduct.gradedComm_one (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] [DirectSum.GSemiring 𝒜] [DirectSum.GSemiring ℬ] : (gradedComm R 𝒜 ℬ) 1 = 1

theorem TensorProduct.gradedComm_tmul_algebraMap (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] [DirectSum.GSemiring ℬ] [DirectSum.GAlgebra R ℬ] (a : DirectSum ι fun (i : ι) => 𝒜 i) (r : R) : (gradedComm R 𝒜 ℬ) (a ⊗ₜ[R] (algebraMap R (DirectSum ι fun (i : ι) => ℬ i)) r) = (algebraMap R (DirectSum ι fun (i : ι) => ℬ i)) r ⊗ₜ[R] a

theorem TensorProduct.gradedComm_algebraMap_tmul (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] [DirectSum.GSemiring 𝒜] [DirectSum.GAlgebra R 𝒜] (r : R) (b : DirectSum ι fun (i : ι) => ℬ i) : (gradedComm R 𝒜 ℬ) ((algebraMap R (DirectSum ι fun (i : ι) => 𝒜 i)) r ⊗ₜ[R] b) = b ⊗ₜ[R] (algebraMap R (DirectSum ι fun (i : ι) => 𝒜 i)) r

theorem TensorProduct.gradedComm_algebraMap (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] [DirectSum.GSemiring 𝒜] [DirectSum.GSemiring ℬ] [DirectSum.GAlgebra R 𝒜] [DirectSum.GAlgebra R ℬ] (r : R) : (gradedComm R 𝒜 ℬ) ((algebraMap R (TensorProduct R (DirectSum ι fun (i : ι) => 𝒜 i) (DirectSum ι fun (i : ι) => ℬ i))) r) = (algebraMap R (TensorProduct R (DirectSum ι fun (i : ι) => ℬ i) (DirectSum ι fun (i : ι) => 𝒜 i))) r

theorem TensorProduct.gradedMul_def (R : Type u_5) {ι : Type u_6} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_7) (ℬ : ι → Type u_8) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] [DirectSum.GRing 𝒜] [DirectSum.GRing ℬ] [DirectSum.GAlgebra R 𝒜] [DirectSum.GAlgebra R ℬ] : gradedMul R 𝒜 ℬ = curry (map (LinearMap.mul' R (DirectSum ι fun (i : ι) => 𝒜 i)) (LinearMap.mul' R (DirectSum ι fun (i : ι) => ℬ i)) ∘ₗ ↑(TensorProduct.assoc R (DirectSum ι fun (i : ι) => 𝒜 i) (DirectSum ι fun (i : ι) => 𝒜 i) (TensorProduct R (DirectSum ι fun (i : ι) => ℬ i) (DirectSum ι fun (i : ι) => ℬ i))).symm ∘ₗ LinearMap.lTensor (DirectSum ι fun (i : ι) => 𝒜 i) (↑(TensorProduct.assoc R (DirectSum ι fun (i : ι) => 𝒜 i) (DirectSum ι fun (i : ι) => ℬ i) (DirectSum ι fun (i : ι) => ℬ i)) ∘ₗ LinearMap.rTensor (DirectSum ι fun (i : ι) => ℬ i) ↑(gradedComm R ℬ 𝒜) ∘ₗ ↑(TensorProduct.assoc R (DirectSum ι ℬ) (DirectSum ι 𝒜) (DirectSum ι ℬ)).symm) ∘ₗ ↑(TensorProduct.assoc R (DirectSum ι 𝒜) (DirectSum ι ℬ) (TensorProduct R (DirectSum ι 𝒜) (DirectSum ι ℬ))))

@[irreducible]

noncomputable def TensorProduct.gradedMul (R : Type u_5) {ι : Type u_6} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_7) (ℬ : ι → Type u_8) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] [DirectSum.GRing 𝒜] [DirectSum.GRing ℬ] [DirectSum.GAlgebra R 𝒜] [DirectSum.GAlgebra R ℬ] : TensorProduct R (DirectSum ι 𝒜) (DirectSum ι ℬ) →ₗ[R] TensorProduct R (DirectSum ι 𝒜) (DirectSum ι ℬ) →ₗ[R] TensorProduct R (DirectSum ι 𝒜) (DirectSum ι ℬ)

The multiplication operation for tensor products of externally ι-graded algebras.

Equations

• One or more equations did not get rendered due to their size.

theorem TensorProduct.tmul_of_gradedMul_of_tmul (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] [DirectSum.GRing 𝒜] [DirectSum.GRing ℬ] [DirectSum.GAlgebra R 𝒜] [DirectSum.GAlgebra R ℬ] (j₁ i₂ : ι) (a₁ : DirectSum ι fun (i : ι) => 𝒜 i) (b₁ : ℬ j₁) (a₂ : 𝒜 i₂) (b₂ : DirectSum ι fun (i : ι) => ℬ i) : ((gradedMul R 𝒜 ℬ) (a₁ ⊗ₜ[R] (DirectSum.lof R ι ℬ j₁) b₁)) ((DirectSum.lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] b₂) = (-1) ^ (j₁ * i₂) • (a₁ * (DirectSum.lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((DirectSum.lof R ι ℬ j₁) b₁ * b₂)

theorem TensorProduct.algebraMap_gradedMul {R : Type u_1} {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] [DirectSum.GRing 𝒜] [DirectSum.GRing ℬ] [DirectSum.GAlgebra R 𝒜] [DirectSum.GAlgebra R ℬ] (r : R) (x : TensorProduct R (DirectSum ι fun (i : ι) => 𝒜 i) (DirectSum ι fun (i : ι) => ℬ i)) : ((gradedMul R 𝒜 ℬ) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1)) x = r • x

theorem TensorProduct.one_gradedMul {R : Type u_1} {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] [DirectSum.GRing 𝒜] [DirectSum.GRing ℬ] [DirectSum.GAlgebra R 𝒜] [DirectSum.GAlgebra R ℬ] (x : TensorProduct R (DirectSum ι fun (i : ι) => 𝒜 i) (DirectSum ι fun (i : ι) => ℬ i)) : ((gradedMul R 𝒜 ℬ) 1) x = x

theorem TensorProduct.gradedMul_algebraMap {R : Type u_1} {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] [DirectSum.GRing 𝒜] [DirectSum.GRing ℬ] [DirectSum.GAlgebra R 𝒜] [DirectSum.GAlgebra R ℬ] (x : TensorProduct R (DirectSum ι fun (i : ι) => 𝒜 i) (DirectSum ι fun (i : ι) => ℬ i)) (r : R) : ((gradedMul R 𝒜 ℬ) x) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1) = r • x

theorem TensorProduct.gradedMul_one {R : Type u_1} {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] [DirectSum.GRing 𝒜] [DirectSum.GRing ℬ] [DirectSum.GAlgebra R 𝒜] [DirectSum.GAlgebra R ℬ] (x : TensorProduct R (DirectSum ι fun (i : ι) => 𝒜 i) (DirectSum ι fun (i : ι) => ℬ i)) : ((gradedMul R 𝒜 ℬ) x) 1 = x

theorem TensorProduct.gradedMul_assoc {R : Type u_1} {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] [DirectSum.GRing 𝒜] [DirectSum.GRing ℬ] [DirectSum.GAlgebra R 𝒜] [DirectSum.GAlgebra R ℬ] (x y z : TensorProduct R (DirectSum ι 𝒜) (DirectSum ι ℬ)) : ((gradedMul R 𝒜 ℬ) (((gradedMul R 𝒜 ℬ) x) y)) z = ((gradedMul R 𝒜 ℬ) x) (((gradedMul R 𝒜 ℬ) y) z)

theorem TensorProduct.gradedComm_gradedMul {R : Type u_1} {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] [DirectSum.GRing 𝒜] [DirectSum.GRing ℬ] [DirectSum.GAlgebra R 𝒜] [DirectSum.GAlgebra R ℬ] (x y : TensorProduct R (DirectSum ι 𝒜) (DirectSum ι ℬ)) : (gradedComm R 𝒜 ℬ) (((gradedMul R 𝒜 ℬ) x) y) = ((gradedMul R ℬ 𝒜) ((gradedComm R 𝒜 ℬ) x)) ((gradedComm R 𝒜 ℬ) y)