Minimal polynomials in torsion-free algebras

Over an integrally closed domain R, the minimal polynomial of an integral element of a torsion-free commutative R-algebra divides every polynomial annihilating that element. The algebra may have zero divisors or nilpotents. This permits minimal equations to be used for finite torsion-free algebras without passing to their domain quotients.

The argument extends the fraction-field comparison in minpoly.isIntegrallyClosed_eq_field_fractions: Gauss's lemma descends the monic minimal polynomial from a fraction-field algebra, and torsion-freeness makes the localization injective. No irreducibility of the minimal polynomial is asserted.

theorem TauCeti.minpoly.isIntegrallyClosed_eq_field_fractions_of_injective {R : Type u_1} {S : Type u_2} [CommRing R] [IsIntegrallyClosed R] [CommRing S] [Algebra R S] (K : Type u_3) [Field K] [Algebra R K] [IsFractionRing R K] {L : Type u_4} [CommRing L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] (φ : S →ₐ[R] L) (hφ : Function.Injective ⇑φ) {s : S} (hs : IsIntegral R s) : minpoly K (φ s) = Polynomial.map (algebraMap R K) (minpoly R s)

The minimal polynomial over an integrally closed domain of an integral element commutes with an injection into an algebra over its fraction field. The target algebra need not be a domain or reduced.

theorem TauCeti.minpoly.isIntegrallyClosed_dvd_of_isTorsionFree {R : Type u_1} {S : Type u_2} [CommRing R] [IsIntegrallyClosed R] [CommRing S] [Algebra R S] [IsDomain R] [Module.IsTorsionFree R S] {s : S} (hs : IsIntegral R s) {p : Polynomial R} (hp : (Polynomial.aeval s) p = 0) : minpoly R s ∣ p

In a torsion-free commutative algebra over an integrally closed domain, the minimal polynomial of an integral element divides every polynomial annihilating it. This includes algebras with zero divisors and nilpotents.