LieSubmodule.ext
theorem LieSubmodule.ext :
∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : LieRingModule L M] (N N' : LieSubmodule R L M),
(∀ (m : M), m ∈ N ↔ m ∈ N') → N = N'
This theorem states that for any two Lie submodules `N` and `N'` of the module `M` over the commutative ring `R`, with `L` as a Lie ring and `M` as a group under addition, if every element `m` of `M` is an element of `N` if and only if it is an element of `N'`, then `N` and `N'` are the same Lie submodule. In other words, two Lie submodules are the same if they contain exactly the same elements.
More concisely: Two Lie submodules of a Lie module over a commutative ring are equal if and only if they contain the same elements.
|
LieModuleHom.map_top
theorem LieModuleHom.map_top :
∀ {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 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup N]
[inst_6 : Module R N] [inst_7 : LieRingModule L N] (f : M →ₗ⁅R,L⁆ N), LieSubmodule.map f ⊤ = f.range
This theorem states that for any commutative ring `R`, Lie ring `L`, additive commutative groups `M` and `N`, and modules `M` and `N` over `R` that are also Lie ring modules over `L`, if `f` is a Lie module homomorphism from `M` to `N`, then the image of the entire Lie submodule of `M` under `f` is equal to the range of `f`. That is, applying `f` to every element of `M` will yield every possible output of `f`.
More concisely: For any commutative ring `R`, Lie ring `L`, additive commutative groups `M` and `N` that are Lie ring modules over `L`, and a Lie module homomorphism `f` from `M` to `N` over `R`, the image of every Lie submodule of `M` under `f` equals the range of `f`.
|
LieHom.idealRange_eq_top_of_surjective
theorem LieHom.idealRange_eq_top_of_surjective :
∀ {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'), Function.Surjective ⇑f → f.idealRange = ⊤
This theorem states that for any commutative ring `R`, Lie rings `L` and `L'`, and a morphism `f` from `L` to `L'` as Lie algebras over `R`, if the morphism `f` is surjective (i.e., every element of `L'` can be mapped from some element of `L`), then the ideal range of `f` (the set of all images of `f`, considered as a Lie ideal in `L'`) equals the whole Lie algebra `L'`. In other words, the ideal range of a surjective Lie algebra morphism spans the entire codomain.
More concisely: If `f` is a surjective Lie algebra homomorphism from a Lie algebra `L` over a commutative ring `R` to a Lie algebra `L'`, then the ideal range of `f` equals `L'`.
|
LieSubmodule.sup_coe_toSubmodule
theorem LieSubmodule.sup_coe_toSubmodule :
∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : LieRingModule L M] (N N' : LieSubmodule R L M), ↑(N ⊔ N') = ↑N ⊔ ↑N'
This theorem, "LieSubmodule.sup_coe_toSubmodule", 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`, and for any two Lie submodules `N` and `N'` of `M`, the Lie submodule generated by the union of `N` and `N'` is the same as the submodule generated by the union of the underlying submodules of `N` and `N'`. In other words, the process of taking a union of two Lie submodules and then considering the underlying submodule does not depend on the order in which these operations are performed.
More concisely: Given a commutative ring `R`, a Lie ring `L`, an additive commutative group `M` that is both an `R`-module and a Lie `L`-module, and Lie submodules `N` and `N'` of `M`, the Lie submodule generated by `N ∪ N'` is equal to the submodule generated by `N ∎ N'`, where `∎` denotes the submodule generated by a union.
|
LieSubmodule.wellFounded_of_noetherian
theorem LieSubmodule.wellFounded_of_noetherian :
∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : IsNoetherian R M],
WellFounded fun x x_1 => x > x_1
This theorem states that for any types `R`, `L`, and `M`, given a commutative ring structure on `R`, a Lie ring structure on `L`, an additively commutative group structure on `M`, a module structure of `R` on `M`, a Lie ring module structure of `L` on `M`, and assuming that `M` is a Noetherian module over `R`, the relation "greater than" (`>`) on the elements of `M` is well-founded. In simpler terms, this theorem is about the order structure of modules in the context of Lie algebras, and it says that if a module is Noetherian, then there are no infinitely descending chains, which is a property known as well-foundedness.
More concisely: Given a commutative ring `R`, a Lie ring `L`, an `R`-module `M` with Lie ring module structure and Noetherian condition, the "greater than" relation on `M` is well-founded.
|
Mathlib.Algebra.Lie.Submodule._auxLemma.52
theorem Mathlib.Algebra.Lie.Submodule._auxLemma.52 :
∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : LieRingModule L M] (N N' : LieSubmodule R L M), (N = N') = (↑N = ↑N')
This theorem, part of the Mathlib library in the section on algebra and Lie submodules, 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 any two Lie submodules `N` and `N'` of `M`, the equality `N = N'` is equivalent to the equality `↑N = ↑N'`. In other words, two Lie submodules are considered equal if and only if they are equal as sets.
Here `↑N` is the coercion of `N` to a set, so the theorem is about the equality of Lie submodules as set-theoretic subsets of `M`.
More concisely: For any commutative ring `R`, Lie ring `L`, and additive commutative group `M` that is an `R`-module, two Lie submodules `N` and `N'` of `M` are equal if and only if their set-theoretic representations `↑N` and `↑N'` are equal.
|
LieIdeal.map_le_iff_le_comap
theorem LieIdeal.map_le_iff_le_comap :
∀ {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'} {I : LieIdeal R L} {J : LieIdeal R L'},
LieIdeal.map f I ≤ J ↔ I ≤ LieIdeal.comap f J
The theorem `LieIdeal.map_le_iff_le_comap` establishes a correspondence between the mapping and comapping of Lie ideals in a Lie algebra. Specifically, for all types `R`, `L`, and `L'`; given a commutative ring `R`, Lie rings `L` and `L'`, and Lie algebras `L` and `L'` over `R`, a linear map `f : L →ₗ⁅R⁆ L'`, and Lie ideals `I` of `L` and `J` of `L'`; the image of the ideal `I` under the map `f` is a subset of the ideal `J` if and only if the ideal `I` is a subset of the preimage of `J` under `f`. This theorem is essentially a version of the fundamental theorem of Galois theory for Lie algebras.
More concisely: For a commutative ring R, Lie rings L and L', Lie algebras L and L' over R, a linear map f : L →ₗ⁅R⁆ L', and Lie ideals I of L and J of L': I ↴ f(I) ⊆ J if and only if I ⊆ f⁻¹(J).
|
LieIdeal.comap_map_le
theorem LieIdeal.comap_map_le :
∀ {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'} {I : LieIdeal R L},
I ≤ LieIdeal.comap f (LieIdeal.map f I)
The theorem `LieIdeal.comap_map_le` states that for any commutative ring `R`, Lie rings `L` and `L'`, Lie algebras `L` and `L'` over `R`, a homomorphism `f` from `L` to `L'`, and a Lie ideal `I` of `L`, `I` is contained in the preimage under `f` of the image under `f` of `I`. In other words, if you map the Lie ideal `I` from `L` to `L'` and then map back, you get something that contains `I`. It's related to the well-known property of functions that preimage of the image of a set is a superset of the original set. This theorem is a version of that property in the context of Lie algebras. This property is also necessary for the proof of another theorem, `LieIdeal.map_comap_eq`.
More concisely: Given a commutative ring `R`, Lie rings/algebras `L` and `L'`, a homomorphism `f` from `L` to `L'`, and a Lie ideal `I` of `L`, `f(I)` contains `I` in `L'`.
|
LieSubmodule.iSup_coe_toSubmodule
theorem LieSubmodule.iSup_coe_toSubmodule :
∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : LieRingModule L M] {ι : Sort u_1} (p : ι → LieSubmodule R L M),
↑(⨆ i, p i) = ⨆ i, ↑(p i)
This theorem states that for any commutative ring `R`, any Lie ring `L`, and any additive commutative group `M` that is also a `R`-module and a `L`-module, for any indexing sort `ι` and any function `p` from `ι` to the set of Lie submodules of `M`, the Lie submodule generated by the union of all `p i` (for all `i` in `ι`) is the same as the union of all Lie submodules `p i`. In simpler terms, the Lie submodule generated by all `p i` is equivalent to the union of all the individual Lie submodules `p i`.
More concisely: For any commutative ring `R`, Lie ring `L`, additive commutative group `M` (an `R`-module and `L-module`), and indexing sort `ι`, the Lie submodule of `M` generated by the union of Lie submodules `p i` (for all `i` in `ι`) is equal to the union of those submodules themselves.
|
LieHom.isIdealMorphism_def
theorem LieHom.isIdealMorphism_def :
∀ {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.IsIdealMorphism ↔ lieIdealSubalgebra R L' f.idealRange = f.range
The theorem `LieHom.isIdealMorphism_def` says that for any given commutative ring `R`, Lie rings `L` and `L'`, and `L` and `L'` being Lie algebras over the ring `R`, a morphism `f` from `L` to `L'` is an ideal morphism if and only if the ideal of `L'` generated by the image of `f` is equal to the image of `f` as a Lie subalgebra. This equivalence serves as the definition for an ideal morphism in the context of Lie algebras. Here, the image of `f` refers to the set of all elements in `L'` that can be obtained by applying `f` to elements in `L`.
More concisely: A morphism between two Lie algebras over a commutative ring is an ideal morphism if and only if the image of the morphism generates the same ideal in the target Lie algebra as the image itself.
|
LieSubmodule.coe_toSubmodule_eq_iff
theorem LieSubmodule.coe_toSubmodule_eq_iff :
∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : LieRingModule L M] (N N' : LieSubmodule R L M), ↑N = ↑N' ↔ N = N'
This theorem states that for any two Lie Submodules `N` and `N'` of a Module `M` over a Commutative Ring `R` with a Lie Ring `L`, the coercion of `N` to a Submodule is equal to the coercion of `N'` to a Submodule if and only if `N` is equal to `N'`. Here, the module `M` is equipped with the structure of a Lie Ring Module over `L`. This connects the equivalence of Lie Submodules with their equivalence as Submodules when coerced.
More concisely: For any Lie Submodules N and N' of a Lie Ring Module M over a commutative ring R, the coercions of N and N' to Submodules of M are equal if and only if N = N'.
|
LieSubalgebra.coe_toLieSubmodule
theorem LieSubalgebra.coe_toLieSubmodule :
∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
(K : LieSubalgebra R L), ↑K.toLieSubmodule = K.toSubmodule
The theorem `LieSubalgebra.coe_toLieSubmodule` states that for any commutative ring `R` and any Lie algebra `L` over `R`, if `K` is a Lie subalgebra of `L`, then the coercion of the Lie submodule associated with `K` (obtained by viewing `L` as a `K`-module by restriction) is equal to the submodule of `L` associated with `K`. In other words, the Lie submodule of `L` that `K` naturally induces is precisely the submodule of `L` that `K` spans.
More concisely: For any commutative ring R and Lie algebra L over R, the coercion of a Lie subalgebra K's associated Lie submodule in L is equal to the submodule of L spanned by K.
|
LieSubmodule.lieSpan_le
theorem LieSubmodule.lieSpan_le :
∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : LieRingModule L M] {s : Set M} {N : LieSubmodule R L M},
LieSubmodule.lieSpan R L s ≤ N ↔ s ⊆ ↑N
The theorem `LieSubmodule.lieSpan_le` states that, for any commutative ring `R`, Lie ring `L`, additively commutative group `M`, with `M` as a module over `R` and as a Lie ring module over `L`, any set `s` of elements of `M`, and any Lie submodule `N` of `M`, the Lie span of `s` is a subset of `N` if and only if `s` is a subset of `N`. This means that the smallest Lie submodule that contains `s` is contained in `N` precisely when `s` itself is contained in `N`.
More concisely: For any commutative ring R, Lie ring L, additively commutative group M as an R-module and Lie module over L, a set s of elements in the Lie module M, and a Lie submodule N of M, the Lie span of s is contained in N if and only if s is contained in N.
|
LieSubmodule.mem_coeSubmodule
theorem LieSubmodule.mem_coeSubmodule :
∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) {x : M}, x ∈ ↑N ↔ x ∈ N
This theorem, `LieSubmodule.mem_coeSubmodule`, states that for any given commutative ring `R`, Lie ring `L`, and additive commutative group `M` with `M` being a module over `R` and a Lie ring module over `L`, a certain element `x` of `M` is in the set underlying a Lie submodule `N` if and only if `x` is an element of the Lie submodule `N`. In other words, it asserts the equivalence of the membership of `x` in the underlying set of `N` and in the submodule `N` itself.
More concisely: For any commutative ring R, Lie ring L, additive commutative group M being an L-Lie module over L, the element x of M is in the underlying set of a Lie submodule N if and only if x is in N as a submodule.
|
LieSubmodule.mem_top
theorem LieSubmodule.mem_top :
∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : LieRingModule L M] (x : M), x ∈ ⊤
This theorem states that for any given types R, L, and M, where R is a commutative ring, L is a Lie ring, M is an additive commutative group, M is also an R-module, and M is an L-Lie ring module, any element x of type M belongs to the top or universal Lie submodule. This is a restatement of the universal property of the "top" (universal) element in the lattice structure of submodules, which says that every element of the parent module is contained in this top submodule.
More concisely: For any commutative ring R, Lie ring L, additive commutative group M being an R-module and an L-Lie ring module, every element of M belongs to the top (universal) Lie submodule of M as an L-Lie submodule.
|
LieSubmodule.bot_coeSubmodule
theorem LieSubmodule.bot_coeSubmodule :
∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : LieRingModule L M], ↑⊥ = ⊥
This theorem states that, for any commutative ring `R`, Lie ring `L`, and additive commutative group `M`, with `M` also being a module over `R` and a Lie ring module over `L`, the Lie submodule generated by the empty set (denoted as `⊥`) is equal to the bottom element of the lattice of submodules (also denoted as `⊥`). This essentially shows that the smallest possible Lie submodule is the one that contains no elements.
More concisely: For any commutative ring `R`, Lie ring `L`, and additive commutative group `M` being an `R`-module and a Lie ring module over `L`, the Lie submodule generated by the empty set of `M` equals the bottom element of the lattice of Lie submodules of `M`.
|
LieSubmodule.subsingleton_iff
theorem LieSubmodule.subsingleton_iff :
∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : LieRingModule L M], Subsingleton (LieSubmodule R L M) ↔ Subsingleton M
This theorem states that for any given types `R`, `L`, `M` where `R` is a commutative ring, `L` is a Lie Ring, and `M` is an additive commutative group with a module structure over `R` and a Lie Ring module structure over `L`, the type `LieSubmodule R L M` is a subsingleton if and only if `M` is a subsingleton. In other words, there is at most one Lie submodule of `M` (under the stated conditions) if and only if `M` itself has at most one element.
More concisely: For a commutative ring `R`, a Lie Ring `L`, and an additive commutative group `M` with module and Lie Ring module structures over `R`, the unique Lie submodule of `M` (if it exists) is isomorphic to `M` itself if and only if `M` is a singleton.
|
LieHom.idealRange_eq_map
theorem LieHom.idealRange_eq_map :
∀ {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.idealRange = LieIdeal.map f ⊤
The theorem `LieHom.idealRange_eq_map` states that for any commutative ring `R`, Lie rings `L` and `L'`, and a Lie algebra morphism `f` from `L` to `L'` (where `L` and `L'` are Lie algebras over `R`), the ideal range of `f` is equal to the image of the top ideal in `L` under `f`. In other words, `f` maps the top (or universal) ideal of `L` onto the ideal generated by the range of `f` in `L'`.
More concisely: For any commutative ring `R`, Lie algebras `L` and `L'`, and a Lie algebra morphism `f` from `L` to `L'`, the image of the top ideal in `L` under `f` generates the ideal range of `f` in `L'`.
|
LieSubmodule.subset_lieSpan
theorem LieSubmodule.subset_lieSpan :
∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : LieRingModule L M] {s : Set M}, s ⊆ ↑(LieSubmodule.lieSpan R L s)
This theorem states that for any types `R`, `L`, and `M` where `R` is a commutative ring, `L` is a Lie ring, `M` is an additive commutative group that is also a module over `R` and a Lie ring module over `L`, and given a set `s` of elements from `M`, the set `s` is a subset of the Lie span of `s`. In mathematical terms, if we consider `M` as a Lie submodule, then for any subset `s` of `M`, all elements of `s` are also elements of the smallest possible Lie submodule that contains `s` (the Lie span of `s`).
More concisely: For any commutative ring `R`, Lie ring `L`, and an additive commutative group `M` that is an `R`-module and a Lie ring module over `L`, every subset `s` of `M` is contained in the Lie span of `s`.
|
LieSubmodule.top_coeSubmodule
theorem LieSubmodule.top_coeSubmodule :
∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] [inst_4 : LieRingModule L M], ↑⊤ = ⊤
This theorem is about Lie algebras and 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 submodule generated by the entire space (denoted by `⊤`) is equal to the entire space itself. In other words, in the given context, every element of the space is, by definition, in the Lie submodule generated by the entire space.
More concisely: For any commutative ring `R`, Lie ring `L`, and additive commutative group `M` being an `R`-module and a Lie `L`-module, the Lie submodule generated by `M` equals `M` itself.
|