Searching for a theorem: Degree of `K/k` vs `K(x)/k(x)`.

Stream: mathlib4

[Xavier Généreux]

Hi everyone,

I wanted to know if the following theorem is in Mathlib in some form :
If $K/k$ is a finite extension of degree $n$ then so is $K(x)/k(x)$.
See here for example.

I could not find it after searching for a little while.
Thanks!
Xavier

[Luigi Massacci]

@loogle FiniteDimensional, RatFunc

[loogle]

:search: functionField_iff

[Luigi Massacci]

Probably not there?

[Junyan Xu]

This is also known as stacks#0G1M and it's essentially saying that k(x) and K are linearly disjoint over k in K(x), see e.g. docs#IntermediateField.LinearDisjoint.linearIndependent_left.
I think it's true and (it would be interesting to prove) that K(x) is in fact isomorphic to the tensor product of k(x) and K over k. (For this you only need that K/k is algebraic; it's interesting to think how this works under the bases of the rational function fields given by partial fractions.) Since K(x) is a field this would imply k(x) and K are "absolutely" linearly disjoint over k (docs#IntermediateField.LinearDisjoint.of_isField').
cc @Jz Pan

[Junyan Xu]

We know that k[X] ⊗[k] K ≃ K[X] and therefore k(X) ⊗[k] K ≃ (k[X]\0)⁻¹k(X) ⊗[k] K ≃ (k[X]\0)⁻¹K[X]. But the RHS is just K(X) because every nonzero polynomial in K[X] divides a nonzero polynomial in k[X] if K/k is algebraic: docs#Irreducible.exists_dvd_monic_irreducible_of_isIntegral (just needs to remove replace Irreducible by nonzero)

[Xavier Généreux]

Thank you yes I was looking at this kind of theorem!

[Xavier Généreux]

But there didn't seem to be something that would give me what I wanted for free.

[Junyan Xu]

Here's a complete proof with a sorry that I'm going to PR soon:

import Mathlib

variable (k K : Type*)

open Polynomial TensorProduct nonZeroDivisors

noncomputable section

variable [CommRing k] [IsDomain k] [CommRing K] [IsDomain K] [Algebra k K] [FaithfulSMul k K]

theorem Polynomial.exists_dvd_map_of_isAlgebraic [Algebra.IsAlgebraic k K] (f : K[X])
    (hf : f ≠ 0) : ∃ g : k[X], g ≠ 0 ∧ f ∣ g.map (algebraMap k K) :=
  sorry

attribute [local instance] Polynomial.algebra

instance : Algebra.IsPushout k k[X] K K[X] := .symm inferInstance

variable [Algebra.IsAlgebraic k K]

instance : IsLocalization
    (Algebra.algebraMapSubmonoid K[X] k[X]⁰) (FractionRing K[X]) :=
  (IsLocalization.iff_of_le_of_exists_dvd _ K[X]⁰
    (map_le_nonZeroDivisors_of_injective _
      (map_injective _ <| FaithfulSMul.algebraMap_injective ..) le_rfl) fun _p hp ↦
        have ⟨q, ne, eq⟩ := exists_dvd_map_of_isAlgebraic k K _ (ne_zero hp)
        ⟨_, ⟨q, mem_nonZeroDivisors_of_ne_zero ne, rfl⟩, eq⟩).mpr
    inferInstance

-- TODO: upgrade to AlgEquiv
def ratFuncLinearEquiv : FractionRing k[X] ⊗[k[X]] K[X] ≃ₗ[k[X]] FractionRing K[X] :=
  IsLocalizedModule.linearEquiv k[X]⁰ (TensorProduct.mk _ _ _ 1)
    (IsScalarTower.toAlgHom k[X] K[X] <| FractionRing K[X]).toLinearMap

def ratFuncLinearEquiv' : FractionRing k[X] ⊗[k] K ≃ₗ[k[X]] FractionRing K[X] :=
  AlgebraTensorModule.congr (TensorProduct.rid k[X] <| FractionRing k[X]).symm (.refl k K) ≪≫ₗ
    AlgebraTensorModule.assoc .. ≪≫ₗ congr (.refl ..) (Algebra.IsPushout.equiv k k[X] K K[X]) ≪≫ₗ ratFuncLinearEquiv k K

instance : FaithfulSMul k[X] (FractionRing K[X]) :=
  (faithfulSMul_iff_algebraMap_injective ..).mpr <|
    (IsFractionRing.injective K[X] _).comp (map_injective _ <| FaithfulSMul.algebraMap_injective ..)

end

attribute [local instance] Polynomial.algebra FractionRing.liftAlgebra

theorem ratFunc_rank_eq [Field k] [CommRing K] [IsDomain K] [Algebra k K] [Algebra.IsAlgebraic k K] :
    Module.rank (FractionRing k[X]) (FractionRing K[X]) = Module.rank k K := by
  have := IsLocalization.linearMap_compatibleSMul k[X]⁰ (FractionRing k[X])
  have eq := (ratFuncLinearEquiv' k K).restrictScalars (FractionRing k[X])|>.symm.lift_rank_eq
  simpa [Module.rank_baseChange] using eq

[Jz Pan]

Maybe in this case IsFractionRing is more convenient?

[Jz Pan]

Do you know k(X) ⊗[k] K is a domain? If yes, then it's automatically a field by docs#Algebra.TensorProduct.isField_of_isAlgebraic.

[Junyan Xu]

a sorry that I'm going to PR soon

The PR is #21566 but I'm still working to remove more injectivity hypotheses ...

Do you know k(X) ⊗[k] K is a domain?

That's basically equivalent to linear disjointness right? There isn't a very slick proof for this in the question other than the one by Martin Brandenburg, which is basically my proof.

Maybe in this case IsFractionRing is more convenient?

It could be but I'm not sure I want to try ... I find RatFunc is missing some instances so I'm not using it. (It's defined as a structure possibly originally for performance reasons (mathlib3 commit), but probably this is no longer needed now and we can just make RatFunc an abbrev for FractionRing (Polynomial _).)

[Jz Pan]

Junyan Xu said:

I find RatFunc is missing some instances so I'm not using it. (It's defined as a structure possibly originally for performance reasons (mathlib3 commit), but probably this is no longer needed now and we can just make RatFunc an abbrev for FractionRing (Polynomial _).)

I have already noticed it in here #Is there code for X? > `MvRatFunc`?

[Jz Pan]

Junyan Xu said:

That's basically equivalent to linear disjointness right?

Yes, that is "relative" linearly disjoint. I'm just wondering if its proof does not required your sorried proof.

[Jz Pan]

I think your sorried result is closely related to docs#Irreducible.exists_dvd_monic_irreducible_of_isIntegral which is introduced in #9522.

[Junyan Xu]

Yes, I've put it right under that lemma.

[Junyan Xu]

We should generalize to "MvRatFunc" (FractionRing of MvPolynomial) to get the full Stacks result but I'm not sure what the shortest route to that is ... by induction and take direct limit? Hmm maybe I can show that any nonzero MvPolynomial in K divides a nonzero MvPolynomial in k too ...

[Jz Pan]

Junyan Xu said:

Hmm maybe I can show that any nonzero MvPolynomial in K divides a nonzero MvPolynomial in k too ...

I think this is better as one can describe explicitly the isomorphism k(X_i) ⊗[k] K ≃ K(X_i).

[Junyan Xu]

By the way this is an interesting question that came up that both DeepSeek-r1 and OpenAI o3-mini (free) are able to provide correct proofs; given existing mathlib it can be proven in four lines in RingTheory/Algebraic/Basic.

Let A be an S-algebra and let S be an R-algebra, such that S is a domain, the composition R->S->A is injective, and S is algebraic over R (meaning every element of S is a root of a nonzero polynomial with coefficients in R). Clearly R->S must be injective and therefore R is also a domain. Does it follow that S->A is also injective?

[Junyan Xu]

#21566 ready for review

[Junyan Xu]

Here's a question they're unable to solve, not even coming close; I can prove them if either R or S is a domain, but am not sure about the general case. r1 thinks there's a counterexample with R=Z and S=Z[1/2], which doesn't work because Z is a domain; o3 thinks S[X] is an algebraic R[X]-algebra iff S is a finite R-algebramodule, which is clearly too strong (it knows finite -> integral).

Let S be an algebraic algebra over a commutative ring R, meaning that every element of S is a root of some nonzero polynomial with coefficients in R. Does it follow that the polynomial ring S[X] is also an algebraic algebra over R[X]?

[Jz Pan]

I think you only need to show the case that S/R is finite? For any g of S[X], let S' be the subalgebra of S/R generated by coefficients of g, then S'/R is finite and g is in S'[X].

[Junyan Xu]

o3's answer actually says finite R-module, not finite type R-algebra (corrected above). Not sure how to do this case either. A more general question (whose positve answer implies a positive answer for the previous question) is:

If A is an R-algebra and there exists an injective R-algebra homomorphism R[X,Y]->A[X], does it follow that there exists an injective R-algebra homomorphism R[X]->A?

[Kevin Buzzard]

Junyan Xu said:

Let S be an algebraic algebra over a commutative ring R, meaning that every element of S is a root of some nonzero polynomial with coefficients in R. Does it follow that the polynomial ring S[X] is also an algebraic algebra over R[X]?

Does this not follow from the fact that the algebraic elements are a subalgebra and they contain S?

[Junyan Xu]

That's basically how I prove the domain case. The subalgebra is Subalgebra.algebraicClosure.

[Kevin Buzzard]

Are you saying this doesn't work in the general case? What is the counterexample?

[Junyan Xu]

Algebraic elements don't necessarily form a subalgebra in general, see https://mathoverflow.net/questions/482944/when-do-algebraic-elements-form-a-subalgebra
(In fact it can happen that the square of an algebraic element is transcendental.)

[Kevin Buzzard]

Oh the polynomial needn't be monic? Is this a sensible notion?

[Jz Pan]

Kevin Buzzard said:

Oh the polynomial needn't be monic? Is this a sensible notion?

It's docs#IsIntegral if the polynomial in question is required to be monic.

[Junyan Xu]

It's natural from the point of view of transcendence/algebraic independence which are about injectivity of maps from (Mv)Polynomial to an algebra (while algebraicity means non-injectivity), and there were at least two MO questions asked under this definition of algebraic (independence), and work of Hamann in the 1980s that studies these notions.

The notion involving monic polynomials is called docs#IsIntegral, and for injective algebra maps between domains, algebraicity is equivalent to integrality of the extension of fraction fields, but it's convenient to work on the level of domains rather than constantly passing to the fraction fields and dealing with the commutative diagrams. Integrality enjoys better properties in general, for example transitivity in a tower A/S/R holds in full generality, but for algebraicity it needs S to be a domain (an unnecessary injectivity assumption is removed in #21566). In general, it's natural to ask whether theorems continue to hold without the IsDomain hypothesis.

[Kevin Buzzard]

In general, it's natural to ask whether theorems continue to hold without the IsDomain hypothesis.

I personally would disagree with this. Given all the counterexamples above it seems to me that the pragmatic conclusion is that algebraicity does not behave well away from domains and it's not worth spending time trying to work out which fragments of the theory hold more generally as these results are unlikely to ever be wanted for any real applications.

[Junyan Xu]

I agree that figuring out the most general conditions shouldn't block development, but these are certainly legitimate questions which I personally find interesting, especially questions not obviously connected to any known counterexamples after having seen many.

Extra assumptions do mean that the user has to supply it or Lean has to search for the instance. In this case they also mean we now have two versions of the same result with different assumptions which could potentially be unified in the future, and I do not find this aesthetically pleasing. Future people (at least some of them) reading the code will definitely be tempted to remove the conditions. I have made an effort to record counterexamples in the docstrings by e.g. adding link to MO quesitons so that people won't make vain attempts.
image.png

[Junyan Xu]

I have extracted a general statement from my proof above: if S is an algebraic R-algebra with injective algebra map where R is an integral domain, and if R' and S' are fraction rings of R and S respectively, then S' is the pushout of the R-algebras S and R' (docs#Algebra.IsPushout). Here we take R=k[X], S=K[X], R'=k(X) and S'=K(X). If we compose this with the pushout square with vertices k, K, k[X] and K[X], we get that K(X) is the pushout of the k-algebras K and k(X), and hence the equality of dimensions.

[Xavier Généreux]

Thanks a lot for this @Junyan Xu, that is exactly what I needed.

A question I have is on your TODO: upgrade to AlgEquiv, how would you go about that? I think it would be nice to have.

[Junyan Xu]

We can get it from docs#Algebra.IsPushout.equiv if we follow my suggested new approach using IsPushout.

[Junyan Xu]

In fact this works

import Mathlib

variable (k K : Type*)

open Polynomial TensorProduct nonZeroDivisors

noncomputable section

variable [CommRing k] [IsDomain k] [CommRing K] [IsDomain K] [Algebra k K] [FaithfulSMul k K]

attribute [local instance] Polynomial.algebra

instance : Algebra.IsPushout k k[X] K K[X] := .symm inferInstance

variable [Algebra.IsAlgebraic k K]

instance : IsLocalization
    (Algebra.algebraMapSubmonoid K[X] k[X]⁰) (FractionRing K[X]) :=
  (IsLocalization.iff_of_le_of_exists_dvd _ K[X]⁰
    (map_le_nonZeroDivisors_of_injective _
      (map_injective _ <| FaithfulSMul.algebraMap_injective ..) le_rfl) fun _p hp ↦
        have ⟨q, ne, eq⟩ := exists_dvd_map_of_isAlgebraic k _ (ne_zero hp)
        ⟨_, ⟨q, mem_nonZeroDivisors_of_ne_zero ne, rfl⟩, eq⟩).mpr
    inferInstance

instance : FaithfulSMul k[X] (FractionRing K[X]) :=
  (faithfulSMul_iff_algebraMap_injective ..).mpr <|
    (IsFractionRing.injective K[X] _).comp (map_injective _ <| FaithfulSMul.algebraMap_injective ..)

attribute [local instance] Polynomial.algebra FractionRing.liftAlgebra

-- upgraded to AlgEquiv
def ratFuncAlgEquiv : FractionRing k[X] ⊗[k[X]] K[X] ≃ₐ[k[X]] FractionRing K[X] :=
  have := (Algebra.isPushout_of_isLocalization k[X]⁰ (FractionRing k[X]) K[X] (FractionRing K[X])).symm
  (Algebra.IsPushout.equiv ..).restrictScalars _

def ratFuncLinearEquiv' : FractionRing k[X] ⊗[k] K ≃ₗ[k[X]] FractionRing K[X] :=
  AlgebraTensorModule.congr (TensorProduct.rid k[X] <| FractionRing k[X]).symm (.refl k K) ≪≫ₗ
    AlgebraTensorModule.assoc .. ≪≫ₗ congr (.refl ..) (Algebra.IsPushout.equiv k k[X] K K[X]) ≪≫ₗ (ratFuncLinearEquiv k K).toLinearEquiv

end

attribute [local instance] Polynomial.algebra FractionRing.liftAlgebra

theorem ratFunc_rank_eq [Field k] [CommRing K] [IsDomain K] [Algebra k K] [Algebra.IsAlgebraic k K] :
    Module.rank (FractionRing k[X]) (FractionRing K[X]) = Module.rank k K := by
  have := IsLocalization.linearMap_compatibleSMul k[X]⁰ (FractionRing k[X])
  have eq := (ratFuncLinearEquiv' k K).restrictScalars (FractionRing k[X])|>.symm.lift_rank_eq
  simpa [Module.rank_baseChange] using eq

[Junyan Xu]

Opened #22966 for this

[Junyan Xu]

The proof eventually decomposes into the following facts:

• IsAlgebraic/IsIntegral R S + IsPushout R S R' S' ⇒ IsAlgebraic/IsIntegral R' S' (for the "IsAlgebraic" version we currently need to assume NoZeroDivisor R' and FaithfulSMul R R' (i.e. Injective (algebraMap R R'))

• IsAlgebraic R S + IsFractionRing R R' + IsFractionRing S S' ⇒ IsPushout R S R' S' (need to assume FaithfulSMul R S + NonZeroDivisors S)

• Base change along an injective map of domains preserves rank. (When proving this I've split results like IsLocalizedModule.rank_eq into two parts (IsLocalizedModule and IsLocalization), even though this isn't necessary. These results were added by @Andrew Yang in #9412.)

One of the proofs exhibits substantial universe yoga; the chained rewrites using lift_id', lift_lift, lift_umax etc. could potentially benefit from some tactic ("convert_to_univs/lifts"?) that auto-generates such rewrites given a goal expression involving iterated lifts.

[Jz Pan]

Junyan Xu said:

... could potentially benefit from some tactic ("convert_to_univs/lifts"?) that auto-generates such rewrites given a goal expression involving iterated lifts.

It was discussed here #mathlib4 > Universe-heterogeneous ordinal and cardinal relations

[Junyan Xu]

#23095 and #23096 have been split off the PR.