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 lemmasAlgebra.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.

Estimated changes

added theorem Algebra.lmul_injective
modified theorem AlgEquiv.isAlgebraic
modified theorem AlgEquiv.isAlgebraic_iff
deleted theorem Algebra.isAlgebraic_trans
added theorem IsAlgebraic.tower_top
added theorem isAlgebraic_algHom_iff
added theorem Algebra.isIntegral_sup
deleted theorem IsIntegral.add
modified theorem IsIntegral.map_of_comp_eq
deleted theorem IsIntegral.mul
modified theorem IsIntegral.neg
modified theorem IsIntegral.nsmul
modified theorem IsIntegral.of_finite
deleted theorem IsIntegral.of_mem_closure
modified theorem IsIntegral.of_mem_of_fg
modified theorem IsIntegral.of_mul_unit
modified theorem IsIntegral.of_pow
modified theorem IsIntegral.of_subring
modified theorem IsIntegral.pow
modified theorem IsIntegral.smul
deleted theorem IsIntegral.sub
added theorem IsIntegral.tower_top
modified theorem IsIntegral.zsmul
deleted theorem RingHom.isIntegral_trans
deleted theorem RingHom.is_integral_add
deleted theorem RingHom.is_integral_map
deleted theorem RingHom.is_integral_mul
deleted theorem RingHom.is_integral_neg
deleted theorem RingHom.is_integral_one
deleted theorem RingHom.is_integral_sub
deleted theorem RingHom.is_integral_zero
modified theorem integralClosure_idem
modified theorem isIntegral_algHom_iff
modified theorem isIntegral_of_noetherian
deleted theorem isIntegral_of_surjective
modified theorem isIntegral_one
deleted theorem isIntegral_sup
deleted theorem isIntegral_trans_aux
modified theorem isIntegral_zero