LieModule.ofAssociativeModule
theorem LieModule.ofAssociativeModule :
∀ {A : Type v} [inst : Ring A] {R : Type u} [inst_1 : CommRing R] [inst_2 : Algebra R A] {M : Type w}
[inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M],
LieModule R A M
This theorem states that for any associative algebra `A` over a commutative ring `R`, and any `R`-module `M` that is also an `A`-module such that the scalar multiplication is compatible (forming a scalar tower), `M` is a Lie module over `A` when `A` is regarded as a Lie algebra using the ring commutator. The theorem also explains that this cannot be a global instance because it would cause problems when `M` is the same as `A`.
More concisely: For any associative algebra `A` over a commutative ring `R`, an `R`-module `M` that is also an `A`-module with compatible scalar multiplication is a Lie module over `A` regarded as a Lie algebra via the ring commutator. However, this cannot be a global instance when `M = A`.
|
LieRing.of_associative_ring_bracket
theorem LieRing.of_associative_ring_bracket : ∀ {A : Type v} [inst : Ring A] (x y : A), ⁅x, y⁆ = x * y - y * x := by
sorry
This theorem states that for any type `A` that has a ring structure, the Lie bracket of two elements `x` and `y` from `A` is defined as the difference of the product of `x` and `y` in one order and the product in the reverse order. In other words, the Lie bracket `[x, y]` is equal to `x * y - y * x`. This is a definition often used in the theory of Lie algebras, which are algebraic structures that generalize certain properties of associative algebras.
More concisely: For any ring `A`, the Lie bracket `[x, y]` of elements `x` and `y` in `A` is defined as their commutator, i.e., `x * y - y * x`.
|