Documentation

Mathlib.LinearAlgebra.TensorProduct.Graded.External

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 #

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 #

noncomputable instance TensorProduct.instModuleFstSnd {R : Type u_1} {ι : Type u_2} (𝒜 : ιType u_5) (ℬ : ιType u_6) [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
noncomputable def TensorProduct.gradedCommAux (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] (𝒜 : ιType u_5) (ℬ : ιType u_6) [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)

Auxliary 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.
Instances For
    @[simp]
    theorem TensorProduct.gradedCommAux_lof_tmul (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] (𝒜 : ιType u_5) (ℬ : ιType u_6) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup ( i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R ( i)] (i : ι) (j : ι) (a : 𝒜 i) (b : j) :
    (TensorProduct.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_5) (ℬ : ιType u_6) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup ( i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R ( i)] :
    TensorProduct.gradedCommAux R 𝒜 ∘ₗ TensorProduct.gradedCommAux R 𝒜 = LinearMap.id
    noncomputable def TensorProduct.gradedComm (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] (𝒜 : ιType u_5) (ℬ : ιType u_6) [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.
    Instances For
      @[simp]
      theorem TensorProduct.gradedComm_symm (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] (𝒜 : ιType u_5) (ℬ : ιType u_6) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup ( i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R ( i)] :

      The braiding is symmetric.

      theorem TensorProduct.gradedComm_of_tmul_of (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] (𝒜 : ιType u_5) (ℬ : ιType u_6) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup ( i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R ( i)] (i : ι) (j : ι) (a : 𝒜 i) (b : j) :
      (TensorProduct.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_5) (ℬ : ιType u_6) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup ( i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R ( i)] (a : DirectSum ι fun (i : ι) => 𝒜 i) (b : 0) :
      (TensorProduct.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_5) (ℬ : ιType u_6) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup ( i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R ( i)] (a : 𝒜 0) (b : DirectSum ι fun (i : ι) => i) :
      (TensorProduct.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_5) (ℬ : ιType u_6) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup ( i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R ( i)] [DirectSum.GRing ] (a : DirectSum ι fun (i : ι) => 𝒜 i) :
      (TensorProduct.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_5) (ℬ : ιType u_6) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup ( i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R ( i)] [DirectSum.GRing 𝒜] (b : DirectSum ι fun (i : ι) => i) :
      (TensorProduct.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_5) (ℬ : ιType u_6) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup ( i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R ( i)] [DirectSum.GRing 𝒜] [DirectSum.GRing ] :
      (TensorProduct.gradedComm R 𝒜 ) 1 = 1
      theorem TensorProduct.gradedComm_tmul_algebraMap (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] (𝒜 : ιType u_5) (ℬ : ιType u_6) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup ( i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R ( i)] [DirectSum.GRing ] [DirectSum.GAlgebra R ] (a : DirectSum ι fun (i : ι) => 𝒜 i) (r : R) :
      (TensorProduct.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_5) (ℬ : ιType u_6) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup ( i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R ( i)] [DirectSum.GRing 𝒜] [DirectSum.GAlgebra R 𝒜] (r : R) (b : DirectSum ι fun (i : ι) => i) :
      (TensorProduct.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_5) (ℬ : ιType u_6) [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) :
      (TensorProduct.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
      @[irreducible]
      noncomputable def TensorProduct.gradedMul (R : Type u_7) {ι : Type u_8} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] (𝒜 : ιType u_9) (ℬ : ιType u_10) [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
      Instances For
        theorem TensorProduct.gradedMul_def (R : Type u_7) {ι : Type u_8} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] (𝒜 : ιType u_9) (ℬ : ιType u_10) [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.gradedMul R 𝒜 = TensorProduct.curry (TensorProduct.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) (TensorProduct.gradedComm R 𝒜) ∘ₗ (TensorProduct.assoc R (DirectSum ι ) (DirectSum ι 𝒜) (DirectSum ι )).symm) ∘ₗ (TensorProduct.assoc R (DirectSum ι 𝒜) (DirectSum ι ) (TensorProduct R (DirectSum ι 𝒜) (DirectSum ι ))))
        theorem TensorProduct.tmul_of_gradedMul_of_tmul (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] (𝒜 : ιType u_5) (ℬ : ιType u_6) [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) :
        ((TensorProduct.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_5) (ℬ : ιType u_6) [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)) :
        ((TensorProduct.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_5) (ℬ : ιType u_6) [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)) :
        ((TensorProduct.gradedMul R 𝒜 ) 1) x = x
        theorem TensorProduct.gradedMul_algebraMap {R : Type u_1} {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] (𝒜 : ιType u_5) (ℬ : ιType u_6) [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) :
        ((TensorProduct.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_5) (ℬ : ιType u_6) [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)) :
        ((TensorProduct.gradedMul R 𝒜 ) x) 1 = x
        theorem TensorProduct.gradedMul_assoc {R : Type u_1} {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] (𝒜 : ιType u_5) (ℬ : ιType u_6) [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 ι 𝒜) (DirectSum ι )) (y : TensorProduct R (DirectSum ι 𝒜) (DirectSum ι )) (z : TensorProduct R (DirectSum ι 𝒜) (DirectSum ι )) :
        ((TensorProduct.gradedMul R 𝒜 ) (((TensorProduct.gradedMul R 𝒜 ) x) y)) z = ((TensorProduct.gradedMul R 𝒜 ) x) (((TensorProduct.gradedMul R 𝒜 ) y) z)
        theorem TensorProduct.gradedComm_gradedMul {R : Type u_1} {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] (𝒜 : ιType u_5) (ℬ : ιType u_6) [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 ι 𝒜) (DirectSum ι )) (y : TensorProduct R (DirectSum ι 𝒜) (DirectSum ι )) :
        (TensorProduct.gradedComm R 𝒜 ) (((TensorProduct.gradedMul R 𝒜 ) x) y) = ((TensorProduct.gradedMul R 𝒜) ((TensorProduct.gradedComm R 𝒜 ) x)) ((TensorProduct.gradedComm R 𝒜 ) y)