Theorems · Definition · ring theory

Coalgebra.TensorProduct.assoc

(R : Type u_5) →
  (S : Type u_6) →
    (M : Type u_7) →
      (N : Type u_8) →
        (P : Type u_9) →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring S] →
              [inst_2 : Algebra R S] →
                [inst_3 : AddCommMonoid M] →
                  [inst_4 : AddCommMonoid N] →
                    [inst_5 : AddCommMonoid P] →
                      [inst_6 : Module R M] →
                        [inst_7 : Module R N] →
                          [inst_8 : Module R P] →
                            [inst_9 : Module S M] →
                              [inst_10 : IsScalarTower R S M] →
                                [inst_11 : Coalgebra S M] →
                                  [inst_12 : Module S N] →
                                    [inst_13 : IsScalarTower R S N] →
                                      [inst_14 : Coalgebra S N] →
                                        [inst_15 : Coalgebra R P] →
                                          TensorProduct R (TensorProduct S M N) P ≃ₗc[S]
                                            TensorProduct S M (TensorProduct R N P)

The associator for tensor products of R-coalgebras, as a coalgebra equivalence.

Defined in

Mathlib.RingTheory.Coalgebra.TensorProduct

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraAddCommMonoidAddCommMonoidAddCommMonoidModuleModuleModuleModuleIsScalarTowerCoalgebraModuleIsScalarTowerCoalgebraCoalgebra