Theorems · Inductive type · nonassociative algebras

LieModuleHom

(R : Type u) →
  (L : Type v) →
    (M : Type w) →
      (N : Type w₁) →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [Module R M] → [Module R N] → [LieRingModule L M] → [LieRingModule L N] → Type (max w w₁)

A morphism of Lie algebra modules (denoted as M →ₗ⁅R,L⁆ N) is a linear map which commutes with the action of the Lie algebra.

Defined in

Mathlib.Algebra.Lie.Basic

Cited by

123 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 41 definitions · uses no axioms

Assumes

CommRingLieRingAddCommGroupAddCommGroupModuleModuleLieRingModuleLieRingModule