LieSubalgebra.coe_to_submodule_eq_iff
theorem LieSubalgebra.coe_to_submodule_eq_iff :
∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
(L₁' L₂' : LieSubalgebra R L), L₁'.toSubmodule = L₂'.toSubmodule ↔ L₁' = L₂'
This theorem states that for any two Lie subalgebras `L₁'` and `L₂'` of a Lie algebra `L` over a commutative ring `R`, the condition of their corresponding submodules being equal is equivalent to the Lie subalgebras themselves being equal. In other words, two Lie subalgebras are identical if and only if their submodules are identical. This theorem is a fundamental result in the theory of Lie algebras, linking the structure of Lie subalgebras with their underlying module structure.
More concisely: Two Lie subalgebras of a Lie algebra over a commutative ring are equal if and only if their submodules are equal.
|
LieSubalgebra.subset_lieSpan
theorem LieSubalgebra.subset_lieSpan :
∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {s : Set L},
s ⊆ ↑(LieSubalgebra.lieSpan R L s)
This theorem states that for any commutative ring `R`, any Lie ring `L` with a Lie algebra structure over `R`, and any set `s` of elements from `L`, the set `s` is a subset of the Lie subalgebra generated by `s`. In other words, every element of `s` belongs to the Lie subalgebra spanned by `s`. This is a foundational property of generated subalgebras in the context of Lie algebras.
More concisely: For any commutative ring `R`, any Lie ring `L` over `R`, and any set `s` of elements from `L`, `s` is contained in the Lie subalgebra of `L` generated by `s`.
|
LieSubalgebra.lie_mem
theorem LieSubalgebra.lie_mem :
∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
(L' : LieSubalgebra R L) {x y : L}, x ∈ L' → y ∈ L' → ⁅x, y⁆ ∈ L'
This theorem states that, for any commutative ring `R` and any Lie ring `L` that also carries a Lie algebra structure over `R`, if `L'` is a Lie subalgebra of `R` and `L`, and if `x` and `y` are elements of `L'`, then the Lie bracket (denoted as `[x, y]`) of `x` and `y` is also an element of `L'`. In other words, the Lie bracket of any two elements in a Lie subalgebra remains within the same subalgebra.
More concisely: For any commutative ring `R`, if `L` is a Lie subalgebra of the Lie algebra `L` over `R`, then the Lie bracket of any two elements in `L` lies in `L`.
|
LieSubalgebra.lie_mem'
theorem LieSubalgebra.lie_mem' :
∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
(self : LieSubalgebra R L) {x y : L}, x ∈ self.carrier → y ∈ self.carrier → ⁅x, y⁆ ∈ self.carrier
This theorem states that a Lie subalgebra is closed under the Lie bracket operation. Specifically, in the context of a commutative ring R and a Lie ring L that also has the structure of a Lie algebra over R, if we have a Lie subalgebra of L, and if x and y are elements in the carrier set of this subalgebra, then the Lie bracket of x and y (denoted by ⁅x, y⁆) is also in the carrier set of this subalgebra. This proves closure of the Lie subalgebra under the Lie bracket operation.
More concisely: In a Lie ring over a commutative ring R with the structure of a Lie algebra, any Lie subalgebra is closed under the Lie bracket operation.
|
LieSubalgebra.coe_to_submodule
theorem LieSubalgebra.coe_to_submodule :
∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
(L' : LieSubalgebra R L), ↑L'.toSubmodule = ↑L'
This theorem states that for any Lie subalgebra `L'` of a Lie algebra `L` over a commutative ring `R`, the coercion of `L'` to a submodule is equal to the coercion of `L'` itself. This ensures that the underlying set of `L'` as a submodule is the same as that of `L'` as a Lie subalgebra, giving consistency across different algebraic structures.
More concisely: The coercion of a Lie subalgebra of a Lie algebra as a submodule is equal to the subalgebra itself.
|
LieSubalgebra.ext
theorem LieSubalgebra.ext :
∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
(L₁' L₂' : LieSubalgebra R L), (∀ (x : L), x ∈ L₁' ↔ x ∈ L₂') → L₁' = L₂'
The theorem `LieSubalgebra.ext` states that for all given types `R` and `L`, where `R` has a Commutative Ring structure, `L` has a Lie Ring structure, and `L` is a Lie algebra over `R`, if we have two Lie subalgebras `L₁'` and `L₂'` of `L` over `R`, then these subalgebras are equal if and only if for all elements `x` in `L`, `x` is in `L₁'` if and only if `x` is in `L₂'`. In other words, two Lie subalgebras are equal if they contain exactly the same elements.
More concisely: Two Lie subalgebras of a Lie algebra over a commutative ring are equal if and only if they have the same elements.
|
LieHom.surjective_rangeRestrict
theorem LieHom.surjective_rangeRestrict :
∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L₂ : Type w}
[inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂), Function.Surjective ⇑f.rangeRestrict
The theorem `LieHom.surjective_rangeRestrict` states that for any commutative ring `R`, Lie rings `L` and `L₂`, and a Lie algebra structure over `L` and `L₂` with coefficients in `R`, every Lie morphism `f` from `L` to `L₂` is surjective when restricted to its range. In other words, for every element in the range of `f`, there exists an element in `L` such that applying the restricted Lie homomorph `f` to this element yields the original element from the range.
More concisely: Given a commutative ring R, Lie rings L and L₂, and a Lie algebra homomorphism f from L to L₂ over R, the image of f is all of L₂.
|