theorem UniversalEnvelopingAlgebra.algHom_ext' {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {A : Type u_3} [Ring A] [Algebra R A] {g₁ g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A} (h : ∀ (x : L), g₁ ((ι R) x) = g₂ ((ι R) x)) : g₁ = g₂

def LieSubmodule.preservingSubalgebra {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] (N : LieSubmodule R L M) : Subalgebra R (UniversalEnvelopingAlgebra R L)

theorem LieSubmodule.preservingSubalgebra_eq_top {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] (hcompat : ∀ (x : L) (m : M), ⁅x, m⁆ = (UniversalEnvelopingAlgebra.ι R) x • m) (N : LieSubmodule R L M) : N.preservingSubalgebra = ⊤

def LieSubmodule.toUEASubmodule {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] (hcompat : ∀ (x : L) (m : M), ⁅x, m⁆ = (UniversalEnvelopingAlgebra.ι R) x • m) (N : LieSubmodule R L M) : Submodule (UniversalEnvelopingAlgebra R L) M

theorem LieSubmodule.mem_toUEASubmodule {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] (hcompat : ∀ (x : L) (m : M), ⁅x, m⁆ = (UniversalEnvelopingAlgebra.ι R) x • m) (N : LieSubmodule R L M) (m : M) : m ∈ toUEASubmodule hcompat N ↔ m ∈ N

theorem LieSubmodule.toUEASubmodule_bot {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] (hcompat : ∀ (x : L) (m : M), ⁅x, m⁆ = (UniversalEnvelopingAlgebra.ι R) x • m) : toUEASubmodule hcompat ⊥ = ⊥

theorem LieSubmodule.toUEASubmodule_top {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] (hcompat : ∀ (x : L) (m : M), ⁅x, m⁆ = (UniversalEnvelopingAlgebra.ι R) x • m) : toUEASubmodule hcompat ⊤ = ⊤

def LieSubmodule.ofUEASubmodule' {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] (hcompat : ∀ (x : L) (m : M), ⁅x, m⁆ = (UniversalEnvelopingAlgebra.ι R) x • m) (N : Submodule (UniversalEnvelopingAlgebra R L) M) : LieSubmodule R L M

theorem LieSubmodule.toUEASubmodule_ofUEASubmodule' {R : Type u_1} [CommRing R] {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] (hcompat : ∀ (x : L) (m : M), ⁅x, m⁆ = (UniversalEnvelopingAlgebra.ι R) x • m) (N : Submodule (UniversalEnvelopingAlgebra R L) M) : toUEASubmodule hcompat (ofUEASubmodule' hcompat N) = N