Theorems · Definition · nonassociative algebras

AlgHom.toLieHom

{A : Type v} →
  [inst : Ring A] →
    {R : Type u} →
      [inst_1 : CommRing R] →
        [inst_2 : Algebra R A] → {B : Type w} → [inst_3 : Ring B] → [inst_4 : Algebra R B] → (A →ₐ[R] B) → A →ₗ⁅R⁆ B

The map ofAssociativeAlgebra associating a Lie algebra to an associative algebra is functorial.

Defined in

Mathlib.Algebra.Lie.OfAssociative

Cited by

8 results in Mathlib

Foundations

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

Assumes

RingCommRingAlgebraRingAlgebra