Theorems · Inductive type · nonassociative algebras

LieEquiv

(R : Type u) →
  (L : Type v) →
    (L' : Type w) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] → [LieAlgebra R L] → [inst_3 : LieRing L'] → [LieAlgebra R L'] → Type (max v w)

An equivalence of Lie algebras (denoted as L₁ ≃ₗ⁅R⁆ L₂) is a morphism which is also a linear equivalence. We could instead define an equivalence to be a morphism which is also a (plain) equivalence. However, it is more convenient to define via linear equivalence to get .toLinearEquiv for free.

Defined in

Mathlib.Algebra.Lie.Basic

Cited by

86 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CommRingLieRingLieAlgebraLieRingLieAlgebra