[Merged by Bors] - chore(IntegralClosure, Algebraic): renames, noncommutative generalizations and golfs #8406

alreadydone · 2023-11-14T10:23:50Z

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.
Add aliases (Algebra.)IsAlgebraic.IsIntegral (in the field case).

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.

alreadydone · 2023-11-14T16:46:52Z

!bench

alreadydone · 2023-11-14T17:17:08Z

Mathlib/RingTheory/IntegralClosure.lean

+  let S := adjoin R (p.frange : Set A)
+  have : Module.Finite R S := ⟨(Subalgebra.toSubmodule S).fg_top.mpr <|
+    fg_adjoin_of_finite p.frange.finite_toSet fun a _ ↦ A_int a⟩
+  let p' : S[X] := p.toSubring S.toSubring fun a ha ↦ subset_adjoin ha
+  have hSx : IsIntegral S x := ⟨p', (p.monic_toSubring _ _).mpr pmonic, by
+    rw [IsScalarTower.algebraMap_eq S A B, ← eval₂_map]
+    convert hp; apply p.map_toSubring S.toSubring⟩
+  let Sx := Subalgebra.toSubmodule (adjoin S {x})
+  let MSx : Module S Sx := SMulMemClass.toModule _ -- the next line times out without this
+  have : Module.Finite S Sx := ⟨(Submodule.fg_top _).mpr hSx.fg_adjoin_singleton⟩
+  refine .of_mem_of_fg ((adjoin S {x}).restrictScalars R) ?_ _
+    ((Subalgebra.mem_restrictScalars R).mpr <| subset_adjoin rfl)
+  rw [← Submodule.fg_top, ← Module.finite_def]
+  letI : SMul S Sx := { MSx with } -- need this even though MSx is there
+  have : IsScalarTower R S Sx :=
+    Submodule.isScalarTower Sx -- Lean looks for `Module A Sx` without this


Some typeclass inference failures that may be worth investigating (but are probably well known)

alreadydone · 2023-11-14T23:51:27Z

cc:

original author of isIntegral_of_mem_of_FG @kckennylau
@erdOne who introduced the generalized Cayley-Hamilton LinearMap.exists_monic_and_aeval_eq_zero allowing to golf the above 97-line proof down to 1+2 lines (I guess it wasn't golfed due to Module.End being noncommutative?). I tried to golf your isIntegral_of_smul_mem_submodule as well using Algebra.lsmul, but Lean has trouble inferring instances involving a submodule, requiring manually writing out some instances, so I gave up and left it alone.
original author of isField_of_isIntegral_of_isField @dtumad: I'm indeed able to use the Polynomial.reverse and Polynomial.DivX API
original author of isIntegral_trans_aux @jcommelin (the aux lemma doesn't allow noncommutative B, so it's now removed, and the main proof now adjoins elements in A rather than in B)
@eric-wieser @haruhisa-enomoto who may be interested in the noncommutative generalization

eric-wieser · 2023-11-15T00:44:21Z

Is it possible to split the dot notation changes to their own PR? It would be much better if the mathematical and stylistic content were in separate reviews.

alreadydone · 2023-11-15T03:49:01Z

Mathlib/RingTheory/IntegralClosure.lean

-variable [CommRing R] [CommRing A] [CommRing B] [CommRing S]
+variable [CommRing R] [CommRing A] [Ring B] [CommRing S]


The only change to lemma statements is here.

alreadydone · 2023-11-15T04:01:59Z

Is it possible to split the dot notation changes to their own PR? It would be much better if the mathematical and stylistic content were in separate reviews.

As I said on Zulip:

The PR golfs some long proofs which collectively makes mathlib4 226 lines leaner, but only adds two new lemmas, removes an auxiliary lemma, and deduplicates some lemmas, so it's hopefully not hard to review.
The PR can't be easily split, as the renamed/reordered lemmas are also used in the golfs.

There is not much "mathematical content" because all I did to the lemma statements is here (replacing [CommRing] by [Ring]). Lemmas may be moved (reordered), golfed, and deduplicated, but the statements are only changed (generalized) in this way, and these are all concentrated in the single file RingTheory/IntegralClosure (plus one lemma in Polynomial/ScaleRoots and Algebra/Bilinear each).

On the other hand, the stylistic (dot notation) changes require fixing lots of files, but those fixes are trivial to review. If I first introduce dot notation in a separate PR, I'll need to fix long proofs (e.g. isIntegral_of_mem_of_FG) that will simply be completely removed in the subsequent golfing PR. If I first do the golfs in a separate PR, I'll need to use the old lemma names and switch to new lemma names in the subsequent dot notations PR. So both options don't seem very economic, though I would choose the second option if you insist on a split.

(I guess the "feat" in the PR title may cause misunderstanding; changed to "chore" now.)

alreadydone · 2023-11-17T05:30:13Z

@adomani's #8437 did part of the renames, but the following were not included:

In IntegralClosure:
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
RingHom.isIntegral_trans → RingHom.IsIntegral.trans
RingHom.isIntegral_quotient/tower_bot/top_of_isIntegral → RingHom.IsIntegral.quotient/tower_bot/top
isIntegral_sup → Algebra.isIntegral_sup
IsIntegral.of_mem_closure' → IsIntegral.of_mem_closure'
isIntegral_of_surjective → Algebra.isIntegral_of_surjective

In RingTheory/Algebraic:
of_larger_base → tower_top (for consistency with IsIntegral)
Algebra.isAlgebraic_of_finite → Algebra.IsAlgebraic.of_finite
Algebra.isAlgebraic_trans → Algebra.IsAlgebraic.trans

I also added a lemma Algebra.IsIntegral.of_injective in IntegralClosure and three in RingTheory/Algebraic: Algebra.IsIntegral.isAlgebraic, isAlgebraic_algHom_iff, and Algebra.IsAlgebraic.of_injective to streamline some proofs.

(Currently I can't easily use @j-loreaux's #8433 to generate decl name changes, because if I merge this PR directly into #8433's branch the diff generated would include new commits on master. If I first merge master into #8433's branch, then I need to wait for the cache, and then merge this PR into #8433 and wait for the cache again, which is time consuming.)

I also decided to make R implicit in IsIntegral.isAlgebraic, which resulted in more files needing to be fixed.

@adomani's PR means that the current changes in IntegralClosure and RingTheory/Algebraic only cause 24 files to break, so it's possible to split PR into one that changes 24 files and another one that changes 17 files (depending on the previous one, which would just be using the new dot notations to golf proofs), but I'm not sure it's worth doing; most diffs would still be in the first PR. If @adomani would do another renaming PR and include some changes in implicitness, then the number 24 would decrease and a split may be more attractive.

jcommelin · 2023-11-17T08:40:12Z

Can you please add the remaining renames to the PR commit message?

jcommelin · 2023-11-17T08:42:16Z

I'm inclined to merge this as is. Damiano's tool was a first success. And hopefully we can use it more in the future. But splitting up this PR seems like it will be a lot of work for comparatively little remaining gain.

alreadydone · 2023-11-17T09:43:39Z

Thanks @jcommelin! PR message edited.

adomani · 2023-11-17T10:14:49Z

The renames were an experiment to test an automated renaming tool. Since it was the first "real world" attempt, I aimed to rename only lemmas for which there was no dot-notation involved.

Currently, the tool finds the positions where the old declaration appears and replaces them with the new one. No fancy namespacing/dot-notation/removal-of-arguments is implemented.

I would like to add namespacing options, since that is easy to implement as a string-based replacement.

However, doing more context/syntax-aware changes is best done with a tool implemented in Lean.

The tool itself, reads the location of the syntax from the ilean files and then uses bash-commands to do the string replacements.

jcommelin · 2023-11-17T13:04:48Z

Thanks 🎉

bors merge

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238406.20IsIntegral.20dot.20notation.2C.20noncomm.20generalization.20.26.20golf/near/402028285) 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](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#Algebra.isIntegral_of_finite) `[Field R] [Ring A]` and [RingHom.IsIntegral.of_finite](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#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](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#isIntegral_of_mem_of_FG) is now proven using [Cayley-Hamilton](https://math.stackexchange.com/a/2494433/12932) and doesn't depend on the Noetherian case [isIntegral_of_noetherian](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#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](https://github.com/leanprover-community/mathlib4/pull/8406/files#diff-426d60d7e9edc9e20379127612410ad633864c2d5a9cd001729d128f0993b00e): + 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. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

… use dot notation (#8437) This PR tests a string-based tool for renaming declarations. Inspired by [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Renaming.20decls.20using.20LSP/near/402399853), I am trying to reduce the diff of #8406. This PR makes the following renames: | From | To |

mathlib-bors · 2023-11-17T14:03:51Z

Pull request successfully merged into master.

Build succeeded:

j-loreaux · 2023-11-17T14:15:56Z

@alreadydone yeah, #8433 is not usable until it's merged because it changes lakefile.lean. Sorry!

… use dot notation (#8437) This PR tests a string-based tool for renaming declarations. Inspired by [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Renaming.20decls.20using.20LSP/near/402399853), I am trying to reduce the diff of #8406. This PR makes the following renames: | From | To |

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238406.20IsIntegral.20dot.20notation.2C.20noncomm.20generalization.20.26.20golf/near/402028285) 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](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#Algebra.isIntegral_of_finite) `[Field R] [Ring A]` and [RingHom.IsIntegral.of_finite](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#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](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#isIntegral_of_mem_of_FG) is now proven using [Cayley-Hamilton](https://math.stackexchange.com/a/2494433/12932) and doesn't depend on the Noetherian case [isIntegral_of_noetherian](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#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](https://github.com/leanprover-community/mathlib4/pull/8406/files#diff-426d60d7e9edc9e20379127612410ad633864c2d5a9cd001729d128f0993b00e): + 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. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

… use dot notation (#8437) This PR tests a string-based tool for renaming declarations. Inspired by [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Renaming.20decls.20using.20LSP/near/402399853), I am trying to reduce the diff of #8406. This PR makes the following renames: | From | To |

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238406.20IsIntegral.20dot.20notation.2C.20noncomm.20generalization.20.26.20golf/near/402028285) 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](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#Algebra.isIntegral_of_finite) `[Field R] [Ring A]` and [RingHom.IsIntegral.of_finite](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#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](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#isIntegral_of_mem_of_FG) is now proven using [Cayley-Hamilton](https://math.stackexchange.com/a/2494433/12932) and doesn't depend on the Noetherian case [isIntegral_of_noetherian](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/IntegralClosure.html#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](https://github.com/leanprover-community/mathlib4/pull/8406/files#diff-426d60d7e9edc9e20379127612410ad633864c2d5a9cd001729d128f0993b00e): + 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. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

alreadydone added 6 commits November 13, 2023 03:45

feat: use dot notation for IsIntegral and noncommutative generalization

2468df5

more golfs / generalizations

510b86e

fix Algebraic

3a46595

fixes

4f7c307

huge golf

bd5d718

finish golfs

64c25fd

alreadydone added awaiting-review awaiting-CI t-algebra Algebra (groups, rings, fields, etc) WIP Work in progress labels Nov 14, 2023

alreadydone added 9 commits November 14, 2023 05:32

fixes

ebca3ba

fixes

11768a6

fix

a31622f

fix

7e20424

fixes

97697d7

fixes

d87211d

fix

c309c8f

fixes

b7eafd0

final fixes

eea6f6a

alreadydone removed awaiting-CI WIP Work in progress labels Nov 14, 2023

alreadydone added 2 commits November 14, 2023 11:18

actual final fix

7c8956d

remove a nonrec

e46659d

alreadydone commented Nov 14, 2023

View reviewed changes

another golf

bec003c

alreadydone commented Nov 15, 2023

View reviewed changes

alias IsAlgebraic.isIntegral

200178d

alreadydone added the awaiting-CI label Nov 16, 2023

alreadydone added 2 commits November 16, 2023 11:34

make R implicit in IsIntegral.isAlgebraic

297d2f8

fix

d9ba3f0

github-actions bot removed the awaiting-CI label Nov 16, 2023

alreadydone added 4 commits November 16, 2023 23:33

more lemmas

281e9f1

fix larger_base -> tower_top

9bb4fbe

protect

b7e1a0c

tinygolfs

2c064d4

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Nov 17, 2023

mathlib-bors bot changed the title ~~chore(IntegralClosure): noncommutative generalizations and golfs~~ [Merged by Bors] - chore(IntegralClosure): noncommutative generalizations and golfs Nov 17, 2023

mathlib-bors bot closed this Nov 17, 2023

mathlib-bors bot deleted the IsIntegral_dot branch November 17, 2023 14:04

alreadydone changed the title ~~[Merged by Bors] - chore(IntegralClosure): noncommutative generalizations and golfs~~ [Merged by Bors] - chore(IntegralClosure, Algebraic): renames, noncommutative generalizations and golfs Nov 17, 2023

alreadydone mentioned this pull request Nov 17, 2023

[Merged by Bors] - feat: IsNormalClosure predicate #8418

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore(IntegralClosure, Algebraic): renames, noncommutative generalizations and golfs #8406

[Merged by Bors] - chore(IntegralClosure, Algebraic): renames, noncommutative generalizations and golfs #8406

alreadydone commented Nov 14, 2023 •

edited

Loading

alreadydone commented Nov 14, 2023

alreadydone Nov 14, 2023

alreadydone commented Nov 14, 2023 •

edited

Loading

eric-wieser commented Nov 15, 2023

alreadydone Nov 15, 2023

alreadydone commented Nov 15, 2023 •

edited

Loading

alreadydone commented Nov 17, 2023 •

edited

Loading

jcommelin commented Nov 17, 2023

jcommelin commented Nov 17, 2023 •

edited

Loading

alreadydone commented Nov 17, 2023

adomani commented Nov 17, 2023 •

edited

Loading

jcommelin commented Nov 17, 2023

mathlib-bors bot commented Nov 17, 2023

j-loreaux commented Nov 17, 2023

		variable [CommRing R] [CommRing A] [CommRing B] [CommRing S]
		variable [CommRing R] [CommRing A] [Ring B] [CommRing S]

[Merged by Bors] - chore(IntegralClosure, Algebraic): renames, noncommutative generalizations and golfs #8406

[Merged by Bors] - chore(IntegralClosure, Algebraic): renames, noncommutative generalizations and golfs #8406

Conversation

alreadydone commented Nov 14, 2023 • edited Loading

alreadydone commented Nov 14, 2023

alreadydone Nov 14, 2023

Choose a reason for hiding this comment

alreadydone commented Nov 14, 2023 • edited Loading

eric-wieser commented Nov 15, 2023

alreadydone Nov 15, 2023

Choose a reason for hiding this comment

alreadydone commented Nov 15, 2023 • edited Loading

alreadydone commented Nov 17, 2023 • edited Loading

jcommelin commented Nov 17, 2023

jcommelin commented Nov 17, 2023 • edited Loading

alreadydone commented Nov 17, 2023

adomani commented Nov 17, 2023 • edited Loading

jcommelin commented Nov 17, 2023

mathlib-bors bot commented Nov 17, 2023

j-loreaux commented Nov 17, 2023

alreadydone commented Nov 14, 2023 •

edited

Loading

alreadydone commented Nov 14, 2023 •

edited

Loading

alreadydone commented Nov 15, 2023 •

edited

Loading

alreadydone commented Nov 17, 2023 •

edited

Loading

jcommelin commented Nov 17, 2023 •

edited

Loading

adomani commented Nov 17, 2023 •

edited

Loading