Theorems · Definition · linear algebra

TensorProduct.liftAddHom

{R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_7} →
      {N : Type u_8} →
        {P : Type u_9} →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid N] →
              [inst_3 : AddCommMonoid P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    (f : M →+ N →+ P) →
                      (∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)) → TensorProduct R M N →+ P

Lift an R-balanced map to the tensor product. A map f : M →+ N →+ P additive in both components is R-balanced, or middle linear with respect to R, if scalar multiplication in either argument is equivalent, f (r • m) n = f m (r • n). Note that strictly the first action should be a right-action by R, but for now R is commutative so it doesn't matter.

Defined in

Mathlib.LinearAlgebra.TensorProduct.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidAddCommMonoidAddCommMonoidModuleModule