[Merged by Bors] - feat(RingTheory/AlgebraicIndependent): add `AlgebraicIndependent.aevalEquivField` and other results by acmepjz · Pull Request #18648 · leanprover-community/mathlib4

acmepjz · 2024-11-05T07:23:29Z

This PR mainly adds

AlgebraicIndependent.aevalEquivField: canonical isomorphism between rational function field and the intermediate field generated by algebraically independent elements.
AlgebraicIndependent.reprField: canonical map from the intermediate field generated by an algebraic independent family into the rational function field.

Other results:

AlgebraicIndependent.aeval_of_algebraicIndependent: if x = {x_i : A | i : ι} and f = {f_i : MvPolynomial ι R | i : ι} are algebraically independent over R, then {f_i(x) | i : ι} is also algebraically independent over R.
AlgebraicIndependent.of_aeval: conversely, if {f_i(x) | i : ι} is algebraically independent over R, then {f_i : MvPolynomial ι R | i : ι} is also algebraically independent over R.
AlgebraicIndependent.polynomial_aeval_of_transcendental: if {x_i : A | i : ι} is algebraically independent over R, and for each i, f_i : R[X] is transcendental over R, then {f_i(x_i) | i : ι} is also algebraically independent over R.
AlgebraicIndependent.isEmpty_of_isAlgebraic: if A/R is algebraic, then all algebraically independent families are empty.
IsTranscendenceBasis.isEmpty_iff_isAlgebraic: if x is a transcendence basis of A/R, then it is empty if and only if A/R is algebraic.
IsTranscendenceBasis.nonempty_iff_transcendental: if x is a transcendence basis of A/R, then it is not empty if and only if A/R is transcendental.
IsTranscendenceBasis.isAlgebraic_field: if x is a transcendence basis of E / F, then the field extension E / F(x) is algebraic.

Also add [of_]ringHom_of_comp_eq for [Algebra.]Transcendental and AlgebraicIndependent.

Also add some results for Subalgebra inspired by IntermediateField.isAlgebraic_iff. Some of them are not back-ported to IntermediateField yet; may be for another PR if they are useful.

github-actions · 2024-11-05T07:24:15Z

PR summary dc56cb32a9

Import changes exceeding 2%

%	File
+2.22%	`Mathlib.RingTheory.AlgebraicIndependent`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.AlgebraicIndependent	1350	1380	+30 (+2.22%)
Mathlib.RingTheory.Algebraic	1347	1346	-1 (-0.07%)

Import changes for all files

Files	Import difference
44 files `Mathlib.LinearAlgebra.FreeModule.Norm` `Mathlib.LinearAlgebra.Charpoly.Basic` `Mathlib.Analysis.InnerProductSpace.Spectrum` `Mathlib.RingTheory.PowerBasis` `Mathlib.LinearAlgebra.Matrix.PosDef` `Mathlib.Data.Real.GoldenRatio` `Mathlib.RingTheory.Adjoin.PowerBasis` `Mathlib.LinearAlgebra.Charpoly.ToMatrix` `Mathlib.FieldTheory.IntermediateField.Algebraic` `Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly` `Mathlib.Data.Real.Pi.Irrational` `Mathlib.NumberTheory.Rayleigh` `Mathlib.RingTheory.Unramified.Pi` `Mathlib.RingTheory.RingHom.FinitePresentation` `Mathlib.RingTheory.Algebraic` `Mathlib.Algebra.AlgebraicCard` `Mathlib.Data.Real.Irrational` `Mathlib.RingTheory.Smooth.Basic` `Mathlib.NumberTheory.Pell` `Mathlib.RingTheory.Smooth.Kaehler` `Mathlib.RingTheory.Unramified.Basic` `Mathlib.LinearAlgebra.AnnihilatingPolynomial` `Mathlib.LinearAlgebra.Matrix.LDL` `Mathlib.RingTheory.AdjoinRoot` `Mathlib.RingTheory.Smooth.Pi` `Mathlib.LinearAlgebra.Matrix.SchurComplement` `Mathlib.Topology.Instances.Irrational` `Mathlib.FieldTheory.Minpoly.Field` `Mathlib.Algebra.Module.LinearMap.Polynomial` `Mathlib.RingTheory.Etale.Basic` `Mathlib.Combinatorics.SimpleGraph.LapMatrix` `Mathlib.Algebra.Polynomial.Module.FiniteDimensional` `Mathlib.LinearAlgebra.Matrix.Spectrum` `Mathlib.Algebra.Lie.Rank` `Mathlib.Algebra.Polynomial.Bivariate` `Mathlib.LinearAlgebra.Eigenspace.Zero` `Mathlib.LinearAlgebra.Eigenspace.Minpoly` `Mathlib.FieldTheory.AxGrothendieck` `Mathlib.LinearAlgebra.Charpoly.BaseChange` `Mathlib.RingTheory.Unramified.Finite` `Mathlib.Algebra.Lie.CartanExists` `Mathlib.RingTheory.Localization.Away.AdjoinRoot` `Mathlib.NumberTheory.DiophantineApproximation` `Mathlib.Topology.Instances.RatLemmas`	-1
`Mathlib.FieldTheory.IsAlgClosed.Classification` `Mathlib.ModelTheory.Algebra.Field.IsAlgClosed`	1
`Mathlib.RingTheory.AlgebraicIndependent`	30

Declarations diff

+ Algebra.Transcendental.of_ringHom_of_comp_eq
+ Algebra.Transcendental.ringHom_of_comp_eq
+ Algebra.isAlgebraic_ringHom_iff_of_comp_eq
+ Algebra.transcendental_ringHom_iff_of_comp_eq
+ AlgebraicIndependent.of_ringHom_of_comp_eq
+ AlgebraicIndependent.polynomial_aeval_of_transcendental
+ AlgebraicIndependent.ringHom_of_comp_eq
+ IsTranscendenceBasis.isAlgebraic_field
+ IsTranscendenceBasis.isEmpty_iff_isAlgebraic
+ IsTranscendenceBasis.nonempty_iff_transcendental
+ MvPolynomial.algebraicIndependent_X
+ Transcendental.of_ringHom_of_comp_eq
+ Transcendental.ringHom_of_comp_eq
+ aevalEquiv
+ aevalEquivField
+ aevalEquivField_algebraMap_apply_coe
+ aevalEquivField_apply_coe
+ aeval_comp_repr
+ aeval_of_algebraicIndependent
+ aeval_repr
+ algebraMap_aevalEquiv
+ algebra_isAlgebraic_bot_left_iff
+ algebra_isAlgebraic_bot_right
+ algebra_isAlgebraic_of_algebra_isAlgebraic_bot_left
+ algebraicIndependent_ringHom_iff_of_comp_eq
+ isAlgebraic_bot_iff
+ isAlgebraic_iff_isAlgebraic_val
+ isAlgebraic_of_isAlgebraic_bot
+ isEmpty_of_isAlgebraic
+ liftAlgHom_comp_reprField
+ lift_reprField
+ of_aeval
+ repr
+ reprField
+ repr_ker
+ transcendental_ringHom_iff_of_comp_eq
- AlgebraicIndependent.aevalEquiv
- AlgebraicIndependent.aeval_comp_repr
- AlgebraicIndependent.aeval_repr
- AlgebraicIndependent.algebraMap_aevalEquiv
- AlgebraicIndependent.repr
- AlgebraicIndependent.repr_ker
- algebra_isAlgebraic_ringHom_iff_of_comp_eq
- algebraicIndependent_X

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

…EquivOfAlgEquiv`

alreadydone

LGTM modulo #18984. The import increase is mainly due to AlgebraicIndependent importing FieldRange importing FieldTheory.Adjoin, but I think we're gonna import FieldTheory.Adjoin into AlgebraicIndependent sooner or later. Notice that AlgebraicIndependent is currently almost a leaf file, being transitively imported by only 2 other files.

Mathlib/RingTheory/Algebraic.lean

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

acmepjz · 2024-11-13T18:12:46Z

I think we're gonna import FieldTheory.Adjoin into AlgebraicIndependent sooner or later.

I think so, as most part of algebraic independent theory is about fields.

Maybe later we need to split AlgebraicIndependent into several files: subalgebra part, field part, and transcendence basis & transcendence degree part.

Notice that AlgebraicIndependent is currently almost a leaf file, being transitively imported by only 2 other files.

Yeah, but once transcendence degree is defined, it should be used extensively in algebraic geometry. We also need separable transcendence basis & separably generated, etc. etc.

mathlib4-dependent-issues-bot · 2024-11-14T18:37:27Z

This PR/issue depends on:

~~[Merged by Bors] - feat(RingTheory/Localization/*): add IsLocalization.algEquivOfAlgEquiv and other results #18661~~
~~[Merged by Bors] - feat: add some result on IsFractionRing and fieldRange #18984~~
By Dependent Issues (🤖). Happy coding!

alreadydone

Thanks 🎉
maintainer merge

github-actions · 2024-11-15T09:06:20Z

🚀 Pull request has been placed on the maintainer queue by alreadydone.

riccardobrasca · 2024-11-15T09:12:33Z

Thanks!

bors merge

…lEquivField` and other results (#18648) This PR mainly adds - `AlgebraicIndependent.aevalEquivField`: canonical isomorphism between rational function field and the intermediate field generated by algebraically independent elements. - `AlgebraicIndependent.reprField`: canonical map from the intermediate field generated by an algebraic independent family into the rational function field. Other results: - `AlgebraicIndependent.aeval_of_algebraicIndependent`: if `x = {x_i : A | i : ι}` and `f = {f_i : MvPolynomial ι R | i : ι}` are algebraically independent over `R`, then `{f_i(x) | i : ι}` is also algebraically independent over `R`. - `AlgebraicIndependent.of_aeval`: conversely, if `{f_i(x) | i : ι}` is algebraically independent over `R`, then `{f_i : MvPolynomial ι R | i : ι}` is also algebraically independent over `R`. - `AlgebraicIndependent.polynomial_aeval_of_transcendental`: if `{x_i : A | i : ι}` is algebraically independent over `R`, and for each `i`, `f_i : R[X]` is transcendental over `R`, then `{f_i(x_i) | i : ι}` is also algebraically independent over `R`. - `AlgebraicIndependent.isEmpty_of_isAlgebraic`: if `A/R` is algebraic, then all algebraically independent families are empty. - `IsTranscendenceBasis.isEmpty_iff_isAlgebraic`: if `x` is a transcendence basis of `A/R`, then it is empty if and only if `A/R` is algebraic. - `IsTranscendenceBasis.nonempty_iff_transcendental`: if `x` is a transcendence basis of `A/R`, then it is not empty if and only if `A/R` is transcendental. - `IsTranscendenceBasis.isAlgebraic_field`: if `x` is a transcendence basis of `E / F`, then the field extension `E / F(x)` is algebraic. Also add `[of_]ringHom_of_comp_eq` for `[Algebra.]Transcendental` and `AlgebraicIndependent`. Also add some results for `Subalgebra` inspired by `IntermediateField.isAlgebraic_iff`. Some of them are not back-ported to `IntermediateField` yet; may be for another PR if they are useful.

mathlib-bors · 2024-11-15T09:25:56Z

Pull request successfully merged into master.

Build succeeded:

…lEquivField` and other results (#18648) This PR mainly adds - `AlgebraicIndependent.aevalEquivField`: canonical isomorphism between rational function field and the intermediate field generated by algebraically independent elements. - `AlgebraicIndependent.reprField`: canonical map from the intermediate field generated by an algebraic independent family into the rational function field. Other results: - `AlgebraicIndependent.aeval_of_algebraicIndependent`: if `x = {x_i : A | i : ι}` and `f = {f_i : MvPolynomial ι R | i : ι}` are algebraically independent over `R`, then `{f_i(x) | i : ι}` is also algebraically independent over `R`. - `AlgebraicIndependent.of_aeval`: conversely, if `{f_i(x) | i : ι}` is algebraically independent over `R`, then `{f_i : MvPolynomial ι R | i : ι}` is also algebraically independent over `R`. - `AlgebraicIndependent.polynomial_aeval_of_transcendental`: if `{x_i : A | i : ι}` is algebraically independent over `R`, and for each `i`, `f_i : R[X]` is transcendental over `R`, then `{f_i(x_i) | i : ι}` is also algebraically independent over `R`. - `AlgebraicIndependent.isEmpty_of_isAlgebraic`: if `A/R` is algebraic, then all algebraically independent families are empty. - `IsTranscendenceBasis.isEmpty_iff_isAlgebraic`: if `x` is a transcendence basis of `A/R`, then it is empty if and only if `A/R` is algebraic. - `IsTranscendenceBasis.nonempty_iff_transcendental`: if `x` is a transcendence basis of `A/R`, then it is not empty if and only if `A/R` is transcendental. - `IsTranscendenceBasis.isAlgebraic_field`: if `x` is a transcendence basis of `E / F`, then the field extension `E / F(x)` is algebraic. Also add `[of_]ringHom_of_comp_eq` for `[Algebra.]Transcendental` and `AlgebraicIndependent`. Also add some results for `Subalgebra` inspired by `IntermediateField.isAlgebraic_iff`. Some of them are not back-ported to `IntermediateField` yet; may be for another PR if they are useful.

add more results on AlgebraicIndependent

d0fd4ab

acmepjz added WIP Work in progress t-algebra Algebra (groups, rings, fields, etc) labels Nov 5, 2024

acmepjz marked this pull request as ready for review November 5, 2024 07:30

acmepjz added 8 commits November 5, 2024 16:16

add some maps

d7f6c0b

add MulEquivClass.map_nonZeroDivisors

1ff5ffd

rename fieldEquivOfRingEquiv -> ringEquivOfRingEquiv and add `alg…

9e8af48

…EquivOfAlgEquiv`

fix

43cf19f

fix

e438dd1

?

9035726

add results

83fe078

fix and add another result

73d9c15

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 5, 2024

acmepjz added 6 commits November 6, 2024 22:16

merge from another branch

eefb5f0

add a new file

987d851

add liftAlgHom

ae0c396

copy

a10d3d3

fix typo

7adc9f1

add aevalEquivField and reprField

69c7ed2

acmepjz removed the WIP Work in progress label Nov 7, 2024

add docstring

1fd87c1

acmepjz changed the title ~~feat(RingTheory/AlgebraicIndependent): add more results on AlgebraicIndependent~~ feat(RingTheory/AlgebraicIndependent): add AlgebraicIndependent.aevalEquivField and other results Nov 8, 2024

acmepjz added 3 commits November 8, 2024 21:59

remove duplicated variables

1210858

add IsTranscendenceBasis.isAlgebraic_field

509e5a0

update docstring

5f27c32

This was referenced Nov 8, 2024

[Merged by Bors] - feat(FieldTheory/SeparableDegree): Field.Emb is infinite for transcendental extension #18770

Closed

[Merged by Bors] - feat: some results on dimension of field adjoin #18515

Closed

acmepjz added 2 commits November 10, 2024 01:13

Merge branch 'master' into acmepjz_alg_indep_4

c04f3b2

add Transcendental version of ringHom_of_comp_eq

8300844

Merge branch 'master' into acmepjz_alg_indep_4

1c32e2e

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 13, 2024

alreadydone mentioned this pull request Nov 13, 2024

[Merged by Bors] - feat: add some result on IsFractionRing and fieldRange #18984

Closed

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 13, 2024

alreadydone approved these changes Nov 13, 2024

View reviewed changes

Mathlib/RingTheory/Algebraic.lean Outdated Show resolved Hide resolved

Mathlib/RingTheory/Algebraic.lean Outdated Show resolved Hide resolved

Apply suggestions from code review

8edc955

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

acmepjz added 2 commits November 14, 2024 20:03

rename bot -> bot_(left|right)

311ce6f

Merge branch 'master' into acmepjz_alg_indep_4

e7f3a7e

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 14, 2024

acmepjz added 2 commits November 15, 2024 14:53

remove file as it is added an another PR

28d3914

Merge branch 'master' into acmepjz_alg_indep_4

d922482

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Nov 15, 2024

oops

66e2e7b

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Nov 15, 2024

get rid of erw

dc56cb3

acmepjz requested a review from alreadydone November 15, 2024 07:18

alreadydone reviewed Nov 15, 2024

View reviewed changes

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Nov 15, 2024

alreadydone approved these changes Nov 15, 2024

View reviewed changes

github-actions bot added the ready-to-merge This PR has been sent to bors. label Nov 15, 2024

mathlib-bors bot changed the title ~~feat(RingTheory/AlgebraicIndependent): add AlgebraicIndependent.aevalEquivField and other results~~ [Merged by Bors] - feat(RingTheory/AlgebraicIndependent): add AlgebraicIndependent.aevalEquivField and other results Nov 15, 2024

mathlib-bors bot closed this Nov 15, 2024

mathlib-bors bot deleted the acmepjz_alg_indep_4 branch November 15, 2024 09:26

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(RingTheory/AlgebraicIndependent): add `AlgebraicIndependent.aevalEquivField` and other results#18648

[Merged by Bors] - feat(RingTheory/AlgebraicIndependent): add `AlgebraicIndependent.aevalEquivField` and other results#18648
acmepjz wants to merge 37 commits intomasterfrom
acmepjz_alg_indep_4

acmepjz commented Nov 5, 2024 •

edited

Loading

Uh oh!

github-actions bot commented Nov 5, 2024 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

alreadydone left a comment

Uh oh!

Uh oh!

Uh oh!

acmepjz commented Nov 13, 2024

Uh oh!

mathlib4-dependent-issues-bot commented Nov 14, 2024

Uh oh!

alreadydone left a comment

Uh oh!

github-actions bot commented Nov 15, 2024

Uh oh!

riccardobrasca commented Nov 15, 2024

Uh oh!

mathlib-bors bot commented Nov 15, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Conversation

acmepjz commented Nov 5, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Nov 5, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary dc56cb32a9

Import changes for modified files

Declarations diff

Uh oh!

alreadydone left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

acmepjz commented Nov 13, 2024

Uh oh!

mathlib4-dependent-issues-bot commented Nov 14, 2024

Uh oh!

alreadydone left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Nov 15, 2024

Uh oh!

riccardobrasca commented Nov 15, 2024

Uh oh!

mathlib-bors bot commented Nov 15, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

acmepjz commented Nov 5, 2024 •

edited

Loading

github-actions bot commented Nov 5, 2024 •

edited

Loading