English
A module M over a ring A can be viewed as a Lie ring module over A, where the Lie bracket on A acts on M by the given module action: for a ∈ A and m ∈ M, ⁅a, m⁆ = a · m.
Русский
Модуль M над кольцом A может рассматриваться как Lie-модуль над A: скобка ⁅a, m⁆ равна действию модуля a·m, при a ∈ A, m ∈ M.
LaTeX
$$$[a,m] = a\cdot m \quad (a \in A, \ m \in M).$$$
Lean4
/-- We can regard a module over an associative ring `A` as a Lie ring module over `A` with Lie
bracket equal to its ring commutator.
Note that this cannot be a global instance because it would create a diamond when `M = A`,
specifically we can build two mathematically-different `bracket A A`s:
1. `@Ring.bracket A _` which says `⁅a, b⁆ = a * b - b * a`
2. `(@LieRingModule.ofAssociativeModule A _ A _ _).toBracket` which says `⁅a, b⁆ = a • b`
(and thus `⁅a, b⁆ = a * b`)
See note [reducible non-instances] -/
abbrev ofAssociativeModule : LieRingModule A M where
bracket := (· • ·)
add_lie := add_smul
lie_add := smul_add
leibniz_lie := by simp [LieRing.of_associative_ring_bracket, sub_smul, mul_smul, sub_add_cancel]
