Theorems · Definition · ring theory

Algebra.TensorProduct.tensorTensorTensorComm

(R : Type uR) →
  (R' : Type u_1) →
    (S : Type uS) →
      (T : Type u_2) →
        (A : Type uA) →
          (B : Type uB) →
            (C : Type uC) →
              (D : Type uD) →
                [inst : CommSemiring R] →
                  [inst_1 : CommSemiring S] →
                    [inst_2 : Algebra R S] →
                      [inst_3 : Semiring A] →
                        [inst_4 : Algebra R A] →
                          [inst_5 : Algebra S A] →
                            [IsScalarTower R S A] →
                              [inst_7 : Semiring B] →
                                [inst_8 : Algebra R B] →
                                  [inst_9 : Semiring C] →
                                    [inst_10 : Algebra R C] →
                                      [inst_11 : Algebra S C] →
                                        [inst_12 : IsScalarTower R S C] →
                                          [inst_13 : Semiring D] →
                                            [inst_14 : Algebra R D] →
                                              [inst_15 : CommSemiring T] →
                                                [inst_16 : Algebra R T] →
                                                  [inst_17 : Algebra T A] →
                                                    [IsScalarTower R T A] →
                                                      [inst_19 : SMulCommClass S T A] →
                                                        [inst_20 : Algebra S T] →
                                                          [IsScalarTower S T A] →
                                                            [inst_22 : CommSemiring R'] →
                                                              [inst_23 : Algebra R R'] →
                                                                [inst_24 : Algebra R' T] →
                                                                  [inst_25 : Algebra R' A] →
                                                                    [inst_26 : Algebra R' B] →
                                                                      [IsScalarTower R R' A] →
                                                                        [inst_28 : SMulCommClass S R' A] →
                                                                          [inst_29 : SMulCommClass R' S A] →
                                                                            [inst_30 : IsScalarTower R' T A] →
                                                                              [inst_31 : IsScalarTower R R' B] →
                                                                                TensorProduct S (TensorProduct R' A B)
                                                                                    (TensorProduct R C D) ≃ₐ[T]
                                                                                  TensorProduct R' (TensorProduct S A C)
                                                                                    (TensorProduct R B D)

Tensor product of algebras analogue of mul_mul_mul_comm. This is the algebra version of TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.

Defined in

Mathlib.RingTheory.TensorProduct.Maps

Cited by

8 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringCommSemiringAlgebraSemiringAlgebraAlgebraIsScalarTowerSemiringAlgebraSemiringAlgebraAlgebraIsScalarTowerSemiringAlgebraCommSemiringAlgebraAlgebraIsScalarTowerSMulCommClassAlgebraIsScalarTowerCommSemiringAlgebraAlgebraAlgebraAlgebraIsScalarTowerSMulCommClassSMulCommClassIsScalarTowerIsScalarTower