[Merged by Bors] - feat(Algebra): Transcendence degree

[alreadydone]

Define transcendence degree Algebra.trdeg and proves some basic properties:

In AlgebraicIndependent/Basic.lean: define Algebra.trdeg to be the supremum of the cardinalities of all AlgebraicIndependent sets, just like Module.rank is defined to be the supremum of the cardinalities of all LinearIndependent sets. Add some API lemmas and trivial results about trdeg, e.g. that injective/surjective AlgHoms induce inequalities between trdegs, and AlgEquivs induce equalities.

In AlgebraicIndependent/Transcendental.lean: add API lemmas and show the inequality trdeg R S + trdeg S A ≤ trdeg R A (which does not require a domain).

In AlgebraicIndependent/Defs.lean: add Stacks tags and some trivial API lemmas about IsTranscendenceBasis.

Thanks to Chris Hughes and Jz Pan for preliminary works and Peter Nelson for the hint about Finitary and IndepMatroid.

TODO:

• The analogue of StrongRankCondition in the setting of algebras, which implies trdeg R (MvPolynomial (Fin n) R) = n for all Nontrivial CommRing R.

---

• depends on: [Merged by Bors] - feat(Matroid): all bases of a finitary matroid have the same cardinality #20888
• depends on: [Merged by Bors] - feat(Matroid): cardinality criteria for indep/spanning sets to be bases #21512
• depends on: [Merged by Bors] - chore(RingTheory/Algebraic): remove unnecessary injectivity assumptions #21566

[github-actions]

PR summary 2661729d66

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ AlgEquiv.isTranscendenceBasis
+ AlgEquiv.isTranscendenceBasis_iff
+ AlgEquiv.lift_trdeg_eq
+ AlgEquiv.trdeg_eq
+ Algebra.trdeg
+ AlgebraicIndepOn
+ AlgebraicIndepOn.insert
+ AlgebraicIndepOn.insert_iff
+ AlgebraicIndependent.cardinalMk_le_trdeg
+ AlgebraicIndependent.lift_cardinalMk_le_trdeg
+ AlgebraicIndependent.of_subsingleton
+ AlgebraicIndependent.option_iff_transcendental
+ IsAlgebraic.adjoin_of_forall_isAlgebraic
+ IsTranscendenceBasis.of_subsingleton
+ IsTranscendenceBasis.of_subtype_range
+ IsTranscendenceBasis.to_subtype_range
+ IsTranscendenceBasis.to_subtype_range'
+ MvPolynomial.algebraicIndependent_polynomial_aeval_X
+ Subalgebra.mem_algebraicClosure
+ _
+ algebraicIndependent_of_set_of_finite
+ iff_adjoin_image
+ iff_adjoin_image_compl
+ iff_transcendental_adjoin_image
+ instance [FaithfulSMul R A] : Nonempty { s : Set A // AlgebraicIndepOn R id s }
+ isEmpty_algebraicIndependent
+ isTranscendenceBasis_equiv
+ isTranscendenceBasis_equiv'
+ isTranscendenceBasis_iff_maximal
+ isTranscendenceBasis_iff_of_subsingleton
+ isTranscendenceBasis_image
+ isTranscendenceBasis_subtype_range
+ lift_trdeg_add_le
+ lift_trdeg_le_of_injective
+ lift_trdeg_le_of_surjective
+ sumElim
+ sumElim_comp
+ sumElim_iff
+ sumElim_of_tower
+ trdeg_add_le
+ trdeg_eq_zero
+ trdeg_eq_zero_iff
+ trdeg_eq_zero_of_not_injective
+ trdeg_le_of_injective
+ trdeg_le_of_surjective
+ trdeg_ne_zero_iff
+ trdeg_pos
+ trdeg_subsingleton
- algebraicIndependent_polynomial_aeval_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

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[acmepjz]

Thank you very much!

[acmepjz]

TODO:

• Inequalities between trdegs induced by injective/surjective AlgHom, and equality induced by AlgEquiv.

I think injective AlgHom version should be a consequence of your lift_trdeg_add_le (if not Injective (algebraMap R S) then it's 0 = 0), and AlgEquiv version is a corollary of it (by the inequality of injectivity of the map and its inverse, or maybe we should add AlgEquiv preserves AlgebraicIndependent (which I think we already have it, EDIT: AlgHom.algebraicIndependent_iff and algebraicIndependent_ringHom_iff_of_comp_eq) and IsTranscendenceBasis). I'm not sure of surjective AlgHom version, though.

EDIT2: Maybe the AlgebraicIndependent.ringHom_of_comp_eq should imply a slight generalization of your injective AlgHom inequality, and the AlgebraicIndependent.of_ringHom_of_comp_eq + g surjective should imply a slight generalization of your surjective AlgHom inequality.

EDIT3: Maybe there is an unconditional trdeg S A ≤ trdeg R A given IsScalarTower R S A (unchecked yet).

[erdOne]

What is the status of this PR? I would very much like to have these results in mathlib.
Is this ready for review yet or are you planning to split this up further?
I think a nice split might be to move everything changed in Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean into a new PR.

[alreadydone]

Is this ready for review yet or are you planning to split this up further?

Yeah it's ready for review and I had no plan to split it up further.

I think a nice split might be to move everything changed in Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean into a new PR.

Okay, changes in that file are now split to #23539.

[erdOne]

I wonder why the docPrime linter does not complain here.

[alreadydone]

It's an existing theorem, just moved up, and it's in nolints_prime_decls.txt.

[erdOne]

Thanks!
maintainer merge

[github-actions]

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

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style