Theorems · Theorem · nonassociative algebras

LieModule.compLieHom

∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} (M : Type w₁) [inst : CommRing R] [inst_1 : LieRing L₁]
  [inst_2 : LieAlgebra R L₁] [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] [inst_5 : AddCommGroup M]
  [inst_6 : LieRingModule L₂ M] (f : L₁ →ₗ⁅R⁆ L₂) [inst_7 : Module R M] [LieModule R L₂ M], LieModule R L₁ M

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

Defined in

Mathlib.Algebra.Lie.Basic

Cited by

1 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext

Assumes

CommRingLieRingLieAlgebraLieRingLieAlgebraAddCommGroupLieRingModuleModuleLieModule