I would like to see a constructive proof (some algorithm?) of the following statement:
Let $A_1, A_2 \cdots ,A_k \in M_n(\mathbb C)$$A_1, A_2, \dotsc ,A_k \in M_n(\mathbb C)$ be some commuting matrices, let $B$ be the commutative algebra (with identity) over $\mathbb C$ generated by $A_1, A_2, \cdots, A_k$$A_1, A_2, \dotsc, A_k$. Suppose $E \in B$ is not invertableinvertible, then $I = (E)$ is a proper ideal of $B$. There existexists a maximal ideal $J$ of $B$ such that $I \subset J$.
I know we can prove the existence of maximal ideal of general commutative rings using the axiom of choice, but I think when dealing with concrete examples, a constructive proof can give us more insights.
In fact, I am trying to apply the proof Gelfand's theory of commutative Banach algebras to the special case of matrix algebras. The existence of maximal ideals is a key fact that estabilishes properties of Gelfand transform. In my experience, applying abstract proofs to concrete examples can always help us gain a better understanding. For example, I am very happy to see a finite-dimensional version of Gelfand-MazurGelfand–Mazur theorem.
Actually I asked a somewhat related question somewhat related questionConstruct maximal ideal in multivariate polynomial ring in MSE, asking for constructive proofs for maximal ideals in multivariate polynomial algebra (since the matrix algebra is quotient algebra of multivariate polynomial algebra). However, the matrix algebra case is what I really concerned.
I have limited knowledges in algebra, so this may be a very simple question. Thank you very much if you would like to help.