Theorems · Definition · nonassociative algebras

TensorProduct.LieModule.liftLie

(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,L⁆ N →ₗ[R] P) ≃ₗ[R] TensorProduct R M N →ₗ⁅R,L⁆ P

A weaker form of the universal property for tensor product of modules of a Lie algebra. Note that maps f of type M →ₗ⁅R,L⁆ N →ₗ[R] P are exactly those R-bilinear maps satisfying ⁅x, f m n⁆ = f ⁅x, m⁆ n + f m ⁅x, n⁆ for all x, m, n (see e.g, LieModuleHom.map_lie₂).

Defined in

Mathlib.Algebra.Lie.TensorProduct

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingLieRingLieAlgebraAddCommGroupModuleLieRingModuleLieModuleAddCommGroupModuleLieRingModuleLieModuleAddCommGroupModuleLieRingModuleLieModule