Theorems · Definition · ring theory

Coalgebra.TensorProduct.map

{R : Type u_5} →
  {S : Type u_6} →
    {M : Type u_7} →
      {N : Type u_8} →
        {P : Type u_9} →
          {Q : Type u_10} →
            [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 : AddCommMonoid Q] →
                          [inst_7 : Module R M] →
                            [inst_8 : Module R N] →
                              [inst_9 : Module R P] →
                                [inst_10 : Module R Q] →
                                  [inst_11 : Module S M] →
                                    [inst_12 : IsScalarTower R S M] →
                                      [inst_13 : Coalgebra S M] →
                                        [inst_14 : Module S N] →
                                          [inst_15 : IsScalarTower R S N] →
                                            [inst_16 : Coalgebra S N] →
                                              [inst_17 : Coalgebra R P] →
                                                [inst_18 : Coalgebra R Q] →
                                                  (M →ₗc[S] N) →
                                                    (P →ₗc[R] Q) → TensorProduct R M P →ₗc[S] TensorProduct R N Q

The tensor product of two coalgebra morphisms as a coalgebra morphism.

Defined in

Mathlib.RingTheory.Coalgebra.TensorProduct

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraAddCommMonoidAddCommMonoidAddCommMonoidAddCommMonoidModuleModuleModuleModuleModuleIsScalarTowerCoalgebraModuleIsScalarTowerCoalgebraCoalgebraCoalgebra