Transcendence degree?

Stream: Is there code for X?

[Jz Pan]

• Anyone is currently working on transcendence degree and related topics?

• Which of the following two definitions is better for transcendence degree?

  • The cardinality of docs#exists_isTranscendenceBasis
  • The supremum of cardinality of algebraic independent subsets

  The docs#Module.rank is defined using the second approach. And this method works without requiring the existence of transcendence basis.

[Jz Pan]

• If using the second approach, what is the best way to show the cardinality of a transcendence basis is equal to transcendence degree? Is it a good idea to introduce matroid? Or just use the usual proof found in textbook?

[Jz Pan]

• Do we have Lüroth's theorem?

[Junyan Xu]

If using the second approach, what is the best way to show the cardinality of a transcendence basis is equal to transcendence degree? Is it a good idea to introduce matroid? Or just use the usual proof found in textbook?

I think with both definition you'd want to show the cardinality of every transcendence basis (= maximal algebraically independent subsets) are the same. Using the latter definition is ostensibly more general as it doesn't require injectivity of the algebraMap, but if it's not injective then there is no algebraically independent subset so this case is not interesting.

There is docs#Matroid in Mathlib but I'm not sure how easy to construct examples and apply it to concrete situations.

Given the proof methods of Lüroth's theorem (genus of curves, or transcendence degree) I'd bet it's not yet formalized in Lean (unless someone has done tr.deg. somewhere).

[Jz Pan]

I'm reading P. M. Cohn's Basic Algebra, seems that it uses matroid:

2024-11-09 225515.png

[Jz Pan]

In https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matroid/Basic.html

For infinite matroids, bases are not in general equicardinal; in fact the equicardinality of bases of infinite matroids is independent of ZFC [3].

:exploding_head:

[Jz Pan]

But in that book we have Theorem 11.1.5 which says that any bases has the same cardinality. I guess that is the matroid in mathlib together with a stronger hypothesis? Any experts?

[Junyan Xu]

I guess you deduce the infinite case from the finite case, and this part of the argument is specific to algebraically independent sets. I think you can refer to nLab or Stacks Project.

[Junyan Xu]

Looking at Stacks, apparently you'd use a different proof for the infinite case.

[Johan Commelin]

I think it would be really cool to have applications of the matroid library in mathlib.

[Johan Commelin]

Also cc @Peter Nelson

[Jz Pan]

In https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matroid/Basic.html

For infinite matroids, bases are not in general equicardinal; in fact the equicardinality of bases of infinite matroids is independent of ZFC [3].

:exploding_head:

In Cohn's book:

2024-11-11 171358.png

There is Theorem 11.1.5 which says that any two bases have the same cardinality. While for the weaker assumption D.1', only finite bases have the same cardinality, which is consistent with the docstring in mathlib. So I suspect that D.1' coincides with the matroid in mathlib, while D.1 is a stronger assumption on it.

[Antoine Chambert-Loir]

Indeed, most presentations of the transcendence degree involve a version of the exchange lemma, but that does not mean that one has to pass through matroids, and indeed, one doesn't. (See my “(Mostly) commutative algebra”, corollary 4.8.7.)

Note that the exchange lemma is needed for possibly infinite transcendent bases, while the classic definition of matroids is not so good in the infinite case, and I don't know what version mathlib has chosen. Still, matroids are cool, and if that works through matroids, then why not, and it would be reasonable to reformulate the existence of dimension in this framework as well.

[Chris Hughes]

I have started work on proving that all transcendence bases have the same cardinality. The work is here I have some version of the exchange lemma with one sorry.

[Chris Hughes]

This was a little more complicated than I anticipated so I might not have time to work on this in the near future. I think we're missing some key lemmas about totalDegree, like totalDegree (X i * p) = ....

Contributions are welcome

[Jz Pan]

Chris Hughes said:

I have started work on proving that all transcendence bases have the same cardinality. The work is here I have some version of the exchange lemma with one sorry.

Great work! Unfortunately I can't take a look in these weeks (in fact I still have some pending TODOs on mathlib not started yet, due to the same reason).

[Chris Hughes]

I think if I were to really do this in the nicest way possible I would probably make the following changes in mathlib. I don't think I will have the time to do this, but I'll pass this on anyway.

• Restate Algebra.isAlgebraic to take a ring hom instead of an algebra instance. I often want to reason about one subalgebra being algebraic over another which means locally introducing instances. In general, I think the Algebra typeclass might be a bit overused and we should just be using ring homs instead. The whole point of this type-class was probably motivated by the fact that RingHoms induce module structures, but in my experience I think it would be easier to locally introduce a module instance when needed than to locally introduce Algebrainstances all the time (other people's experience may differ).
• Redefine the internal algebraic closure, algebraicClosure to take a set as an argument, and it would be defined as the elements algebraic over the subring generated by the set. This would have all the nice galois-insertion properties as well as a useful "compactness" property x ∈ algebraicClosure S ↔ ∃ (t : Set R), Set.Finite t ∧ t ⊆ S ∧ x ∈ algebraicClosure t. This could be done for integralClosure as well.

[Johan Commelin]

@Chris Hughes Can the new algebraize tactic help with the first point? It's meant to help with moving ring homs and properties of ring homs to (locally in the proof) algebras and properties of algebras

[Chris Hughes]

It would help in some cases, but obviously you can't easily state theorems without a global instance. For example, the key theorem about the algebraicClosure definition I mentioned above would be Algebra.isAlgebraic (Subring.closure s) (algebraicClosure s) and maybe some other things about which subrings are or are not algebraic over others. Of course you could state these with an Algebra hypothesis and also a hypothesis saying algebraMap _ _ = ....

When talking about transcendence bases it would be nice to know IsTranscendenceBasis R x -> Algebraic (MvPolynomial _ R) A, with the algebra instance given by evaluating the polynomial at x. It's almost always much nicer to work with an MvPolynomial instead of Algebra.adjoin R (range x) and they're isomorphic. But I'm finding myself forced to use Algebra.adjoin R (range x) just for the algebra instance. Of course I could maybe use the same method as before with a hypothesis saying algebraMap _ _ = MvPolynomial.aeval _, but this feels wrong.

[Johan Commelin]

Maybe I should clarify that I was in favour of your point that we should also have RingHom.isAlgebraic. But my point is that we should also keep Algebra.isAlgebraic. And then use algebraize to move back and forth as needed.

[Chris Hughes]

Yes, I'm happy with that

[Jz Pan]

Maybe for now we should define a RingHom.IsAlgebraic as a workaround. In this way the existing APIs are not needed to be changed.

[Jz Pan]

Just like my ongoing work of RingHom.relrank which should fix the slowness of Subfield.relrank

[Junyan Xu]

It seems this AddCommMonoid instance is the slowest (maybe it's AddCommGroup before #20774); maybe we should add this shortcut instance to remind Lean locally.

[Junyan Xu]

I hope the following approach could lead to a simpler proof; unfortunately it's too late now and I have to continue tomorrow. Feel free to fill in the sorry :)

import Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure

variable {ι R A : Type*} [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A']

open Algebra Set Function

theorem algebraicIndependent_of_set_of_finite {x : ι → A}
    (s : Set ι) (ind : AlgebraicIndependent R fun i : s ↦ x i)
    (H : ∀ t : Set ι, t.Finite → AlgebraicIndependent R (fun i : t ↦ x i) →
      ∀ i ∉ s, i ∉ t → Transcendental (adjoin R (x '' t)) (x i)) :
    AlgebraicIndependent R x := by
  classical
  refine algebraicIndependent_of_finite_type fun t hfin ↦ ?_
  suffices AlgebraicIndependent R fun i : ↥(t ∩ s ∪ t \ s) ↦ x i from
    this.comp (Equiv.Set.ofEq (t.inter_union_diff s).symm) (Equiv.injective _)
  refine hfin.diff.induction_on_subset _ (ind.comp (inclusion <| by simp) (inclusion_injective _))
    fun {a u} ha hu ha' h ↦ ?_
  have : a ∉ t ∩ s ∪ u := (·.elim (ha.2 ·.2) ha')
  convert (((image_eq_range _ _ ▸ h.option_iff <| x a).2 <| H _ (hfin.subset (union_subset
    inter_subset_left <| hu.trans diff_subset)) h a ha.2 this).comp _ (subtypeInsertEquivOption
    this).injective).comp (Equiv.Set.ofEq union_insert) (Equiv.injective _) with x
  by_cases h : ↑x = a <;> simp [h, Set.subtypeInsertEquivOption]

/- if we assume that hx is a transcendence basis, then we should be able to
replace NoZeroDivisor A by NoZeroDivisor R, because a polynomial ring over
a ring with no zero divisor has no zero divisor. -/
open Set in
theorem exchange_lemma [DecidableEq ι] (x : ι → A) (y : A) [NoZeroDivisors A]
    (hx : Algebra.IsAlgebraic (adjoin R (range x)) A) (hy : Transcendental R y) :
    ∃ i : ι, Algebra.IsAlgebraic (adjoin R (range (update x i y))) A := by
  let xy (o : Option ι) := o.elim y x
  have : ¬ AlgebraicIndependent R xy := fun h ↦ by
    have := h.transcendental_adjoin (s := range some) (i := none) (by simp)
    rw [← range_comp] at this
    exact this (hx.1 y)
  have := mt (algebraicIndependent_of_set_of_finite {none} <|
    (algebraicIndependent_singleton_iff ⟨_, rfl⟩).mpr hy) this
  simp_rw [Transcendental] at this; push_neg at this
  obtain ⟨t, fin, ind, _|i, hi, hit, alg⟩ := this
  · exact (hi rfl).elim
  let Rxyi := adjoin R (range (update x i y))
  let Rxy := adjoin R (range x ∪ {y})
  let _ : Algebra Rxyi Rxy := by
    refine (Subalgebra.inclusion <| adjoin_mono <| range_subset_iff.mpr fun j ↦ ?_).toAlgebra
    obtain rfl | ne := eq_or_ne j i
    · rw [update_self]; exact .inr rfl
    · rw [update_of_ne ne]; exact .inl ⟨_, rfl⟩
  have : IsScalarTower Rxyi Rxy A := .of_algebraMap_eq fun ⟨a, _⟩ ↦ show a = _ from rfl
  set Rx := adjoin R (range x)
  let _ : Algebra Rx Rxy := (Subalgebra.inclusion <| adjoin_mono subset_union_left).toAlgebra
  have : IsScalarTower Rx Rxy A := .of_algebraMap_eq fun ⟨a, _⟩ ↦ show a = _ from rfl
  have : Algebra.IsAlgebraic Rxy A :=
    .extendScalars (R := adjoin R (range x)) (Subalgebra.inclusion_injective _)
  have : Algebra.IsAlgebraic Rxyi Rxy := by
    sorry
  exact ⟨i, Algebra.IsAlgebraic.trans' _ (S := Rxy) Subtype.val_injective⟩

[Junyan Xu]

I just pushed sorry-free exchange lemma. The proof is restructured a bit from the code above.

[Chris Hughes]

I've done some work in the CHTranscendence degree branch on using the exchange lemma to prove what I call the big_exchange_lemma

theorem big_exchange_lemma
    [IsDomain A] (x : ι → A) (y : ι' → A)
    (hx : Algebra.IsAlgebraic (adjoin R (range x)) A) (hy : AlgebraicIndependent R y) :
    ∃ f : ι' ↪ ι, Algebra.IsAlgebraic (adjoin R (range y ∪ (x '' (range f)ᶜ))) A

This is a non-textbook approach and I'm trying to use zorn's lemma to generalize the proof for the finite case to the infinite case instead of using the seperate proof. I have an inkling one of the sorrys is false (the one currently on line 301 of Mathlib/RingTheory/AlgebraicIndependent. The code is there if you want to use it, but of course it may be easier to do it your own way.

[Junyan Xu]

if we assume that hx is a transcendence basis, then we should be able to replace NoZeroDivisor A by NoZeroDivisor R, because a polynomial ring over a ring with no zero divisor has no zero divisor.

I just realized that this comment in my code above is wrong, because an algebra over a domain may have transcendence bases of different cardinality if the algebra is not a domain: just take the example in the second paragraph in this answer ($A$ is arbitrary and could be taken to be a domain). I started having this strange misconception since ~3 weeks ago.

[Junyan Xu]

Pushed some helper lemmas for the IsTranscendenceBasis version of the exchange lemma, and calling it a day. I expect that the finite version of the big exchange lemma is easiest to prove using induction and another similar helper lemma that requires an inline R[X]-algebra instance (from the y : A) to state.

[Junyan Xu]

This is a non-textbook approach and I'm trying to use zorn's lemma to generalize the proof for the finite case to the infinite case instead of using the seperate proof.

It seems that there's an obstruction to make this work. Consider $\{x_1,x_2,x_3,\dots\}$ and $\{x_1,x_1-x_2,x_2-x_3,x_3-x_4,\dots\}$, which are both transcendence bases of $R[x_1,x_2,x_3,\dots]$. You can replace the 1st element in the first basis by the 2nd element in the second basis, the 2nd by the 3rd, the 3rd by the 4th, and so forth, and still get a transcendence basis as long as you only do this finitely many times. But if you do all replacements at once, the result becomes a proper subset of a transcendence basis. I believe the big exchange lemma is still true, but you'll need a different approach than Zorn's lemma.

[Chris Hughes]

I guess that's why they didn't do it that way on the stacks project.

[Peter Nelson]

Jz Pan said:

I'm reading P. M. Cohn's Basic Algebra, seems that it uses matroid:

2024-11-09 225515.png

Sorry I’m a little late to the party here. The definition given looks like it’s basically that of Finitary matroids, which are a subclass (defined in mathlib) that avoid many pathologies found in general infinite matroids. A finitary matroid is just one where X is independent iff its finite subsets are all independent.

They aren’t the right generality for the matroid API, because the dual of a finitary matroid isn’t finitary. But finitary matroids do have equicardinal bases - this isn’t in mathlib or my repo yet but wouldn’t take me long to do if needed. So this would perhaps be a legitimate way to handle transcendence bases.

[Junyan Xu]

Importing Mathlib.Data.Matroid.Basic into Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis only adds to transitive imports (1239 -> 1241). Looks like a good deal! I'll try to establish connections between Base / Indep and IsTranscendenceBasis / AlgebraicIndependent.

[Peter Nelson]

Is a transcendence basis the same thing as a maximal algebraically independent set?

[Peter Nelson]

(Within a given family)

[Junyan Xu]

Yes, it is. An algebraic independent family is always injective (except over the trivial ring), so it's equivalent to consider its range.

[Peter Nelson]

If so, one just needs to define an algebraic matroid (using IndepMatroid.ofFinitary) and that would open up a lot of matroid machinery to be applied out of the box to this stuff

[Peter Nelson]

(deleted)

[Junyan Xu]

image.png
The definition switches to the range in the second part.

[Junyan Xu]

I think it's pretty easy to construct an IndepMatroid directly. The finitary property is just algebraicIndependent_of_finite.

[Peter Nelson]

That is good news! My repo (https://github.com/apnelson1/Matroid) has a lot of things that aren’t yet in mathlib, and might have some use to avoid reinventing the wheel.

[Junyan Xu]

It looks like the author of docs#exists_maximal_algebraicIndependent must have had matroids in mind because it's exactly what we need for indep_maximal :)

[Junyan Xu]

This was by @Chris Hughes 4 years ago in mathlib3#9229.

[Chris Hughes]

I didn't have matroids in mind but I'm glad it works nicely

[Junyan Xu]

indep_maximal X _ I ind hIX := exists_maximal_algebraicIndependent I X hIX ind

no need to even unwrap Maximal

[Junyan Xu]

I've constructed the finitary matroid and it's only +76 -13. Looks like matroids are offering a vast simplification here!

[Chris Hughes]

So is the fact that any two transcendence bases have the same cardinality just an application of a generic matroid theorem now?

[Peter Nelson]

Yes, albeit one that isn’t yet formalized

[Peter Nelson]

I can hopefully do it in the next couple of days, though

[Junyan Xu]

I'd expect the "big exchange lemma" is also theorem of matroids, but I'm not sure how useful it is ...

[Peter Nelson]

What is that lemma?

[Chris Hughes]

Chris Hughes said:

theorem big_exchange_lemma
    [IsDomain A] (x : ι → A) (y : ι' → A)
    (hx : Algebra.IsAlgebraic (adjoin R (range x)) A) (hy : AlgebraicIndependent R y) :
    ∃ f : ι' ↪ ι, Algebra.IsAlgebraic (adjoin R (range y ∪ (x '' (range f)ᶜ))) A

Here it is, but not in the language of matroids. It's the approach I was going to use to prove the cardinality theorem, but it turned out to be more difficult than I thought

[Peter Nelson]

I’m sorry if it’s implicit in the above discussion; I’m on mobile

[Junyan Xu]

I think it says: if B is a base and I is independent, then there exists an injection f : I → B such that I ∪ f(I)ᶜ is a base. In other words, you can replace a subset of B of the same cardinality as I by I and still get a base. Probably only works in a finitary matroid.

[Peter Nelson]

Aha - yes, that should be true in a finitary matroid.

[Peter Nelson]

It’s not something I’ve encountered, though

[Peter Nelson]

I’m very happy to see this application. Allowing my matroids to be infinite was a consequential decision that created a lot of extra work in API-building, and this use of infinite matroids suggests it might have been actually worth it!

(Matroids are finite in most of the literature)

[Junyan Xu]

I think it's a trivial consequence of the invariance of cardinality of bases. You can always extend I to a basis using only elements from B: take X = I ∪ B in indep_maximal, and show a maximal independent set in X must be a base using indep_aug), and this basis has the same cardinality as B. Restrict the equivalence to I will give the desired injection f.

[Junyan Xu]

Hmm, we at least already have one theorem docs#Matroid.Base.ncard_eq_ncard_of_base about invariance of cardinality of bases: it applies to any matroid, but only shows cardinalities are equal if they are finite.

[Junyan Xu]

For the infinite case, I think I can translate stacks#030F's proof in ~an hour.

[Peter Nelson]

I know the proof of the matroid statement, and it’s worth doing at that generality, I think. From your perspective, leaving it as a sorry is probably the best use of your time.

[Junyan Xu]

I mean I can translate it to the matroid setting.

[Peter Nelson]

Oh I see - for what it’s worth, here’s a sketch of a purely matroidal proof. Don’t know how much it differs conceptually from the algebraic one. I’ve phrased it in terms of stuff that is already in mathlib. Apologies for the typesetting - still on mobile.

It suffices to show that for any pair of infinite bases B,B’, the cardinality of B’ is at most that of B. Since M is finitary and B is a base, for each y in B’, there is a finite independent subset C(y) of B such that C(y) + y is dependent, or C(y) = {y}

Let A(y) be the preimage of C(y) under C. Now C(y) is a basis of C(y) union A(y), and A(y) is independent, so |A(y)| \le |C(y)| - it follows that C is a function from B’ to Finset B with finite fibres. Both sets are infinite, so B’ is not larger than B in cardinality.

[Junyan Xu]

Thanks! The last paragraph is a bit different from (and might be harder to formalize than) Stacks' proof. My plan is just to show that the union of all the C(y) is B.

[Peter Nelson]

That will work, too - and you're right that my last paragraph is annoying to formalize. I'm looking forward to seeing where this goes. Please ping me if there is some fact you need that you think may be matroidal - there's a good chance it'll be somewhere in my repo.

[Junyan Xu]

It seems I need to use Matroid.Indep.exists_insert_of_not_base, since there isn't a way to obtain IndepMatroid directly from Matroid. It's also slightly annoying to split into B' \ B and B ∩ B'. And now I realize I may need to create a new file since importing Cardinal.mul_aleph0_eq adds ~100 transitive imports ...

[Peter Nelson]

On the first point, you shouldn't be interacting much with IndepMatroid. (the only lemmas/functions with IndepMatroid in the type signature should be IndepMatroid.matroid and IndepMatroid.of_____). The idea is that you define an IndepMatroid from one of the constructors, then immediately use IndepMatroid.matroid to turn it into a Matroid, and use the Matroid API.

IndepMatroid is simply a way to add some organization to the many ways of building a matroid via the independence axioms.

[Peter Nelson]

In particular, you should have algebraicMatroidOf (something) : Matroid \a := IndepMatroid.matroid <| IndepMatroid.ofFinitary _ _ _ _.

[Junyan Xu]

I can change the IndepMatroid.algebraicIndependent to a Matroid if IndepMatroid is not be be exposed. However, the indep_aug in IndepMatroid.ofFinitary seems harder to prove than that in IndepMatroid, so I simply directly constructed an IndepMatroid.

[Peter Nelson]

That works, too - the constructor used isn't important, but IndepMatroid being solely internal is key to the design, to avoid API duplication. I think the simplifier should give you want you need if you stick to Matroid.

[Junyan Xu]

I've finished the proof! Took longer than expected but not very difficult
image.png

[Junyan Xu]

I think it would be nicer to make IndepMatroid.matroid be able to change the defeq of the data field Base. For example in this case I'd like the Base to be defeq to IsTranscendenceBasis.

[Junyan Xu]

However I expect that matroids will only be used as an auxiliary construction here (albeit a great effort saver) and most API will still revolve around AlgebraicIndependent and IsTranscendenceBasis.

[Peter Nelson]

Junyan Xu said:

I think it would be nicer to make IndepMatroid.matroid be able to change the defeq of the data field Base. For example in this case I'd like the Base to be defeq to IsTranscendenceBasis.

This is a reasonable request. I didn't focus on the defeq aspect, but I think an alternative form of IndepMatroid.matroid where Base can be defeq would make sense.

Matroid.ofExistsMatroid does something similar, but still doesn't give definitional bases.

[Junyan Xu]

I'm now developing some API for transcendence degree (trdeg).
Puzzle: this answer shows that docs#Module.rank may not be attained by a linearly independent set, even over a commutative ring. Could trdeg also not be attained by an algebraic independent set (of course, in some algebra that is not a domain)?
There is an analogue of StrongRankCondition in the context of transcendence that holds even for non-domains (lemma 1 of the paper of Hamann). Once we show that in/surjective AlgHoms give inequalities between trdegs, we will then be able to show that the trdeg of an algebra is at most the cardinality of any generating set. Transitivity of trdeg (stacks#030H) is another nice target.

[Peter Nelson]

Junyan Xu said:

I think it would be nicer to make IndepMatroid.matroid be able to change the defeq of the data field Base. For example in this case I'd like the Base to be defeq to IsTranscendenceBasis.

#20876 . I've designed it a little differently from your suggestion, so it will interact with other ways of defining matroids (closure function, circuits, etc) in the future. But Matroid.congrBaseIndep from that PR will do what you need.

[Peter Nelson]

Junyan Xu said:

I can change the IndepMatroid.algebraicIndependent to a Matroid if IndepMatroid is not be be exposed. However, the indep_aug in IndepMatroid.ofFinitary seems harder to prove than that in IndepMatroid, so I simply directly constructed an IndepMatroid.

#20877 provides the constructor you wanted here.

[Junyan Xu]

Opened #20888 for the matroid equal cardinality result and #20887 for transcendence degree.

[Peter Nelson]

I’m thinking of making a PR that defines a cardinal-valued rank function for a finitary matroid and proves basic properties like monotonicity, submodularity, etc.

Transcendence degree will be a special case - are there any particular statements about transcendence degree that you would like to have available?

[Junyan Xu]

I found a fairly short proof of Lüroth's theorem (~1 page) in Jacobson's Basic Algebra II on p.522 which doesn't rely on the transcendence degree. (The reason I looked into it is because I asked DeepSeek-r1 a question and it quotes Jacobson as a reference.)

[Antoine Chambert-Loir]

(That's the classic proof that is given in most algebra books. Note you'll have to prove 8.38 before that, which is interesting in its own right. That'll a be a good test of the one-variable two-variables interaction in mathlib.)

[Junyan Xu]

I think @Jz Pan proved [F(t):F(t^n)]=n but I forgot what PR it is. I recall during the PR review I suggested the more general statement identical to 8.38 and might have suggested something about the proof. (Edit: the comment is here.)

[Jz Pan]

I think I only proved F(t^n) ≠ F(t^m) for n ≠ m in PR #7788. You had a comment on that PR.

[Junyan Xu]

#20887 is ready for review again. In the last two commits I've built a dictionary between the matroid language and the algebraic language, and proven trdeg inequalities from injective/surjective AlgHom / finite type algebras. trdeg is computed for (Mv)Polynomial algebras but only over domains. To generalize to any nontrivial comm. rings we need the result of Hamann.

[Junyan Xu]

The PR now depends on:

#21512 matroid lemmas, reviewed by @Peter Nelson

[Junyan Xu]

#21566 removes unnecessary injectivity assumptions around algebraicity of algebras, should be uncontroversial.

[Jz Pan]

Junyan Xu said:

To generalize to any nontrivial comm. rings we need the result of Hamann.

How complicated is it? Would you like to work on it in future PRs?

[Junyan Xu]

It's a one-paragraph proof that can be reasonably expected to be done in one day. If any PKU student is interested I could work with them on it ...

[Junyan Xu]

All we need is this, I think.
image.png