LieSubmodule.Quotient.mk_bracket
theorem LieSubmodule.Quotient.mk_bracket :
∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I : LieIdeal R L}
(x y : L), LieSubmodule.Quotient.mk ⁅x, y⁆ = ⁅LieSubmodule.Quotient.mk x, LieSubmodule.Quotient.mk y⁆
The theorem `LieSubmodule.Quotient.mk_bracket` states that for any commutative ring `R`, Lie ring `L`, and Lie algebra of `L` over `R`, the Lie bracket of two elements `x` and `y` in the Lie ideal `I` of `L` remains the same even when the elements are mapped to the quotient space `M/N` of the Lie submodule `N`. In other words, the Lie bracket operation is well-defined under the quotient map of the Lie submodule.
More concisely: The Lie bracket of elements in a Lie ideal of a Lie algebra is invariant under the quotient map of the Lie submodule.
|
LieSubmodule.Quotient.is_quotient_mk
theorem LieSubmodule.Quotient.is_quotient_mk :
∀ {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} (m : M),
Quotient.mk'' m = LieSubmodule.Quotient.mk m
This theorem 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`, given any Lie submodule `N` of `M`, the Quotient of any element `m` of `M` by the equivalence relation on `M` induced by `N` using the `Quotient.mk''` function is the same as the result of applying the `LieSubmodule.Quotient.mk` function to `m`. In other words, the `Quotient.mk''` function and `LieSubmodule.Quotient.mk` function are equivalent for Lie submodules.
More concisely: For any commutative ring `R`, Lie ring `L`, additive commutative group `M` that is both an `R`-module and a Lie ring module over `L`, and any Lie submodule `N` of `M`, the Quotient of any `m` in `M` by the equivalence relation induced by `N` is equivalent to the Lie submodule quotient of `m` by `N`.
|
LieSubmodule.Quotient.lieModuleHom_ext
theorem LieSubmodule.Quotient.lieModuleHom_ext :
∀ {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]
(N : LieSubmodule R L M) ⦃f g : M ⧸ N →ₗ⁅R,L⁆ M⦄,
f.comp (LieSubmodule.Quotient.mk' N) = g.comp (LieSubmodule.Quotient.mk' N) → f = g
This theorem states that in the context of a commutative ring `R`, a Lie ring `L`, a Lie algebra `R L`, an additive commutative group `M`, a module `R M`, a Lie ring module `L M`, and a Lie module `R L M`, given a Lie submodule `N` of `R L M`, two Lie module homomorphisms `f` and `g` from the quotient module `M/N` to `M` are equal if their compositions with the function `LieSubmodule.Quotient.mk'` (which maps `M` to the quotient module `M/N`) are equal. In other words, if applying `LieSubmodule.Quotient.mk'` followed by `f` gives the same result as applying `LieSubmodule.Quotient.mk'` followed by `g` , then `f` and `g` must be the same.
More concisely: Given a commutative ring `R`, a Lie ring `L`, a Lie module `R L M` over `M`, and a Lie submodule `N` of `R L M`, if for all `x` in `M`, `LieSubmodule.Quotient.mk' x = LieSubmodule.Quotient.mk' x` in `M/N` implies that `f(x) = g(x)` in `M`, then `f` and `g` are the same Lie module homomorphisms from `M/N` to `M`.
|