smul_lie
theorem smul_lie :
∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
[inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (t : R)
(x : L) (m : M), ⁅t • x, m⁆ = t • ⁅x, m⁆
This theorem states that for any commutative ring `R`, any Lie ring `L`, and any additive commutative group `M` that is a module over `R` and a Lie ring module over `L`, and for any `t` in `R`, `x` in `L`, and `m` in `M`, the Lie bracket of `t` times `x` and `m` is equal to `t` times the Lie bracket of `x` and `m`. This effectively shows that the scalar multiplication `t • x` can be distributed over the Lie bracket operation.
More concisely: For any commutative ring `R`, Lie ring `L`, and additive commutative group `M` being an `R`-module and an `L`-Lie module, the Lie bracket [x, m] equals the scalar multiplication by x of the Lie bracket [m, -] applied to m for all x in L and m in M.
|
LieRing.add_lie
theorem LieRing.add_lie : ∀ {L : Type v} [self : LieRing L] (x y z : L), ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆
The theorem `LieRing.add_lie` states that for any given Lie ring `L`, the Lie bracket is additive in its first component. Specifically, for any elements `x`, `y`, and `z` in `L`, the Lie bracket of the sum of `x` and `y` with `z` (denoted as [x + y, z]) is equal to the sum of the Lie bracket of `x` with `z` and the Lie bracket of `y` with `z` (denoted as [x, z] + [y, z]). In mathematical notation, this is often expressed as [x + y, z] = [x, z] + [y, z]. This property is a fundamental aspect of Lie rings.
More concisely: The Lie bracket in a Lie ring is additive in the first component, that is, [x + y, z] = [x, z] + [y, z] for all x, y, z in the Lie ring.
|
LieRingModule.leibniz_lie
theorem LieRingModule.leibniz_lie :
∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [self : LieRingModule L M] (x y : L)
(m : M), ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
This theorem states that for any Lie ring 'L', additive commutative group 'M', and a Lie ring module structure on 'L' and 'M', the bracket operation on 'L', 'M' and its elements 'x', 'y' (from 'L') and 'm' (from 'M') satisfies the Leibniz or Jacobi identity. The identity is expressed as the bracket of 'x' with the bracket of 'y' and 'm' equals the sum of the bracket of the bracket of 'x' and 'y' with 'm', and the bracket of 'y' with the bracket of 'x' and 'm'. This is an essential property of Lie algebras in the context of algebraic structures.
More concisely: For any Lie ring 'L', additive commutative group 'M' with a Lie ring module structure, and elements 'x', 'y' in 'L' and 'm' in 'M', the Lie bracket satisfies the Leibniz identity: [x, [y, m]] = [[x, y], m] + [ [y, x], m].
|
LieHom.map_zero
theorem LieHom.map_zero :
∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
[inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂), f 0 = 0
The theorem `LieHom.map_zero` states that for any given Lie algebra homomorphism `f` from `L₁` to `L₂` over a commutative ring `R`, the image of the zero element of `L₁` under `f` is the zero element of `L₂`. In other words, `f` preserves the zero element when mapping from one Lie algebra to another. This theorem is valid for any types `R`, `L₁`, and `L₂` where `R` is a commutative ring and `L₁` and `L₂` are Lie algebras over `R`.
More concisely: For any Lie algebra homomorphism f from Lie algebra L₁ to Lie algebra L₂ over commutative ring R, f(0) = 0, where 0 denotes the zero element in L₁ and L₂.
|
LieRingModule.lie_add
theorem LieRingModule.lie_add :
∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [self : LieRingModule L M] (x : L)
(m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆
This theorem states that for any Lie ring `L`, additive commutative group `M`, and any `L`-module structure on `M`, the Lie bracket operation is additive in its second component. Specifically, given any element `x` from `L` and any two elements `m` and `n` from `M`, the Lie bracket of `x` with the sum of `m` and `n` equals the sum of the Lie bracket of `x` with `m` and the Lie bracket of `x` with `n`. This essentially means that the Lie bracket respects the addition operation in the second component of the bracket.
More concisely: For any Lie ring `L`, additive commutative group `M`, and `L`-module structure on `M`, the Lie bracket of an element `x` in `L` with the sum of two elements `m` and `n` in `M` equals the sum of the Lie brackets of `x` with `m` and `x` with `n`.
|
add_lie
theorem add_lie :
∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (x y : L)
(m : M), ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆
This theorem, `add_lie`, states that for any types `L` and `M`, where `L` is a Lie ring, `M` is an additive commutative group, and `M` is also a module over `L`, the Lie bracket of the sum of two elements `x` and `y` in `L` with an element `m` in `M` equals the sum of the Lie brackets of `x` and `m` and of `y` and `m`. In the language of mathematics, this can be represented as: ∀x, y ∈ L and m ∈ M, [x + y, m] = [x, m] + [y, m]. This property is a key aspect of the structure of Lie rings and their modules.
More concisely: For any Lie ring `L`, additive commutative group and `L`-module `M`, the Lie bracket of a sum of elements in `L` with an element in `M` equals the sum of the Lie brackets of each element with that element in `M`.
|
lie_neg
theorem lie_neg :
∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (x : L)
(m : M), ⁅x, -m⁆ = -⁅x, m⁆
This theorem states that for any Lie ring `L`, additive commutative group `M`, and Lie ring module `L M`, if `x` is an element of `L` and `m` is an element of `M`, the Lie bracket of `x` and the negation of `m` is equal to the negation of the Lie bracket of `x` and `m`. In other words, the negation of an element in the additive commutative group `M` can be moved outside of the Lie bracket with a change of sign.
More concisely: For any Lie ring `L`, additive commutative group `M`, and Lie ring module `LM`, the Lie bracket of an element `x` in `L` and the negation of an element `m` in `M` is equal to the negation of the Lie bracket of `x` and `m`.
|
lie_smul
theorem lie_smul :
∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
[inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (t : R)
(x : L) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆
This theorem, `lie_smul`, states that for any commutative ring `R`, any Lie ring `L`, and any additive commutative group `M` that is also a module over `R` and a Lie ring module over `L`, and which forms a Lie module over `R` and `L`, the Lie bracket of an element `x` in `L` and the scalar multiplication of a scalar `t` in `R` and an element `m` in `M` is equal to the scalar multiplication of `t` with the Lie bracket of `x` and `m`. In terms of mathematics notation, for all `t` in `R`, `x` in `L`, and `m` in `M`, the theorem states that `[x, t * m] = t * [x, m]`, where `[.,.]` denotes the Lie bracket, and `*` denotes scalar multiplication.
More concisely: For any commutative ring `R`, Lie ring `L`, and additive commutative group `M` that is both an `R`-module and a Lie ring module, the Lie bracket of an element in `L` with the scalar multiplication of a scalar in `R` and an element in `M` equals the scalar multiplication of the scalar with the Lie bracket of the element in `L` and the element in `M`.
|
LieRing.leibniz_lie
theorem LieRing.leibniz_lie : ∀ {L : Type v} [self : LieRing L] (x y z : L), ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆
This theorem states that for any Lie ring `L` and any elements `x`, `y`, and `z` of `L`, the Lie ring bracket satisfies the Leibniz (or Jacobi) identity. In terms of the Lie bracket notation, the identity is expressed as `[x, [y, z]] = [[x, y], z] + [y, [x, z]]`. This is a fundamental property of Lie rings and underlies their structure and operation.
More concisely: The Lie bracket of a Lie ring satisfies the Jacobi identity: `[x, [y, z]] = [[x, y], z] + [y, [x, z]]` for all `x, y, z` in the Lie ring.
|
LieRing.lie_self
theorem LieRing.lie_self : ∀ {L : Type v} [self : LieRing L] (x : L), ⁅x, x⁆ = 0
This theorem, `LieRing.lie_self`, states that for any Lie ring `L`, the Lie bracket of any element with itself is always zero. In other words, if `x` is an element in `L`, then the Lie bracket of `x` and `x`, denoted as `⁅x, x⁆`, equals zero. This is a key property of Lie rings, reflecting the antisymmetry of the Lie bracket operation.
More concisely: For any Lie ring `L` and element `x` in `L`, the Lie bracket `⁅x, x⁆` equals zero.
|
LieEquiv.right_inv
theorem LieEquiv.right_inv :
∀ {R : Type u} {L : Type v} {L' : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
[inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] (self : L ≃ₗ⁅R⁆ L'),
Function.RightInverse self.invFun self.toFun
This theorem states that for any commutative ring `R`, and any two Lie algebras `L` and `L'` over `R`, if there exists a Lie algebra equivalence from `L` to `L'`, then the inverse function of this equivalence is a right inverse to the underlying function of the equivalence. In other words, if we apply the equivalence to an element in `L`, and then apply the inverse function, we get back the original element. This is symbolically expressed as "f composed with g equals the identity function", which is written as `f ∘ g = id` in functional notation.
More concisely: Given any Lie algebra equivalence `f: L ↔ L'` between commutative ring Lie algebras `L` and `L'`, the inverse function `g` of `f` is a right inverse, i.e., `f ∘ g = id_L` on `L` and `g ∘ f = id_L'` on `L'`.
|
zero_lie
theorem zero_lie :
∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (m : M),
⁅0, m⁆ = 0
This theorem states that for any types `L` and `M`, given `L` is a Lie ring, `M` is an additive commutative group, and `M` is a Lie ring module over `L`, the Lie bracket of zero from `L` and any element `m` from `M` is zero. In other words, the Lie bracket of zero with any element in a Lie ring module results in zero.
More concisely: For any Lie ring `L`, additive commutative group `M`, and Lie ring module `M` over `L`, the Lie bracket of the zero element in `L` with any element in `M` is the zero element in `L`.
|
LieRing.lie_add
theorem LieRing.lie_add : ∀ {L : Type v} [self : LieRing L] (x y z : L), ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆
The theorem `LieRing.lie_add` states that for any Lie ring `L`, and any three elements `x`, `y`, and `z` in `L`, the Lie bracket operation with `x` and the sum of `y` and `z` (denoted by `⁅x, y + z⁆`) is equal to the sum of the Lie bracket of `x` with `y` and the Lie bracket of `x` with `z` (denoted by `⁅x, y⁆ + ⁅x, z⁆`). In other words, the Lie ring bracket operation is additive in its second component.
More concisely: For any Lie ring `L` and elements `x, y, z` in `L`, `⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆`.
|
lie_skew
theorem lie_skew : ∀ {L : Type v} [inst : LieRing L] (x y : L), -⁅y, x⁆ = ⁅x, y⁆
This theorem, named "lie_skew", states that for any type `L` that has a Lie ring structure, and for any two elements `x` and `y` of this type, the Lie bracket of `y` and `x` negated is equal to the Lie bracket of `x` and `y`. In mathematical notation, this would be written as: for all `x` and `y` in `L`, `- [y,x] = [x,y]`. This property is known as skew-symmetry and is one of the defining properties of Lie algebras.
More concisely: For any Lie ring `L`, the Lie bracket is skew-symmetric, that is, `- [y,x] = [x,y]` for all `x, y` in `L`.
|
LieHom.map_lie
theorem LieHom.map_lie :
∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
[inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁), f ⁅x, y⁆ = ⁅f x, f y⁆
This theorem states that for any commutative ring `R` and two Lie Algebras `L₁` and `L₂` over `R`, any Lie algebra homomorphism `f` from `L₁` to `L₂` preserves the Lie brackets. In other words, applying `f` to the Lie bracket of `x` and `y` (denoted as `⁅x, y⁆`) in `L₁` results in the same as the Lie bracket of `f x` and `f y` in `L₂`.
More concisely: Given any commutative ring `R`, Lie algebra homomorphism `f` from Lie algebra `L₁` to Lie algebra `L₂` over `R`, for all elements `x, y` in `L₁`, `f(⁅x, y⁆) = ⁅f(x), f(y)⁆`.
|
LieModuleEquiv.left_inv
theorem LieModuleEquiv.left_inv :
∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
[inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
[inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (self : M ≃ₗ⁅R,L⁆ N),
Function.LeftInverse self.invFun self.toFun
The theorem `LieModuleEquiv.left_inv` states that for any commutative ring `R`, Lie ring `L`, and additively commutative groups `M` and `N` that are also `R`-modules, and if `M` and `N` are Lie ring modules over `L`, then for any Lie module equivalence (denoted by `M ≃ₗ⁅R,L⁆ N`) from `M` to `N`, the inverse function of the equivalence is a left inverse to the underlying function. This means that if we apply the equivalence to an element of `M` and then apply the inverse function, we get the original element of `M` back.
More concisely: Given a Lie ring equivalence between additively commutative `R`-module Lie rings `M` and `N`, the inverse function is a left inverse to the underlying function.
|
LieModule.smul_lie
theorem LieModule.smul_lie :
∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
[inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [self : LieModule R L M] (t : R)
(x : L) (m : M), ⁅t • x, m⁆ = t • ⁅x, m⁆
This theorem states that for any commutative ring `R`, Lie ring `L`, and additive commutative group `M` that is also a module over `R` and a Lie ring module over `L`, the Lie bracket operation is compatible with scalar multiplication in its first argument. More precisely, for any scalar `t` from `R`, any element `x` from `L`, and any element `m` from `M`, the Lie bracket of the scalar multiple of `x` by `t` and `m` is equal to the scalar multiple of the Lie bracket of `x` and `m` by `t`. This means that scalar multiplication can be factored out of the Lie bracket, a property that shows the compatibility between the operations of scalar multiplication and the Lie bracket.
More concisely: For any commutative ring R, Lie ring L, and additive abelian group M as an R-module and Lie module over L, the Lie bracket [x, m] of any x in L and m in M satisfies [tx, m] = t[x, m] for all scalars t in R.
|
LieHom.coe_toLinearMap
theorem LieHom.coe_toLinearMap :
∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
[inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L₁ →ₗ⁅R⁆ L₂), ⇑↑f = ⇑f
This theorem states that for any commutative ring `R`, Lie rings `L₁` and `L₂`, and Lie algebras over `R` on `L₁` and `L₂`, the coercion (type conversion) of any Lie algebra homomorphism `f` from `L₁` to `L₂` to a linear map is equal to the original Lie algebra homomorphism `f`. In other words, applying the coercion function to `f` doesn't change its behavior.
More concisely: For any commutative ring `R`, Lie algebra homomorphisms `f` from Lie algebra `L₁` to Lie algebra `L₂` over `R` coerce to the same linear maps.
|
LieModuleHom.map_lie
theorem LieModuleHom.map_lie :
∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
[inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
[inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (x : L) (m : M),
f ⁅x, m⁆ = ⁅x, f m⁆
This theorem states that for any commutative ring `R`, any Lie ring `L`, and any additive commutative groups `M` and `N` that are also `R`-modules, given a Lie module homomorphism `f` from `M` to `N` and elements `x` from `L` and `m` from `M`, the application of `f` to the Lie bracket of `x` and `m` is equal to the Lie bracket of `x` and the application of `f` to `m`. In other words, the Lie module homomorphism `f` preserves the operation of the Lie bracket.
More concisely: Given a Lie module homomorphism `f` between commutative `R`-modules `M` and `N` over a commutative ring `R`, and Lie rings `L`, the application of `f` to the Lie bracket of an element `x` in `L` and an element `m` in `M` is equal to the Lie bracket of `x` and `f(m)`.
|
LieModuleHom.map_lie'
theorem LieModuleHom.map_lie' :
∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
[inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
[inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (self : M →ₗ⁅R,L⁆ N) {x : L} {m : M},
self.toFun ⁅x, m⁆ = ⁅x, self.toFun m⁆
This theorem states that for any commutative ring R, Lie ring L, additive commutative groups M and N, and any modules M and N over R, if M and N are also modules over the Lie ring L, then the action of the Lie algebra on the module is compatible with a given Lie module homomorphism. Specifically, if we have a Lie module homomorphism from M to N, then applying this homomorphism to the Lie bracket of an element from L and an element from M results in the same as the Lie bracket of the same element from L and the homomorphism applied to the element from M.
More concisely: For any commutative ring R, Lie rings L, modules M and N over R, given a Lie module homomorphism f : M -> N between M and N as Lie modules over L, the commutativity of the following diagram holds: L x M -> M, (x, m) -> x.m, and L x N -> N, x.f(m) -> f(x.m), where x is an element from L.
|
LieModule.compLieHom
theorem 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] [inst_8 : LieModule R L₂ M],
LieModule R L₁ M
This theorem states that for any commutative ring `R` and Lie algebras `L₁` and `L₂`, along with a module `M` over `L₂` that is also a Lie ring module, we can "pull back" this module structure along a morphism `f` from `L₁` to `L₂`. This results in a new Lie module structure on `M` over `L₁`. This is essentially a generalization of the pullback operation from topology and algebra, in the context of Lie algebras and Lie modules.
More concisely: Given a commutative ring `R`, Lie algebras `L₁` and `L₂`, and a Lie module `M` over `L₂`, there exists a Lie module structure on `M` over `L₁` induced by a morphism `f` from `L₁` to `L₂`.
|
lie_zero
theorem lie_zero :
∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (x : L),
⁅x, 0⁆ = 0
This theorem states that for all elements `x` of a Lie Ring `L` acting on an Additive Commutative Group `M`, where `M` is a module over the Lie ring `L` (i.e., `M` is a `LieRingModule` for `L`), the Lie bracket of `x` and the zero element of `M` is itself zero. Essentially, it expresses that zero behaves as an identity element with respect to the Lie bracket operation.
More concisely: For every Lie Ring element `x` and any Additive Commutative Group element `m` in a Lie Ring Module, the Lie bracket `[x, 0_M]` equals the zero element of the Lie Ring.
|
lie_lie
theorem lie_lie :
∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (x y : L)
(m : M), ⁅⁅x, y⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆
This theorem, called `lie_lie`, states that for any two elements `x` and `y` of a Lie ring `L`, and any element `m` of an additive commutative group `M` which is also a `L`-module, the double Lie bracket of `x`, `y`, and `m` is equal to the difference between the Lie bracket of `x` with the Lie bracket of `y` and `m`, and the Lie bracket of `y` with the Lie bracket of `x` and `m`. In mathematical notation, this is: [[x, y], m] = [x, [y, m]] - [y, [x, m]].
More concisely: The double Lie bracket of two elements in a Lie ring and an element of the associated Lie-module equals the commutator of the Lie brackets of the two elements with the module element. In Lean notation: [[x, y], m] = [x, [y, m]] - [y, [x, m]].
|
lie_add
theorem lie_add :
∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (x : L)
(m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆
This theorem, `lie_add`, states that for any Lie ring `L` and any additive commutative group `M`, where `M` is also a module over the Lie ring `L`, the Lie bracket of an element `x` in `L` with the sum of two elements `m` and `n` in `M` is equal to the sum of the Lie bracket of `x` with `m` and the Lie bracket of `x` with `n`. In terms of mathematical notation, this is stating that for all `x`, `m`, and `n`, `[x, m + n] = [x, m] + [x, n]`, where `[.,.]` denotes the Lie bracket.
More concisely: For any Lie ring `L` and additive commutative group `M` being an `L`-module, the Lie bracket of an element `x` in `L` with the sum of two elements `m` and `n` in `M` equals the sum of the Lie brackets of `x` with `m` and `n`, i.e., `[x, m + n] = [x, m] + [x, n]`.
|
LieModule.lie_smul
theorem LieModule.lie_smul :
∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
[inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [self : LieModule R L M] (t : R)
(x : L) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆
The theorem `LieModule.lie_smul` states that for any commutative ring `R`, any Lie ring `L`, and any additive commutative group `M` that is also a module over `R` and a Lie ring module over `L`, the Lie bracket operation is compatible with scalar multiplication in its second argument. More specifically, the Lie bracket of `x` from `L` and the scalar multiple `t • m` from `M` is equal to the scalar multiple `t •` the Lie bracket of `x` and `m`. This is expressed mathematically as `⁅x, t • m⁆ = t • ⁅x, m⁆` for all `t` in `R`, `x` in `L`, and `m` in `M`.
More concisely: For any commutative ring R, Lie ring L, and an additive commutative group M that is both an R-module and an L-Lie module, the Lie bracket of an element x in L with the scalar multiple t • m in M is equal to the scalar multiple t of the Lie bracket of x and m, i.e., ⁅x, t • m⁆ = t • ⁅x, m⁆.
|
LieModuleEquiv.ext
theorem LieModuleEquiv.ext :
∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
[inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
[inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (e₁ e₂ : M ≃ₗ⁅R,L⁆ N),
(∀ (m : M), e₁ m = e₂ m) → e₁ = e₂
This theorem states that for any given commutative ring "R", Lie ring "L", and additive commutative groups "M" and "N" that also have a module structure over "R" with "M" and "N" being Lie ring modules over "L", if there are two Lie algebra module isomorphisms (denoted as "e₁" and "e₂") between "M" and "N" that have the same effect on every element of "M", then "e₁" and "e₂" are the same isomorphism. In simpler terms, if you have two transformation rules that behave the same way for each element of "M", then these transformation rules are in fact the same.
More concisely: If two Lie algebra module isomorphisms between two Lie ring modules over a commutative ring have the same action on every element, then they are equal.
|
LieEquiv.left_inv
theorem LieEquiv.left_inv :
∀ {R : Type u} {L : Type v} {L' : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
[inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] (self : L ≃ₗ⁅R⁆ L'),
Function.LeftInverse self.invFun self.toFun
The theorem `LieEquiv.left_inv` states that for any commutative ring `R` and any two Lie algebras `L` and `L'` over `R`, for any Lie algebra equivalence between `L` and `L'`, the inverse function of this equivalence is a left inverse of the function underlying the equivalence. In other words, if we apply the inverse function after applying the function of the equivalence to any element in the Lie algebra `L`, we will get back the original element. This theorem guarantees the reversibility of the mapping defined by the Lie algebra equivalence.
More concisely: Given any Lie algebra equivalence between commutative ring Lie algebras, the inverse function is a left inverse of the underlying function.
|
LieEquiv.injective
theorem LieEquiv.injective :
∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
[inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂), Function.Injective ⇑e.toLieHom
The theorem `LieEquiv.injective` states that for all types `R`, `L₁`, and `L₂` such that `R` is a commutative ring, `L₁` and `L₂` are both Lie rings, and `L₁` and `L₂` are Lie algebras over `R`, if `e` is a Lie algebra equivalence from `L₁` to `L₂`, then the underlying function of the Lie homomorphism associated with `e` is injective. In other words, if two elements in `L₁` are mapped to the same element in `L₂` by `e`, then those two elements must have been the same to begin with.
More concisely: If `e` is a Lie algebra equivalence between Lie rings `L₁` and `L₂` over a commutative ring `R`, then the underlying function of the associated Lie homomorphism is injective.
|
LieHom.map_lie'
theorem LieHom.map_lie' :
∀ {R : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
[inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] (self : L →ₗ⁅R⁆ L') {x y : L},
self.toFun ⁅x, y⁆ = ⁅self.toFun x, self.toFun y⁆
The theorem `LieHom.map_lie'` states that for any commutative ring `R` and Lie algebras `L` and `L'` over `R`, any Lie algebra morphism from `L` to `L'` preserves the Lie bracket operation. More specifically, for any two elements `x` and `y` in `L`, the Lie bracket of their images under the morphism is equal to the image of their Lie bracket in `L`.
More concisely: Given a commutative ring R, Lie algebras L and L' over R, and a Lie algebra morphism f : L -> L', for all x, y in L, we have f[([x, y]\_L)] = [f[x], f[y]]\_L'.
|
neg_lie
theorem neg_lie :
∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (x : L)
(m : M), ⁅-x, m⁆ = -⁅x, m⁆
This theorem, `neg_lie`, states that for any Lie ring `L`, additively commutative group `M`, and any Lie ring module (a module for a Lie ring) `L M`, for any elements `x` of `L` and `m` of `M`, the Lie bracket of `-x` and `m` is equal to the negation of the Lie bracket of `x` and `m`. In mathematical notation, this would be denoted as `-x, m = -⁅x, m⁆`. This theorem holds for all possible `x` in `L` and `m` in `M`.
More concisely: For any Lie ring `L`, additively commutative group `M`, and Lie ring module `L M`, the Lie bracket of `-x` and `m` equals the negation of the Lie bracket of `x` and `m`, for all `x` in `L` and `m` in `M`.
|
LieHom.ext
theorem LieHom.ext :
∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
[inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] {f g : L₁ →ₗ⁅R⁆ L₂}, (∀ (x : L₁), f x = g x) → f = g
This theorem, `LieHom.ext`, states that for any commutative ring `R` and two Lie algebras `L₁` and `L₂` over `R`, if two Lie algebra homomorphisms `f` and `g` from `L₁` to `L₂` agree on all elements of `L₁` (i.e., `f x = g x` for all `x` in `L₁`), then `f` and `g` must be the same homomorphism. In other words, two Lie algebra homomorphisms are identical if they coincide on every element of the domain.
More concisely: If `R` is a commutative ring and `f` and `g` are Lie algebra homomorphisms from a Lie algebra `L₁` to a Lie algebra `L₂` over `R` such that `f x = g x` for all `x` in `L₁`, then `f = g`.
|
LieRingModule.add_lie
theorem LieRingModule.add_lie :
∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [self : LieRingModule L M] (x y : L)
(m : M), ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆
This theorem states that the Lie bracket operation in a Lie ring module is additive in its first component. Specifically, for any elements 'x' and 'y' of a type 'L', which is a Lie ring, and 'm' of a type 'M', which is an additive commutative group, the Lie bracket of the sum of 'x' and 'y' with 'm' is equal to the sum of the Lie brackets of 'x' with 'm' and 'y' with 'm'. This holds for all Lie ring modules 'L' and 'M'.
More concisely: For any Lie ring module L and additive commutative group M, the Lie bracket of (x + y) with m equals the sum of the Lie brackets of x with m and y with m, for all x, y in L and m in M.
|
lie_self
theorem lie_self : ∀ {L : Type v} [inst : LieRing L] (x : L), ⁅x, x⁆ = 0
This theorem, referred to as `lie_self`, states that for all elements `x` of a type `L`, where `L` is equipped with a Lie ring structure (denoted by `[inst : LieRing L]`), the Lie bracket of `x` with itself (denoted by `⁅x, x⁆`) equals zero. In other words, for any element in a Lie ring, the Lie bracket of the element with itself is always zero. The notation `⁅x, x⁆` is used to represent the Lie bracket, which is a binary operation that combines two elements in the Lie ring.
More concisely: For any element x in a Lie ring L, the Lie bracket [x, x] equals zero.
|
leibniz_lie
theorem leibniz_lie :
∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (x y : L)
(m : M), ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
The theorem `leibniz_lie` states that for any Lie ring `L`, additive commutative group `M`, and a Lie ring module `M` over `L`, given any elements `x` and `y` in `L` and an element `m` in `M`, the nested Lie bracket of `x` with the Lie bracket of `y` and `m` equals the sum of the Lie bracket of `x` with `y` acted on `m` and the Lie bracket of `y` with the Lie bracket of `x` and `m`. It is a formulation of the Leibniz identity in the context of Lie algebras.
More concisely: For any Lie ring `L`, additive commutative group `M`, and Lie module `M` over `L`, the Lie bracket of `x` and the Lie bracket of `y` with `m` in `L x M` satisfies the Leibniz identity: `[x, [y, m]] = [x, y] . m + [y, x] . m`.
|
LieModuleEquiv.right_inv
theorem LieModuleEquiv.right_inv :
∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
[inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
[inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (self : M ≃ₗ⁅R,L⁆ N),
Function.RightInverse self.invFun self.toFun
The theorem `LieModuleEquiv.right_inv` states that for any commutative ring `R`, Lie ring `L`, and additive commutative groups `M` and `N` which are also both `R`-modules and `L`-Lie ring modules, the inverse function of an equivalence between `M` and `N` (denoted `M ≃ₗ⁅R,L⁆ N`) is a right inverse to the function of the equivalence. In other words, if we apply the equivalence function to an element and then apply the inverse function, we get back the original element.
More concisely: For any commutative ring `R`, Lie ring `L`, and additive commutative `R`-module and `L`-Lie ring module groups `M` and `N` with an equivalence `M ≃ₗ⁅R,L⁆ N`, the inverse function of this equivalence is a right inverse.
|
LieAlgebra.lie_smul
theorem LieAlgebra.lie_smul :
∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [self : LieAlgebra R L] (t : R) (x y : L),
⁅x, t • y⁆ = t • ⁅x, y⁆
This theorem states that for any commutative ring `R`, any Lie ring `L`, and a Lie algebra `self` over `R` and `L`, the Lie algebra bracket is compatible with scalar multiplication in its second argument. In other words, for any elements `x` and `y` of the Lie ring `L` and any scalar `t` from the commutative ring `R`, the Lie bracket of `x` and the product of `t` and `y` equals the product of `t` and the Lie bracket of `x` and `y`. This compatibility in the first argument is not a class property, but it follows since every Lie algebra has a natural Lie module action on itself.
More concisely: For any commutative ring `R`, Lie ring `L`, Lie algebra `self` over `R` and `L`, and elements `x` in `L` and scalar `t` in `R`, we have `[x, t*y] = t*[x, y]`.
|