Theorems · Definition · ring theory

TensorProduct.gradedComm

(R : Type u_1) →
  {ι : Type u_2} →
    [inst : CommSemiring ι] →
      [Module ι (Additive ℤˣ)] →
        [DecidableEq ι] →
          (𝒜 : ι → Type u_3) →
            (ℬ : ι → Type u_4) →
              [inst : CommRing R] →
                [inst_1 : (i : ι) → AddCommGroup (𝒜 i)] →
                  [inst_2 : (i : ι) → AddCommGroup (ℬ i)] →
                    [inst_3 : (i : ι) → Module R (𝒜 i)] →
                      [inst_4 : (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)$.

Defined in

Mathlib.LinearAlgebra.TensorProduct.Graded.External

Cited by

15 results in Mathlib

Foundations

Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringModuleDecidableEqCommRingAddCommGroupAddCommGroupModuleModule