Maximal and primitive weights in integrable category O modules

If $V\mathrm{\ne }0$, take any support weight $\mu$. The finite nonempty set of support weights above $\mu$ has a maximal element $\lambda$, which is also globally maximal: any larger support weight would still belong to that finite set. For any nonzero $v\in V_{\lambda }$, every positive root vector kills $v$, because its image would have a strictly larger weight. Thus $v$ is highest. Its cyclic submodule inherits the weight decomposition by F1, and both simple local nilpotences by restriction from $V$. It is integrable, so F2 makes $\lambda$ dominant integral. F4 makes this cyclic module a highest-weight Verma quotient.

If $v$ is primitive of weight $\lambda$, choose its witnessing submodule $N$ from F3. The quotient $V\mathrm{/}N$ is a weight module by F1. Both simple local nilpotences descend: each quotient vector has a preimage and every power killing that preimage also kills its class. Its cyclic module generated by the specified nonzero highest class of $v$ is therefore integrable. Apply F2 to obtain $\lambda \in P^{+}$. This proves dominance for every primitive vector, without claiming that the original representative is itself highest in $V$.

By F3, every vector of $V$ is a finite sum of negative enveloping words applied to primitive vectors. Step 1.2 proves that all the generating weights in this assertion are dominant integral. Step 1.1 supplies the maximal-weight case and the Verma quotient description. The assertion for $V=0$ is the empty span. In a one-weight module the positive generators vanish and each nonzero vector is already highest. Zero labels are allowed by F2. The existence of one maximal element in a fixed finite upper set and one witness for a fixed primitive vector requires no arbitrary choice family; no AC is used.