Theorems · Definition · nonassociative algebras

TensorProduct.LieModule.lift

(R : Type u) →
  [inst : CommRing R] →
    (L : Type v) →
      (M : Type w) →
        (N : Type w₁) →
          (P : Type w₂) →
            [inst_1 : LieRing L] →
              [inst_2 : LieAlgebra R L] →
                [inst_3 : AddCommGroup M] →
                  [inst_4 : Module R M] →
                    [inst_5 : LieRingModule L M] →
                      [inst_6 : LieModule R L M] →
                        [inst_7 : AddCommGroup N] →
                          [inst_8 : Module R N] →
                            [inst_9 : LieRingModule L N] →
                              [inst_10 : LieModule R L N] →
                                [inst_11 : AddCommGroup P] →
                                  [inst_12 : Module R P] →
                                    [inst_13 : LieRingModule L P] →
                                      [inst_14 : LieModule R L P] →
                                        (M →ₗ[R] N →ₗ[R] P) ≃ₗ⁅R,L⁆ TensorProduct R M N →ₗ[R] P

The universal property for tensor product of modules of a Lie algebra: the R-linear tensor-hom adjunction is equivariant with respect to the L action.

Defined in

Mathlib.Algebra.Lie.TensorProduct

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingLieRingLieAlgebraAddCommGroupModuleLieRingModuleLieModuleAddCommGroupModuleLieRingModuleLieModuleAddCommGroupModuleLieRingModuleLieModule