Lie algebras

This file defines Lie rings and Lie algebras over a commutative ring together with their modules, morphisms and equivalences, as well as various lemmas to make these definitions usable.

Main definitions

• LieRing
• LieAlgebra
• LieRingModule
• LieModule
• LieHom
• LieEquiv
• LieModuleHom
• LieModuleEquiv

Notation

Working over a fixed commutative ring R, we introduce the notations:

• L →ₗ⁅R⁆ L' for a morphism of Lie algebras,
• L ≃ₗ⁅R⁆ L' for an equivalence of Lie algebras,
• M →ₗ⁅R,L⁆ N for a morphism of Lie algebra modules M, N over a Lie algebra L,
• M ≃ₗ⁅R,L⁆ N for an equivalence of Lie algebra modules M, N over a Lie algebra L.

Implementation notes

Lie algebras are defined as modules with a compatible Lie ring structure and thus, like modules, are partially unbundled.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 1--3

Tagsc

lie bracket, jacobi identity, lie ring, lie algebra, lie module

class LieRing (L : Type v) extends AddCommGroup , Bracket : Type v

• add : L → L → L
• add_assoc : ∀ (a b c : L), a + b + c = a + (b + c)
• zero : L
• zero_add : ∀ (a : L), 0 + a = a
• add_zero : ∀ (a : L), a + 0 = a
• nsmul : ℕ → L → L
• nsmul_zero : ∀ (x : L), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : L), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x
• neg : L → L
• sub : L → L → L
• sub_eq_add_neg : ∀ (a b : L), a - b = a + -b
• zsmul : ℤ → L → L
• zsmul_zero' : ∀ (a : L), SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' : ∀ (n : ℕ) (a : L), SubNegMonoid.zsmul (Int.ofNat (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : L), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) a
• add_left_neg : ∀ (a : L), -a + a = 0
• add_comm : ∀ (a b : L), a + b = b + a
• bracket : L → L → L
• add_lie : ∀ (x y z : L), ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆

  A Lie ring bracket is additive in its first component.

• lie_add : ∀ (x y z : L), ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆

  A Lie ring bracket is additive in its second component.

• lie_self : ∀ (x : L), ⁅x, x⁆ = 0

  A Lie ring bracket vanishes on the diagonal in L × L.

• leibniz_lie : ∀ (x y z : L), ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆

  A Lie ring bracket satisfies a Leibniz / Jacobi identity.

A Lie ring is an additive group with compatible product, known as the bracket, satisfying the Jacobi identity.

class LieAlgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] extends Module : Type (max u v)

• smul : R → L → L
• one_smul : ∀ (b : L), 1 • b = b
• mul_smul : ∀ (x y : R) (b : L), (x * y) • b = x • y • b
• smul_zero : ∀ (a : R), a • 0 = 0
• smul_add : ∀ (a : R) (x y : L), a • (x + y) = a • x + a • y
• add_smul : ∀ (r s_1 : R) (x : L), (r + s_1) • x = r • x + s_1 • x
• zero_smul : ∀ (x : L), 0 • x = 0
• lie_smul : ∀ (t : R) (x y : L), ⁅x, t • y⁆ = t • ⁅x, y⁆

  A Lie algebra bracket is compatible with scalar multiplication in its second argument.

  The compatibility in the first argument is not a class property, but follows since every Lie algebra has a natural Lie module action on itself, see LieModule.

A Lie algebra is a module with compatible product, known as the bracket, satisfying the Jacobi identity. Forgetting the scalar multiplication, every Lie algebra is a Lie ring.

class LieRingModule (L : Type v) (M : Type w) [LieRing L] [AddCommGroup M] extends Bracket : Type (max v w)

• bracket : L → M → M
• add_lie : ∀ (x y : L) (m : M), ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆

  A Lie ring module bracket is additive in its first component.

• lie_add : ∀ (x : L) (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆

  A Lie ring module bracket is additive in its second component.

• leibniz_lie : ∀ (x y : L) (m : M), ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆

  A Lie ring module bracket satisfies a Leibniz / Jacobi identity.

A Lie ring module is an additive group, together with an additive action of a Lie ring on this group, such that the Lie bracket acts as the commutator of endomorphisms. (For representations of Lie algebras see LieModule.)

class LieModule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Prop

• smul_lie : ∀ (t : R) (x : L) (m : M), ⁅t • x, m⁆ = t • ⁅x, m⁆

  A Lie module bracket is compatible with scalar multiplication in its first argument.

• lie_smul : ∀ (t : R) (x : L) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆

  A Lie module bracket is compatible with scalar multiplication in its second argument.

A Lie module is a module over a commutative ring, together with a linear action of a Lie algebra on this module, such that the Lie bracket acts as the commutator of endomorphisms.

@[simp]

theorem add_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (y : L) (m : M) : ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆

@[simp]

theorem lie_add {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) (n : M) : ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆

@[simp]

theorem smul_lie {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (t : R) (x : L) (m : M) : ⁅t • x, m⁆ = t • ⁅x, m⁆

@[simp]

theorem lie_smul {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (t : R) (x : L) (m : M) : ⁅x, t • m⁆ = t • ⁅x, m⁆

theorem leibniz_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (y : L) (m : M) : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆

@[simp]

theorem lie_zero {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) : ⁅x, 0⁆ = 0

@[simp]

theorem zero_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (m : M) : ⁅0, m⁆ = 0

@[simp]

theorem lie_self {L : Type v} [LieRing L] (x : L) : ⁅x, x⁆ = 0

instance lieRingSelfModule {L : Type v} [LieRing L] : LieRingModule L L

@[simp]

theorem lie_skew {L : Type v} [LieRing L] (x : L) (y : L) : -⁅y, x⁆ = ⁅x, y⁆

instance lieAlgebraSelfModule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : LieModule R L L

Every Lie algebra is a module over itself.

@[simp]

theorem neg_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) : ⁅-x, m⁆ = -⁅x, m⁆

@[simp]

theorem lie_neg {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) : ⁅x, -m⁆ = -⁅x, m⁆

@[simp]

theorem sub_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (y : L) (m : M) : ⁅x - y, m⁆ = ⁅x, m⁆ - ⁅y, m⁆

@[simp]

theorem lie_sub {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) (n : M) : ⁅x, m - n⁆ = ⁅x, m⁆ - ⁅x, n⁆

@[simp]

theorem nsmul_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) (n : ℕ) : ⁅n • x, m⁆ = n • ⁅x, m⁆

@[simp]

theorem lie_nsmul {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) (n : ℕ) : ⁅x, n • m⁆ = n • ⁅x, m⁆

@[simp]

theorem zsmul_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) (a : ℤ) : ⁅a • x, m⁆ = a • ⁅x, m⁆

@[simp]

theorem lie_zsmul {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) (a : ℤ) : ⁅x, a • m⁆ = a • ⁅x, m⁆

@[simp]

theorem lie_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (y : L) (m : M) : ⁅⁅x, y⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆

theorem lie_jacobi {L : Type v} [LieRing L] (x : L) (y : L) (z : L) : ⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, ⁅x, y⁆⁆ = 0

instance LieRing.intLieAlgebra {L : Type v} [LieRing L] : LieAlgebra ℤ L

instance instLieRingModuleLinearMapToSemiringToCommSemiringIdToNonAssocSemiringToAddCommMonoidToAddCommMonoidAddCommGroup {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] : LieRingModule L (M →ₗ[R] N)

@[simp]

theorem LieHom.lie_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (f : M →ₗ[R] N) (x : L) (m : M) : ↑⁅x, f⁆ m = ⁅x, ↑f m⁆ - ↑f ⁅x, m⁆

instance instLieModuleLinearMapToSemiringToCommSemiringIdToNonAssocSemiringToAddCommMonoidToAddCommMonoidAddCommGroupModuleSmulCommClass_selfToCommMonoidToMulActionToMonoidWithZeroToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToMulActionWithZeroInstLieRingModuleLinearMapToSemiringToCommSemiringIdToNonAssocSemiringToAddCommMonoidToAddCommMonoidAddCommGroup {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] : LieModule R L (M →ₗ[R] N)

structure LieHom (R : Type u_1) (L : Type u_2) (L' : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] extends LinearMap : Type (max u_2 u_3)

• toFun : L → L'
• map_add' : ∀ (x y : L), AddHom.toFun s.toAddHom (x + y) = AddHom.toFun s.toAddHom x + AddHom.toFun s.toAddHom y
• map_smul' : ∀ (r : R) (x : L), AddHom.toFun s.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun s.toAddHom x
• map_lie' : ∀ {x y : L}, AddHom.toFun s.toAddHom ⁅x, y⁆ = ⁅AddHom.toFun s.toAddHom x, AddHom.toFun s.toAddHom y⁆

  A morphism of Lie algebras is compatible with brackets.

A morphism of Lie algebras is a linear map respecting the bracket operations.

def «term_→ₗ⁅_⁆_» : Lean.TrailingParserDescr

A morphism of Lie algebras is a linear map respecting the bracket operations.

instance LieHom.instCoeLieHomLinearMapToSemiringToCommSemiringIdToNonAssocSemiringToAddCommMonoidToAddCommGroupToAddCommMonoidToAddCommGroupToModuleToModule {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] : Coe (L₁ →ₗ⁅R⁆ L₂) (L₁ →ₗ[R] L₂)

instance LieHom.instFunLikeLieHom {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] : FunLike (L₁ →ₗ⁅R⁆ L₂) L₁ fun x => L₂

@[simp]

theorem LieHom.coe_toLinearMap {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) : ↑↑f = ↑f

@[simp]

theorem LieHom.toFun_eq_coe {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) : f.toFun = ↑f

@[simp]

theorem LieHom.map_smul {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (c : R) (x : L₁) : ↑f (c • x) = c • ↑f x

@[simp]

theorem LieHom.map_add {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (x : L₁) (y : L₁) : ↑f (x + y) = ↑f x + ↑f y

@[simp]

theorem LieHom.map_sub {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (x : L₁) (y : L₁) : ↑f (x - y) = ↑f x - ↑f y

@[simp]

theorem LieHom.map_neg {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (x : L₁) : ↑f (-x) = -↑f x

@[simp]

theorem LieHom.map_lie {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (x : L₁) (y : L₁) : ↑f ⁅x, y⁆ = ⁅↑f x, ↑f y⁆

@[simp]

theorem LieHom.map_zero {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) : ↑f 0 = 0

def LieHom.id {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] : L₁ →ₗ⁅R⁆ L₁

The identity map is a morphism of Lie algebras.

@[simp]

theorem LieHom.coe_id {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] : ↑LieHom.id = id

theorem LieHom.id_apply {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] (x : L₁) : ↑LieHom.id x = x

instance LieHom.instZeroLieHom {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] : Zero (L₁ →ₗ⁅R⁆ L₂)

The constant 0 map is a Lie algebra morphism.

@[simp]

theorem LieHom.coe_zero {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] : ↑0 = 0

theorem LieHom.zero_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (x : L₁) : ↑0 x = 0

instance LieHom.instOneLieHom {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] : One (L₁ →ₗ⁅R⁆ L₁)

The identity map is a Lie algebra morphism.

@[simp]

theorem LieHom.coe_one {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] : ↑1 = id

theorem LieHom.one_apply {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] (x : L₁) : ↑1 x = x

instance LieHom.instInhabitedLieHom {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] : Inhabited (L₁ →ₗ⁅R⁆ L₂)

theorem LieHom.coe_injective {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] : Function.Injective FunLike.coe

theorem LieHom.ext {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] {f : L₁ →ₗ⁅R⁆ L₂} {g : L₁ →ₗ⁅R⁆ L₂} (h : ∀ (x : L₁), ↑f x = ↑g x) : f = g

theorem LieHom.ext_iff {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] {f : L₁ →ₗ⁅R⁆ L₂} {g : L₁ →ₗ⁅R⁆ L₂} : f = g ↔ ∀ (x : L₁), ↑f x = ↑g x

theorem LieHom.congr_fun {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] {f : L₁ →ₗ⁅R⁆ L₂} {g : L₁ →ₗ⁅R⁆ L₂} (h : f = g) (x : L₁) : ↑f x = ↑g x

@[simp]

theorem LieHom.mk_coe {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (h₁ : ∀ (x y : L₁), ↑f (x + y) = ↑f x + ↑f y) (h₂ : ∀ (r : R) (x : L₁), AddHom.toFun { toFun := ↑f, map_add' := h₁ } (r • x) = ↑(RingHom.id R) r • AddHom.toFun { toFun := ↑f, map_add' := h₁ } x) (h₃ : ∀ {x y : L₁}, AddHom.toFun { toAddHom := { toFun := ↑f, map_add' := h₁ }, map_smul' := h₂ }.toAddHom ⁅x, y⁆ = ⁅AddHom.toFun { toAddHom := { toFun := ↑f, map_add' := h₁ }, map_smul' := h₂ }.toAddHom x, AddHom.toFun { toAddHom := { toFun := ↑f, map_add' := h₁ }, map_smul' := h₂ }.toAddHom y⁆) : { toLinearMap := { toAddHom := { toFun := ↑f, map_add' := h₁ }, map_smul' := h₂ }, map_lie' := h₃ } = f

@[simp]

theorem LieHom.coe_mk {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ → L₂) (h₁ : ∀ (x y : L₁), f (x + y) = f x + f y) (h₂ : ∀ (r : R) (x : L₁), AddHom.toFun { toFun := f, map_add' := h₁ } (r • x) = ↑(RingHom.id R) r • AddHom.toFun { toFun := f, map_add' := h₁ } x) (h₃ : ∀ {x y : L₁}, AddHom.toFun { toAddHom := { toFun := f, map_add' := h₁ }, map_smul' := h₂ }.toAddHom ⁅x, y⁆ = ⁅AddHom.toFun { toAddHom := { toFun := f, map_add' := h₁ }, map_smul' := h₂ }.toAddHom x, AddHom.toFun { toAddHom := { toFun := f, map_add' := h₁ }, map_smul' := h₂ }.toAddHom y⁆) : ↑{ toLinearMap := { toAddHom := { toFun := f, map_add' := h₁ }, map_smul' := h₂ }, map_lie' := h₃ } = f

def LieHom.comp {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) : L₁ →ₗ⁅R⁆ L₃

The composition of morphisms is a morphism.

theorem LieHom.comp_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) (x : L₁) : ↑(LieHom.comp f g) x = ↑f (↑g x)

@[simp]

theorem LieHom.coe_comp {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) : ↑(LieHom.comp f g) = ↑f ∘ ↑g

@[simp]

theorem LieHom.coe_linearMap_comp {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) : ↑(LieHom.comp f g) = LinearMap.comp ↑f ↑g

@[simp]

theorem LieHom.comp_id {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) : LieHom.comp f LieHom.id = f

@[simp]

theorem LieHom.id_comp {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) : LieHom.comp LieHom.id f = f

def LieHom.inverse {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (g : L₂ → L₁) (h₁ : Function.LeftInverse g ↑f) (h₂ : Function.RightInverse g ↑f) : L₂ →ₗ⁅R⁆ L₁

The inverse of a bijective morphism is a morphism.

def LieRingModule.compLieHom {R : Type u} {L₁ : Type v} {L₂ : Type w} (M : Type w₁) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [AddCommGroup M] [LieRingModule L₂ M] (f : L₁ →ₗ⁅R⁆ L₂) : LieRingModule L₁ M

A Lie ring module may be pulled back along a morphism of Lie algebras.

See note [reducible non-instances].

theorem LieRingModule.compLieHom_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} (M : Type w₁) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [AddCommGroup M] [LieRingModule L₂ M] (f : L₁ →ₗ⁅R⁆ L₂) (x : L₁) (m : M) : ⁅x, m⁆ = ⁅↑f x, m⁆

theorem LieModule.compLieHom {R : Type u} {L₁ : Type v} {L₂ : Type w} (M : Type w₁) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [AddCommGroup M] [LieRingModule L₂ M] (f : L₁ →ₗ⁅R⁆ L₂) [Module R M] [LieModule R L₂ M] : LieModule R L₁ M

A Lie module may be pulled back along a morphism of Lie algebras.

structure LieEquiv (R : Type u) (L : Type v) (L' : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] extends LieHom : Type (max v w)

• toFun : L → L'
• map_add' : ∀ (x y : L), AddHom.toFun s.toAddHom (x + y) = AddHom.toFun s.toAddHom x + AddHom.toFun s.toAddHom y
• map_smul' : ∀ (r : R) (x : L), AddHom.toFun s.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun s.toAddHom x
• map_lie' : ∀ {x y : L}, AddHom.toFun s.toAddHom ⁅x, y⁆ = ⁅AddHom.toFun s.toAddHom x, AddHom.toFun s.toAddHom y⁆
• invFun : L' → L

  The inverse function of an equivalence of Lie algebras

• left_inv : Function.LeftInverse s.invFun s.toFun

  The inverse function of an equivalence of Lie algebras is a left inverse of the underlying function.

• right_inv : Function.RightInverse s.invFun s.toFun

  The inverse function of an equivalence of Lie algebras is a right inverse of the underlying function.

An equivalence of Lie algebras 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.

def «term_≃ₗ⁅_⁆_» : Lean.TrailingParserDescr

An equivalence of Lie algebras 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.

def LieEquiv.toLinearEquiv {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (f : L₁ ≃ₗ⁅R⁆ L₂) : L₁ ≃ₗ[R] L₂

Consider an equivalence of Lie algebras as a linear equivalence.

instance LieEquiv.hasCoeToLieHom {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] : Coe (L₁ ≃ₗ⁅R⁆ L₂) (L₁ →ₗ⁅R⁆ L₂)

instance LieEquiv.hasCoeToLinearEquiv {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] : Coe (L₁ ≃ₗ⁅R⁆ L₂) (L₁ ≃ₗ[R] L₂)

instance LieEquiv.instEquivLikeLieEquiv {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] : EquivLike (L₁ ≃ₗ⁅R⁆ L₂) L₁ L₂

theorem LieEquiv.coe_to_lieHom {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) : ↑e.toLieHom = ↑e

@[simp]

theorem LieEquiv.coe_to_linearEquiv {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) : ↑(LieEquiv.toLinearEquiv e) = ↑e

@[simp]

theorem LieEquiv.to_linearEquiv_mk {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (g : L₂ → L₁) (h₁ : Function.LeftInverse g f.toFun) (h₂ : Function.RightInverse g f.toFun) : LieEquiv.toLinearEquiv { toLieHom := f, invFun := g, left_inv := h₁, right_inv := h₂ } = { toLinearMap := ↑f, invFun := g, left_inv := h₁, right_inv := h₂ }

theorem LieEquiv.coe_linearEquiv_injective {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] : Function.Injective LieEquiv.toLinearEquiv

theorem LieEquiv.coe_injective {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] : Function.Injective FunLike.coe

theorem LieEquiv.ext {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] {f : L₁ ≃ₗ⁅R⁆ L₂} {g : L₁ ≃ₗ⁅R⁆ L₂} (h : ∀ (x : L₁), ↑f x = ↑g x) : f = g

instance LieEquiv.instOneLieEquiv {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] : One (L₁ ≃ₗ⁅R⁆ L₁)

@[simp]

theorem LieEquiv.one_apply {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] (x : L₁) : ↑1 x = x

instance LieEquiv.instInhabitedLieEquiv {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] : Inhabited (L₁ ≃ₗ⁅R⁆ L₁)

def LieEquiv.refl {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] : L₁ ≃ₗ⁅R⁆ L₁

Lie algebra equivalences are reflexive.

@[simp]

theorem LieEquiv.refl_apply {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] (x : L₁) : ↑LieEquiv.refl x = x

def LieEquiv.symm {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) : L₂ ≃ₗ⁅R⁆ L₁

Lie algebra equivalences are symmetric.

@[simp]

theorem LieEquiv.symm_symm {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) : LieEquiv.symm (LieEquiv.symm e) = e

@[simp]

theorem LieEquiv.apply_symm_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) (x : L₂) : ↑e (↑(LieEquiv.symm e) x) = x

@[simp]

theorem LieEquiv.symm_apply_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) (x : L₁) : ↑(LieEquiv.symm e) (↑e x) = x

@[simp]

theorem LieEquiv.refl_symm {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] : LieEquiv.symm LieEquiv.refl = LieEquiv.refl

def LieEquiv.trans {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieRing L₂] [LieRing L₃] [LieAlgebra R L₁] [LieAlgebra R L₂] [LieAlgebra R L₃] (e₁ : L₁ ≃ₗ⁅R⁆ L₂) (e₂ : L₂ ≃ₗ⁅R⁆ L₃) : L₁ ≃ₗ⁅R⁆ L₃

Lie algebra equivalences are transitive.

@[simp]

theorem LieEquiv.self_trans_symm {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) : LieEquiv.trans e (LieEquiv.symm e) = LieEquiv.refl

@[simp]

theorem LieEquiv.symm_trans_self {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) : LieEquiv.trans (LieEquiv.symm e) e = LieEquiv.refl

@[simp]

theorem LieEquiv.trans_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieRing L₂] [LieRing L₃] [LieAlgebra R L₁] [LieAlgebra R L₂] [LieAlgebra R L₃] (e₁ : L₁ ≃ₗ⁅R⁆ L₂) (e₂ : L₂ ≃ₗ⁅R⁆ L₃) (x : L₁) : ↑(LieEquiv.trans e₁ e₂) x = ↑e₂ (↑e₁ x)

@[simp]

theorem LieEquiv.symm_trans {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieRing L₂] [LieRing L₃] [LieAlgebra R L₁] [LieAlgebra R L₂] [LieAlgebra R L₃] (e₁ : L₁ ≃ₗ⁅R⁆ L₂) (e₂ : L₂ ≃ₗ⁅R⁆ L₃) : LieEquiv.symm (LieEquiv.trans e₁ e₂) = LieEquiv.trans (LieEquiv.symm e₂) (LieEquiv.symm e₁)

theorem LieEquiv.bijective {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) : Function.Bijective ↑e.toLieHom

theorem LieEquiv.injective {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) : Function.Injective ↑e.toLieHom

theorem LieEquiv.surjective {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) : Function.Surjective ↑e.toLieHom

@[simp]

theorem LieEquiv.ofBijective_toFun {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (h : Function.Bijective ↑f) (a : L₁) : ↑(LieEquiv.ofBijective f h) a = ↑f a

@[simp]

theorem LieEquiv.ofBijective_invFun {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (h : Function.Bijective ↑f) : ∀ (a : L₂), LieEquiv.invFun (LieEquiv.ofBijective f h) a = ↑(LinearEquiv.symm (LinearEquiv.ofBijective (↑f) h)) a

noncomputable def LieEquiv.ofBijective {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (h : Function.Bijective ↑f) : L₁ ≃ₗ⁅R⁆ L₂

A bijective morphism of Lie algebras yields an equivalence of Lie algebras.

structure LieModuleHom (R : Type u) (L : Type v) (M : Type w) (N : Type w₁) [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] extends LinearMap : Type (max w w₁)

• toFun : M → N
• map_add' : ∀ (x y : M), AddHom.toFun s.toAddHom (x + y) = AddHom.toFun s.toAddHom x + AddHom.toFun s.toAddHom y
• map_smul' : ∀ (r : R) (x : M), AddHom.toFun s.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun s.toAddHom x
• map_lie' : ∀ {x : L} {m : M}, AddHom.toFun s.toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun s.toAddHom m⁆

  A module of Lie algebra modules is compatible with the action of the Lie algebra on the modules.

A morphism of Lie algebra modules is a linear map which commutes with the action of the Lie algebra.

def «term_→ₗ⁅_,_⁆_» : Lean.TrailingParserDescr

A morphism of Lie algebra modules is a linear map which commutes with the action of the Lie algebra.

instance LieModuleHom.instCoeOutLieModuleHomLinearMapToSemiringToCommSemiringIdToNonAssocSemiringToAddCommMonoidToAddCommMonoid {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] : CoeOut (M →ₗ⁅R,L⁆ N) (M →ₗ[R] N)

instance LieModuleHom.instFunLikeLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] : FunLike (M →ₗ⁅R,L⁆ N) M fun x => N

@[simp]

theorem LieModuleHom.coe_toLinearMap {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) : ↑↑f = ↑f

@[simp]

theorem LieModuleHom.map_smul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (c : R) (x : M) : ↑f (c • x) = c • ↑f x

@[simp]

theorem LieModuleHom.map_add {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (x : M) (y : M) : ↑f (x + y) = ↑f x + ↑f y

@[simp]

theorem LieModuleHom.map_sub {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (x : M) (y : M) : ↑f (x - y) = ↑f x - ↑f y

@[simp]

theorem LieModuleHom.map_neg {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (x : M) : ↑f (-x) = -↑f x

@[simp]

theorem LieModuleHom.map_lie {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (x : L) (m : M) : ↑f ⁅x, m⁆ = ⁅x, ↑f m⁆

theorem LieModuleHom.map_lie₂ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] [LieModule R L N] [LieModule R L P] (f : M →ₗ⁅R,L⁆ N →ₗ[R] P) (x : L) (m : M) (n : N) : ⁅x, ↑(↑f m) n⁆ = ↑(↑f ⁅x, m⁆) n + ↑(↑f m) ⁅x, n⁆

@[simp]

theorem LieModuleHom.map_zero {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) : ↑f 0 = 0

def LieModuleHom.id {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : M →ₗ⁅R,L⁆ M

The identity map is a morphism of Lie modules.

@[simp]

theorem LieModuleHom.coe_id {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : ↑LieModuleHom.id = id

theorem LieModuleHom.id_apply {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (x : M) : ↑LieModuleHom.id x = x

instance LieModuleHom.instZeroLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] : Zero (M →ₗ⁅R,L⁆ N)

The constant 0 map is a Lie module morphism.

@[simp]

theorem LieModuleHom.coe_zero {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] : ↑0 = 0

theorem LieModuleHom.zero_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (m : M) : ↑0 m = 0

instance LieModuleHom.instOneLieModuleHom {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : One (M →ₗ⁅R,L⁆ M)

The identity map is a Lie module morphism.

instance LieModuleHom.instInhabitedLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] : Inhabited (M →ₗ⁅R,L⁆ N)

theorem LieModuleHom.coe_injective {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] : Function.Injective FunLike.coe

theorem LieModuleHom.ext {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] {f : M →ₗ⁅R,L⁆ N} {g : M →ₗ⁅R,L⁆ N} (h : ∀ (m : M), ↑f m = ↑g m) : f = g

theorem LieModuleHom.ext_iff {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] {f : M →ₗ⁅R,L⁆ N} {g : M →ₗ⁅R,L⁆ N} : f = g ↔ ∀ (m : M), ↑f m = ↑g m

theorem LieModuleHom.congr_fun {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] {f : M →ₗ⁅R,L⁆ N} {g : M →ₗ⁅R,L⁆ N} (h : f = g) (x : M) : ↑f x = ↑g x

@[simp]

theorem LieModuleHom.mk_coe {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (h : ∀ {x : L} {m : M}, AddHom.toFun f.toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun f.toAddHom m⁆) : { toLinearMap := ↑f, map_lie' := h } = f

@[simp]

theorem LieModuleHom.coe_mk {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ[R] N) (h : ∀ {x : L} {m : M}, AddHom.toFun f.toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun f.toAddHom m⁆) : ↑{ toLinearMap := f, map_lie' := h } = ↑f

theorem LieModuleHom.coe_linear_mk {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ[R] N) (h : ∀ {x : L} {m : M}, AddHom.toFun f.toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun f.toAddHom m⁆) : ↑{ toLinearMap := f, map_lie' := h } = f

def LieModuleHom.comp {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) : M →ₗ⁅R,L⁆ P

The composition of Lie module morphisms is a morphism.

theorem LieModuleHom.comp_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) (m : M) : ↑(LieModuleHom.comp f g) m = ↑f (↑g m)

@[simp]

theorem LieModuleHom.coe_comp {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) : ↑(LieModuleHom.comp f g) = ↑f ∘ ↑g

@[simp]

theorem LieModuleHom.coe_linearMap_comp {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) : ↑(LieModuleHom.comp f g) = LinearMap.comp ↑f ↑g

def LieModuleHom.inverse {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (g : N → M) (h₁ : Function.LeftInverse g ↑f) (h₂ : Function.RightInverse g ↑f) : N →ₗ⁅R,L⁆ M

The inverse of a bijective morphism of Lie modules is a morphism of Lie modules.

instance LieModuleHom.instAddLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] : Add (M →ₗ⁅R,L⁆ N)

instance LieModuleHom.instSubLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] : Sub (M →ₗ⁅R,L⁆ N)

instance LieModuleHom.instNegLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] : Neg (M →ₗ⁅R,L⁆ N)

@[simp]

theorem LieModuleHom.coe_add {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (g : M →ₗ⁅R,L⁆ N) : ↑(f + g) = ↑f + ↑g

theorem LieModuleHom.add_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (g : M →ₗ⁅R,L⁆ N) (m : M) : ↑(f + g) m = ↑f m + ↑g m

@[simp]

theorem LieModuleHom.coe_sub {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (g : M →ₗ⁅R,L⁆ N) : ↑(f - g) = ↑f - ↑g

theorem LieModuleHom.sub_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (g : M →ₗ⁅R,L⁆ N) (m : M) : ↑(f - g) m = ↑f m - ↑g m

@[simp]

theorem LieModuleHom.coe_neg {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) : ↑(-f) = -↑f

theorem LieModuleHom.neg_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (m : M) : ↑(-f) m = -↑f m

instance LieModuleHom.hasNsmul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] : SMul ℕ (M →ₗ⁅R,L⁆ N)

@[simp]

theorem LieModuleHom.coe_nsmul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (n : ℕ) (f : M →ₗ⁅R,L⁆ N) : ↑(n • f) = n • ↑f

theorem LieModuleHom.nsmul_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (n : ℕ) (f : M →ₗ⁅R,L⁆ N) (m : M) : ↑(n • f) m = n • ↑f m

instance LieModuleHom.hasZsmul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] : SMul ℤ (M →ₗ⁅R,L⁆ N)

@[simp]

theorem LieModuleHom.coe_zsmul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (z : ℤ) (f : M →ₗ⁅R,L⁆ N) : ↑(z • f) = z • ↑f

theorem LieModuleHom.zsmul_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (z : ℤ) (f : M →ₗ⁅R,L⁆ N) (m : M) : ↑(z • f) m = z • ↑f m

instance LieModuleHom.instAddCommGroupLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] : AddCommGroup (M →ₗ⁅R,L⁆ N)

instance LieModuleHom.instSMulLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] [LieModule R L N] : SMul R (M →ₗ⁅R,L⁆ N)

@[simp]

theorem LieModuleHom.coe_smul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] [LieModule R L N] (t : R) (f : M →ₗ⁅R,L⁆ N) : ↑(t • f) = t • ↑f

theorem LieModuleHom.smul_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] [LieModule R L N] (t : R) (f : M →ₗ⁅R,L⁆ N) (m : M) : ↑(t • f) m = t • ↑f m

instance LieModuleHom.instModuleLieModuleHomToSemiringToCommSemiringToAddCommMonoidInstAddCommGroupLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] [LieModule R L N] : Module R (M →ₗ⁅R,L⁆ N)

structure LieModuleEquiv (R : Type u) (L : Type v) (M : Type w) (N : Type w₁) [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] extends LieModuleHom : Type (max w w₁)

• toFun : M → N
• map_add' : ∀ (x y : M), AddHom.toFun s.toAddHom (x + y) = AddHom.toFun s.toAddHom x + AddHom.toFun s.toAddHom y
• map_smul' : ∀ (r : R) (x : M), AddHom.toFun s.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun s.toAddHom x
• map_lie' : ∀ {x : L} {m : M}, AddHom.toFun s.toAddHom ⁅x, m⁆ = ⁅x, AddHom.toFun s.toAddHom m⁆
• invFun : N → M

  The inverse function of an equivalence of Lie modules

• left_inv : Function.LeftInverse s.invFun s.toFun

  The inverse function of an equivalence of Lie modules is a left inverse of the underlying function.

• right_inv : Function.RightInverse s.invFun s.toFun

  The inverse function of an equivalence of Lie modules is a right inverse of the underlying function.

An equivalence of Lie algebra modules is a linear equivalence which is also a morphism of Lie algebra modules.

def «term_≃ₗ⁅_,_⁆_» : Lean.TrailingParserDescr

An equivalence of Lie algebra modules is a linear equivalence which is also a morphism of Lie algebra modules.

def LieModuleEquiv.toLinearEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) : M ≃ₗ[R] N

View an equivalence of Lie modules as a linear equivalence.

def LieModuleEquiv.toEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) : M ≃ N

View an equivalence of Lie modules as a type level equivalence.

instance LieModuleEquiv.hasCoeToEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] : CoeOut (M ≃ₗ⁅R,L⁆ N) (M ≃ N)

instance LieModuleEquiv.hasCoeToLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] : Coe (M ≃ₗ⁅R,L⁆ N) (M →ₗ⁅R,L⁆ N)

instance LieModuleEquiv.hasCoeToLinearEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] : CoeOut (M ≃ₗ⁅R,L⁆ N) (M ≃ₗ[R] N)

instance LieModuleEquiv.instEquivLikeLieModuleEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] : EquivLike (M ≃ₗ⁅R,L⁆ N) M N

theorem LieModuleEquiv.injective {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) : Function.Injective ↑e

@[simp]

theorem LieModuleEquiv.toEquiv_mk {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (g : N → M) (h₁ : Function.LeftInverse g f.toFun) (h₂ : Function.RightInverse g f.toFun) : LieModuleEquiv.toEquiv { toLieModuleHom := f, invFun := g, left_inv := h₁, right_inv := h₂ } = { toFun := ↑f, invFun := g, left_inv := h₁, right_inv := h₂ }

@[simp]

theorem LieModuleEquiv.coe_mk {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (invFun : N → M) (h₁ : Function.LeftInverse invFun f.toFun) (h₂ : Function.RightInverse invFun f.toFun) : ↑{ toLieModuleHom := f, invFun := invFun, left_inv := h₁, right_inv := h₂ } = ↑f

theorem LieModuleEquiv.coe_to_lieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) : ↑e.toLieModuleHom = ↑e

@[simp]

theorem LieModuleEquiv.coe_to_linearEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) : ↑(LieModuleEquiv.toLinearEquiv e) = ↑e

theorem LieModuleEquiv.toEquiv_injective {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] : Function.Injective LieModuleEquiv.toEquiv

theorem LieModuleEquiv.ext {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e₁ : M ≃ₗ⁅R,L⁆ N) (e₂ : M ≃ₗ⁅R,L⁆ N) (h : ∀ (m : M), ↑e₁ m = ↑e₂ m) : e₁ = e₂

instance LieModuleEquiv.instOneLieModuleEquiv {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : One (M ≃ₗ⁅R,L⁆ M)

@[simp]

theorem LieModuleEquiv.one_apply {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (m : M) : ↑1 m = m

instance LieModuleEquiv.instInhabitedLieModuleEquiv {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Inhabited (M ≃ₗ⁅R,L⁆ M)

def LieModuleEquiv.refl {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : M ≃ₗ⁅R,L⁆ M

Lie module equivalences are reflexive.

@[simp]

theorem LieModuleEquiv.refl_apply {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (m : M) : ↑LieModuleEquiv.refl m = m

def LieModuleEquiv.symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) : N ≃ₗ⁅R,L⁆ M

Lie module equivalences are symmetric.

@[simp]

theorem LieModuleEquiv.apply_symm_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) (x : N) : ↑e (↑(LieModuleEquiv.symm e) x) = x

@[simp]

theorem LieModuleEquiv.symm_apply_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) (x : M) : ↑(LieModuleEquiv.symm e) (↑e x) = x

@[simp]

theorem LieModuleEquiv.symm_symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) : LieModuleEquiv.symm (LieModuleEquiv.symm e) = e

def LieModuleEquiv.trans {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (e₁ : M ≃ₗ⁅R,L⁆ N) (e₂ : N ≃ₗ⁅R,L⁆ P) : M ≃ₗ⁅R,L⁆ P

Lie module equivalences are transitive.

@[simp]

theorem LieModuleEquiv.trans_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (e₁ : M ≃ₗ⁅R,L⁆ N) (e₂ : N ≃ₗ⁅R,L⁆ P) (m : M) : ↑(LieModuleEquiv.trans e₁ e₂) m = ↑e₂ (↑e₁ m)

@[simp]

theorem LieModuleEquiv.symm_trans {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (e₁ : M ≃ₗ⁅R,L⁆ N) (e₂ : N ≃ₗ⁅R,L⁆ P) : LieModuleEquiv.symm (LieModuleEquiv.trans e₁ e₂) = LieModuleEquiv.trans (LieModuleEquiv.symm e₂) (LieModuleEquiv.symm e₁)

@[simp]

theorem LieModuleEquiv.self_trans_symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) : LieModuleEquiv.trans e (LieModuleEquiv.symm e) = LieModuleEquiv.refl

@[simp]

theorem LieModuleEquiv.symm_trans_self {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) : LieModuleEquiv.trans (LieModuleEquiv.symm e) e = LieModuleEquiv.refl