seen to be invariant—because . The quotient module is then the finite-dimensional irreducible representation of of dimension Definition of Verma modules There are two standard constructions of the Verma module, both of which involve the concept of universal enveloping algebra. We continue the notation of the previous section: is a complex semisimple Lie algebra, is a fixed Cartan subalgebra, is the associated root system with a fixed set of positive roots. For each , we choose nonzero elements and . As a quotient of the enveloping algebra The first construction of the Verma module is a quotient of the universal enveloping algebra of . Since the Verma module is supposed to be a -module, it will also be a -module, by the universal property of the enveloping algebra. Thus, if we have a Verma module with highest weight vector , there will be a linear map from into given by . Since is supposed to be generated by , the map should be surjective. Since is supposed to be a highest weight vector, the kernel of should include all the root vectors for in . Since, also, is supposed to be a weight vector with weight , the kernel of should include all vectors of the form . Finally, the kernel of should be a left ideal in ; after all, if then for all . The previous discussion motivates the following construction of Verma module. We define as the quotient vector space , where is the left ideal generated by all elements of the form and . Because is a left ideal, the natural left action of on itself carries over to the quotient. Thus, is a -module and therefore also a -module. By extension of scalars The "extension of scalars" procedure is a method for changing a left module over one algebra (not necessarily commutative) into a left module over a larger algebra that contains as a subalgebra. We can think of as a right -module, where acts on by multiplication on the right. Since is a left -module and is a right -module, we can form the tensor product of the two over the algebra : . Now, since is a left -module over itself, the above tensor product carries a left module structure over the larger algebra , uniquely determined by the requirement that for all and in . Thus, starting from the left -module ,