def nPosInvariants {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (W : Type u) [AddCommGroup W] [Module R W] [LieRingModule 𝔤 W] [LieModule R 𝔤 W] : Submodule R W

def singularVectorsOfWeight {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (W : Type u) [AddCommGroup W] [Module R W] [LieRingModule 𝔤 W] [LieModule R 𝔤 W] (wt : ↥Δ.𝔥 →ₗ[R] R) : Submodule R W

def verma_hom_forward {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {M : Type u} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] {wt : ↥Δ.𝔥 →ₗ[R] R} (hV : IsVermaModule Δ M wt) {W : Type u} [AddCommGroup W] [Module R W] [LieRingModule 𝔤 W] [LieModule R 𝔤 W] (φ : M →ₗ⁅R,𝔤⁆ W) : ↥(singularVectorsOfWeight Δ W wt)

noncomputable def verma_hom_backward {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {M : Type u} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] {wt : ↥Δ.𝔥 →ₗ[R] R} (hV : IsVermaModule Δ M wt) {W : Type u} [AddCommGroup W] [Module R W] [LieRingModule 𝔤 W] [LieModule R 𝔤 W] (w : ↥(singularVectorsOfWeight Δ W wt)) : M →ₗ⁅R,𝔤⁆ W

theorem verma_hom_backward_spec {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {M : Type u} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] {wt : ↥Δ.𝔥 →ₗ[R] R} (hV : IsVermaModule Δ M wt) {W : Type u} [AddCommGroup W] [Module R W] [LieRingModule 𝔤 W] [LieModule R 𝔤 W] (w : ↥(singularVectorsOfWeight Δ W wt)) : (verma_hom_backward hV w) hV.highestWeightVec = ↑w

theorem verma_hom_forward_backward {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {M : Type u} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] {wt : ↥Δ.𝔥 →ₗ[R] R} (hV : IsVermaModule Δ M wt) {W : Type u} [AddCommGroup W] [Module R W] [LieRingModule 𝔤 W] [LieModule R 𝔤 W] (w : ↥(singularVectorsOfWeight Δ W wt)) : verma_hom_forward hV (verma_hom_backward hV w) = w