2 The Quotient Isomorphism
This chapter establishes that when \(R[\beta ] = S\) for a finite free extension, the natural map \(R[X]/(\operatorname {minpoly}_R \beta ) \to S\) is an isomorphism, without assuming \(R\) is integrally closed.
2.1 Degree Bound via Cayley–Hamilton
Let \(R \to S\) be a finite free extension with \(R\) nontrivial. For any \(\alpha \in S\),
Let \(\ell _\alpha = \operatorname {Algebra.lmul}_R\, \alpha \) be the left-multiplication endomorphism. By Cayley–Hamilton (\(\mathtt{LinearMap.aeval\_ self\_ charpoly}\)), \(\operatorname {aeval}_\alpha (\operatorname {charpoly}(\ell _\alpha )) = 0\). Since \(\operatorname {charpoly}(\ell _\alpha )\) is monic, the minimal polynomial divides it, so \(\deg (\operatorname {minpoly}_R \alpha ) \le \deg (\operatorname {charpoly}(\ell _\alpha )) = \operatorname {finrank}_R S\).
2.2 The Isomorphism via Orzech’s Property
Let \(R \to S\) be a finite free extension with \(R\) nontrivial, and let \(\alpha \in S\) with \(R[\alpha ] = S\). Then \(f = \operatorname {minpoly}_R \alpha \) is monic, and the natural map
is an \(R\)-algebra isomorphism. In particular, \(S\) admits an \(\mathtt{IsAdjoinRootMonic}\) structure for \(f\).
The map \(\varphi \) is well-defined since \(f(\alpha ) = 0\), and surjective since \(R[\alpha ] = S\).
Rank equality. The upper bound \(\deg f \le \operatorname {finrank}_R S\) follows from Lemma 1. For the lower bound, consider the surjection \(\varphi \). By the quotient rank formula (\(\mathtt{finrank\_ quotient\_ }\allowbreak \mathtt{span\_ eq\_ natDegree'}\)), \(\operatorname {finrank}_R(R[X]/(f)) = \deg f\). Since \(\varphi \) is surjective, \(\operatorname {finrank}_R S \le \operatorname {finrank}_R(R[X]/(f)) = \deg f\). Hence \(\deg f = \operatorname {finrank}_R S\).
Injectivity. Since both \(R[X]/(f)\) and \(S\) are free \(R\)-modules of the same finite rank, and \(\varphi \) is surjective, the composite \(e^{-1} \circ \varphi \) is a surjective endomorphism of a finitely generated free module (where \(e\) is a linear equivalence from the rank equality). By \(\mathtt{OrzechProperty.}\allowbreak \mathtt{injective\_ of\_ surjective\_ endomorphism}\) (which holds for all commutative rings), this composite is injective, hence \(\varphi \) is injective.