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/TranscendenceBasis.lean, we show:

• The AlgebraicIndependent sets in a domain form a Matroid, which is used to show all transcendence bases have the same cardinality. Provide algebraic characterizations of the matroid notions Indep, Base, cRank, Basis, closure, Flat, and Spanning.

• Transcendence bases are exactly algebraic independent families that are spanning (i.e. the whole algebra is algebraic over the algebra generated by the family). On the other hand, a spanning set in a domain contains a transcendence basis.

• There always exists an transcendence basis between an arbitrary AlgebraicIndependent set and an "almost generating" set in a domain.

• trdeg R S + trdeg S A = trdeg R A in a domain, which depends on AlgebraicIndependent/IsTranscendenceBasis.sumElim_comp.

• A finite AlgebraicIndependent family or spanning family in a domain that has the same cardinality as trdeg must be a transcendence basis.

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 9ff1e5d7b4

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis	1411	1420	+9 (+0.64%)

Import changes for all files

Files

Import difference

20 files Mathlib.FieldTheory.AxGrothendieck Mathlib.FieldTheory.CardinalEmb Mathlib.FieldTheory.Galois.GaloisClosure Mathlib.FieldTheory.Galois.Infinite Mathlib.FieldTheory.Galois.Profinite Mathlib.FieldTheory.IsAlgClosed.Classification Mathlib.FieldTheory.IsPerfectClosure Mathlib.FieldTheory.JacobsonNoether Mathlib.FieldTheory.LinearDisjoint Mathlib.FieldTheory.PurelyInseparable.Basic Mathlib.FieldTheory.PurelyInseparable.PerfectClosure Mathlib.FieldTheory.PurelyInseparable.Tower Mathlib.FieldTheory.SeparableClosure Mathlib.FieldTheory.SeparableDegree Mathlib.ModelTheory.Algebra.Field.IsAlgClosed Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis Mathlib.RingTheory.Etale.Field Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Unramified.LocalRing

9

---

Declarations diff

+ AlgEquiv.isTranscendenceBasis
+ AlgEquiv.isTranscendenceBasis_iff
+ AlgEquiv.lift_trdeg_eq
+ AlgEquiv.trdeg_eq
+ Algebra.trdeg
+ AlgebraicIndependent.cardinalMk_le_trdeg
+ AlgebraicIndependent.insert
+ AlgebraicIndependent.insert_iff
+ AlgebraicIndependent.isTranscendenceBasis_iff_isAlgebraic
+ AlgebraicIndependent.lift_cardinalMk_le_trdeg
+ AlgebraicIndependent.of_subsingleton
+ AlgebraicIndependent.option_iff_transcendental
+ Function.Injective.nonempty_algebraicIndependent
+ IsAlgebraic.adjoin_of_forall_isAlgebraic
+ IsTranscendenceBasis.mvPolynomial
+ IsTranscendenceBasis.mvPolynomial'
+ IsTranscendenceBasis.of_subsingleton
+ IsTranscendenceBasis.of_subtype_range
+ IsTranscendenceBasis.polynomial
+ IsTranscendenceBasis.sumElim_comp
+ IsTranscendenceBasis.to_subtype_range
+ IsTranscendenceBasis.to_subtype_range'
+ MvPolynomial.algebraicIndependent_polynomial_aeval_X
+ MvPolynomial.trdeg_of_isDomain
+ Polynomial.trdeg_of_isDomain
+ Set.AlgebraicIndependent
+ Subalgebra.mem_algebraicClosure
+ _
+ algebraicIndependent_of_set_of_finite
+ cardinalMk_eq
+ cardinalMk_eq_trdeg
+ exists_isTranscendenceBasis_between
+ exists_isTranscendenceBasis_subset
+ exists_isTranscendenceBasis_superset
+ iff_adjoin_image
+ iff_adjoin_image_compl
+ iff_transcendental_adjoin_image
+ instance : (matroid inj).Finitary
+ isAlgebraic_adjoin_iff_of_matroid_basis
+ isAlgebraic_iff_exists_isTranscendenceBasis_subset
+ isDomain_of_adjoin_range
+ isEmpty_algebraicIndependent
+ isTranscendenceBasis_equiv
+ isTranscendenceBasis_equiv'
+ isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic
+ isTranscendenceBasis_iff_maximal
+ isTranscendenceBasis_iff_of_subsingleton
+ isTranscendenceBasis_image
+ isTranscendenceBasis_of_le_trdeg
+ isTranscendenceBasis_of_le_trdeg_of_finite
+ isTranscendenceBasis_of_lift_le_trdeg
+ isTranscendenceBasis_of_lift_le_trdeg_of_finite
+ isTranscendenceBasis_of_lift_trdeg_le
+ isTranscendenceBasis_of_lift_trdeg_le_of_finite
+ isTranscendenceBasis_of_trdeg_le
+ isTranscendenceBasis_of_trdeg_le_of_finite
+ isTranscendenceBasis_subtype_range
+ lift_cardinalMk_eq
+ lift_cardinalMk_eq_trdeg
+ lift_trdeg_add_eq
+ lift_trdeg_add_eq_of_field
+ lift_trdeg_add_le
+ lift_trdeg_le_of_injective
+ lift_trdeg_le_of_surjective
+ matroid
+ matroid_base_iff
+ matroid_basis_iff
+ matroid_basis_iff_of_subsingleton
+ matroid_cRank_eq
+ matroid_closure_eq
+ matroid_closure_of_subsingleton
+ matroid_e
+ matroid_flat_iff
+ matroid_flat_of_subsingleton
+ matroid_indep_iff
+ matroid_spanning_iff
+ matroid_spanning_iff_of_subsingleton
+ sumElim
+ sumElim_comp
+ sumElim_iff
+ sumElim_of_tower
+ trdeg_add_eq
+ trdeg_add_eq_of_finite
+ trdeg_add_le
+ trdeg_eq_iSup_cardinalMk_isTranscendenceBasis
+ trdeg_eq_zero
+ trdeg_eq_zero_iff
+ trdeg_eq_zero_of_not_injective
+ trdeg_le_cardinalMk
+ trdeg_le_of_injective
+ trdeg_le_of_surjective
+ trdeg_lt_aleph0
+ trdeg_ne_zero_iff
+ trdeg_subsingleton
+ zero_lt_trdeg
- 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).

[apnelson1]

I think that (unless I'm misunderstanding something mathematical) defining a matroid with an injectivity assumption might cause problems later. Presumably if I have some 'repeated elements' in an algebra, I can still make a matroid - these elements will just be parallel pairs in the matroid.

On the other hand possibly your definition makes sense as a 'matroid on an algebra', and then an 'algebraic matroid' on some indexing type is something that arises from a map from the type to an algebra.

Even though the Simple and Loopless typeclasses are only in my repo and not mathlib, they are on their way, and I think the ad hoc lemmas about looplessness and simplicity of algebraic matroids you have included won't be needed in the forms you're stating them, rather just as special cases of lemmas with instance arguments. Do you explicitly need them to make things work, or are they just intended as API?

[alreadydone]

Even though the Simple and Loopless typeclasses are only in my repo and not mathlib, they are on their way, and I think the ad hoc lemmas about looplessness and simplicity of algebraic matroids you have included won't be needed in the forms you're stating them, rather just as special cases of lemmas with instance arguments. Do you explicitly need them to make things work, or are they just intended as API?

I'm not really using the of_subsingleton lemmas, they're included just for completeness. In fact I don't need the two Flat lemmas either, because I can go directly from closure to Spanning. Once you add Simple and Loopless to mathlib I'd be happy to include these instances and golf these lemmas, maybe in a future PR. However notice that we're talking about the matroid on a singleton type where Set.univ is independent, which is the freeOn matroid. Is there a typeclass for that?

[apnelson1]

Even though the Simple and Loopless typeclasses are only in my repo and not mathlib, they are on their way, and I think the ad hoc lemmas about looplessness and simplicity of algebraic matroids you have included won't be needed in the forms you're stating them, rather just as special cases of lemmas with instance arguments. Do you explicitly need them to make things work, or are they just intended as API?

I'm not really using the of_subsingleton lemmas, they're included just for completeness. In fact I don't need the two Flat lemmas either, because I can go directly from closure to Spanning. Once you add Simple and Loopless to mathlib I'd be happy to include these instances and golf these lemmas, maybe in a future PR. However notice that we're talking about the matroid on a singleton type where Set.univ is independent, which is the freeOn matroid. Is there a typeclass for that?

No, but perhaps there should be. It would be RankZero M✶, where RankZero is the negation of what is currently calledRkPos.

[apnelson1]

Even though the Simple and Loopless typeclasses are only in my repo and not mathlib, they are on their way, and I think the ad hoc lemmas about looplessness and simplicity of algebraic matroids you have included won't be needed in the forms you're stating them, rather just as special cases of lemmas with instance arguments. Do you explicitly need them to make things work, or are they just intended as API?

I'm not really using the of_subsingleton lemmas, they're included just for completeness. In fact I don't need the two Flat lemmas either, because I can go directly from closure to Spanning. Once you add Simple and Loopless to mathlib I'd be happy to include these instances and golf these lemmas, maybe in a future PR. However notice that we're talking about the matroid on a singleton type where Set.univ is independent, which is the freeOn matroid. Is there a typeclass for that?

No, but perhaps there should be. It would be RankZero M✶, where RankZero is the negation of what is currently calledRkPos.

And I hadn't noticed the Subsingleton part - those lemmas make sense now, and aren't to do with simplicity/looplessness as I'd thought. Sorry for the noise!

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

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

[apnelson1]

It seems like the design concerns here are analogous to linear independence, and it looks like LinearIndependentOn might become the solution, rather than having a predicate for sets of vectors. see #21799 and this zulip discussion

A specific problem with this definition is that it doesn't let one talk about algebraic independence of sets of indices for a non-injective function from a type to an algebra, and this will in turn make 'algebraic representations' of non-simple matroids hard to define.

Could you consider defining AlgebraicIndependentOn R (f : ι → A) (s : Set ι) here, and using AlgebraicIndependentOn R id s to spell this predicate?

[alreadydone]

My purpose of introducing this abbrev is simply to shorten a common expression that appears many times across the AlgebraicIndependent files, and it's desirable to use dot notation to make it shorter.

In order to define 'algebraic representations' of non-simple matroids, wouldn't you just say it's a function such that your matroid is Matroid.comap of some algebraic matroid via this function?
(By the way I find it interesting that people only consider such "faithful" representation of matroids, which is not the case for group and algebra representations. Maybe there isn't a good notion of general representations for matroids.)

[apnelson1]

By a representation of M, I mean a function f from M.E to some algebra A such that matroid independence corresponds to algebraic independence of the image, but in the sense where two elements with the same image count as a dependency. This is indeed the same as M being a comap of the natural algebraic matroid whose ground set is A.

I don't quite understand what you mean by 'faithful'ness here - is there a more general notion of matroid representation that you're alluding to?

I'm of course speaking from the implicit perspective that the (abstract) matroid is the object you're being given, and the question is whether it has an algebraic representation. From where you're standing, I can understand if this seems weird. But for example, it is still an open question whether the matroid dual of an algebraic matroid is always algebraic, and that question is awkward to even state without the notion of an algebraic representation of an abstract matroid. (Note that duality does not respect simplicity).

But more concretely, I think that AlgebraicIndependentOn would be a useful definition that has your abbrev Set.AlgebraicIndependent as a special case, and that refactoring this PR slightly to include it would save future work.