# Commit 2023-11-17 13:15 8dba065d

View on Github →chore(IntegralClosure): noncommutative generalizations and golfs (#8406)
Zulip
Initially I just wanted to add more dot notations for IsIntegral and IsAlgebraic (done in #8437); then I noticed near-duplicates
Algebra.isIntegral_of_finite `[Field R] [Ring A]`

and
RingHom.IsIntegral.of_finite `[CommRing R] [CommRing A]`

so I went on to generalize the latter to cover the former, and generalized everything in the IntegralClosure file to the noncommutative case whenever possible.
In the process I noticed more golfs, which result in this PR. Most notably, isIntegral_of_mem_of_FG is now proven using Cayley-Hamilton and doesn't depend on the Noetherian case isIntegral_of_noetherian; the latter is now proven using the former. In total the golfs makes mathlib 227 lines leaner (+487 -714).
The main changes are in the single file RingTheory/IntegralClosure:

- Change the definition of
`Algebra.IsIntegral`

which makes it unfold to`IsIntegral`

rather than`RingHom.IsIntegralElem`

because the former has much more APIs. - Fix lemma names involving
`is_integral`

which are actually about`IsIntegralElem`

:`RingHom.is_integral_map`

→`RingHom.isIntegralElem_map`

`RingHom.is_integral_of_mem_closure`

→`RingHom.IsIntegralElem.of_mem_closure`

`RingHom.is_integral_zero/one`

→`RingHom.isIntegralElem_zero/one`

`RingHom.is_integral_add/neg/sub/mul/of_mul_unit`

→`RingHom.IsIntegralElem.add/neg/sub/mul/of_mul_unit`

- Add a lemma
`Algebra.IsIntegral.of_injective`

. - Move
`isIntegral_of_(submodule_)noetherian`

down and golf them. - Remove
`(Algebra.)isIntegral_of_finite`

that work only over fields, in favor of the more general`(Algebra.)isIntegral.of_finite`

. - Merge duplicate lemmas
`isIntegral_of_isScalarTower`

and`isIntegral_tower_top_of_isIntegral`

into`IsIntegral.tower_top`

. - Golf
`IsIntegral.of_mem_of_fg`

by first proving`IsIntegral.of_finite`

using Cayley-Hamilton. - Add a docstring mentioning the Kurosh problem at
`Algebra.IsIntegral.finite`

. The negative solution to the problem means the theorem doesn't generalize to noncommutative algebras. - Golf
`IsIntegral.tmul`

and`isField_of_isIntegral_of_isField(')`

. - Combine
`isIntegral_trans_aux`

into`isIntegral_trans`

and golf. - Add
`Algebra`

namespace to`isIntegral_sup`

. - rename lemmas for dot notation:
`RingHom.isIntegral_trans`

→`RingHom.IsIntegral.trans`

`RingHom.isIntegral_quotient/tower_bot/top_of_isIntegral`

→`RingHom.IsIntegral.quotient/tower_bot/top`

`isIntegral_of_mem_closure'`

→`IsIntegral.of_mem_closure'`

(and the '' version)`isIntegral_of_surjective`

→`Algebra.isIntegral_of_surjective`

The next changed file is RingTheory/Algebraic: - Rename:
`of_larger_base`

→`tower_top`

(for consistency with`IsIntegral`

)`Algebra.isAlgebraic_of_finite`

→`Algebra.IsAlgebraic.of_finite`

`Algebra.isAlgebraic_trans`

→`Algebra.IsAlgebraic.trans`

- Add new lemmas
`Algebra.IsIntegral.isAlgebraic`

,`isAlgebraic_algHom_iff`

, and`Algebra.IsAlgebraic.of_injective`

to streamline some proofs. The generalization from CommRing to Ring requires an additional lemma`scaleRoots_eval₂_mul_of_commute`

in Polynomial/ScaleRoots. A lemma`Algebra.lmul_injective`

is added to Algebra/Bilinear (in order to golf the proof of`IsIntegral.of_mem_of_fg`

). In all other files, I merely fix the changed names, or use newly available dot notations.