Transcendental and algebraically independent

Stream: PR reviews

[Jz Pan]

Some of my PRs with the goal to prove that if E/F is transcendental, then there are infinitely many F-embeddings from E to its algebraic closure.

• #18378 add some results on AlgebraicIndependent - already merged

[Jz Pan]

• #18433 some more results on transcendental and algebraically independent

This PR is ready for review.

• Transcendental.aeval_of_transcendental, Transcendental.of_aeval, transcendental_aeval_iff, IsAlgebraic.of_aeval_of_transcendental: Polynomial.aeval r f is transcendental if and only if r and f are both transcendental (in some sense)
• make is_transcendental_of_subsingleton a nontriviality lemma
• IsAlgebraic.[of_]ringHom, isAlgebraic_ringHom_iff: generalize the similar result for algHom
• Transcendental.of_tower_top[_of_injective]: negation of IsAlgebraic.tower_top[_of_injective]
• move MvPolynomial.transcendental_X to earlier file
• MvPolynomial.transcendental_supported_X[_iff]: X_i is transcendental in R[X_j | j \in S] if and only if i \notin S
• algebraicIndependent_of_finite_type': Type version of algebraicIndependent_of_finite' which will be used later

[Jz Pan]

The next step is prove this:

import Mathlib.RingTheory.AlgebraicIndependent
import Mathlib.Algebra.Polynomial.Lifts

noncomputable section

open Function Set Subalgebra MvPolynomial Algebra

open scoped Classical

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

theorem MvPolynomial.algebraicIndependent_aeval_pointwise
    (f : ι → Polynomial R) (hf : ∀ i, Transcendental R (f i)) :
    AlgebraicIndependent R fun i ↦ Polynomial.aeval (X i : MvPolynomial ι R) (f i) := by
  set x := fun i ↦ Polynomial.aeval (X i : MvPolynomial ι R) (f i)
  refine algebraicIndependent_of_finite_type' (C_injective _ _) fun t _ i hi ↦ ?_
  suffices H : Transcendental (supported R t) (x i) by
    rw [Transcendental] at H ⊢
    contrapose! H
    have hle : adjoin R (x '' t) ≤ supported R t := by
      rw [Algebra.adjoin_le_iff, Set.image_subset_iff]
      intro _ h
      rw [Set.mem_preimage]
      refine Algebra.adjoin_mono ?_ (Polynomial.aeval_mem_adjoin_singleton R _)
      simp_rw [singleton_subset_iff, Set.mem_image_of_mem _ h]
    letI := (Subalgebra.inclusion hle).toAlgebra
    haveI : IsScalarTower (adjoin R (x '' t)) (supported R t) (MvPolynomial ι R) :=
      .of_algebraMap_eq fun _ ↦ rfl
    exact H.tower_top_of_injective (Subalgebra.inclusion_injective hle)
  have h1 := transcendental_supported_X R hi
  have h2 := hf i
  sorry

[Jz Pan]

Which states that if f_i : R[X] are R-transcendental, then f_i(X_i) are R-algebraically independent in R[X_i | i \in ι].

My plan is to use algebraicIndependent_of_finite_type' and we only need to prove that if i \notin S, then f_i(X_i) is transcendental over R[X_j | j \in S]. It's known that X_i is transcendental over R[X_j | j \in S] and f_i : R[X] is transcendental over R. In order to use Transcendental.aeval_of_transcendental I need that f_i base changed to R[X_j | j \in S][X] is transcendental over R[X_j | j \in S]. which needs Module.Flat and which is not imported in this file.

I suspect that my proof is over-complicated. Any suggestion for a simpler proof?

[Jz Pan]

which needs Module.Flat and which is not imported in this file

Specifically, if A and S are R-algebras, a : A is transcendental over R, S is flat R-algebra, then a \otimes 1 : A \otimes_R S is transcendental over S. This just because - \otimes_R S preserves the injectivity of Polynomial.aeval.

[Jz Pan]

Jz Pan said:

that f_i base changed to R[X_j | j \in S][X] is transcendental over R[X_j | j \in S].

I think I have a proof of this without using flatness. More generally, if a : A is transcendental over R, then MvPolynomial.C a : MvPolynomial ι A is transcendental over MvPolynomial ι R. Because the aeval map (MvPolynomial ι A)[X] -> MvPolynomial ι R, under suitable isomorphism, is MvPolynomial ι A[X] -> MvPolynomial ι R, which is MvPolynomial.map of the original aeval, so it is also injective.

Similarly, AlgebraicIndependent is also preserved by MvPolynomial.C.

[Jz Pan]

I got the proof, but could someone please looking at compile error introduced by it? The following is MWE:

import Mathlib.RingTheory.AlgebraicIndependent
import Mathlib.Algebra.Polynomial.Lifts

noncomputable section

open Function Set Subalgebra MvPolynomial Algebra

open scoped Classical

variable {σ R S A ι : Type*} [CommRing R] [CommRing S] [CommRing A]
  [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A]

theorem algebraicIndependent_of_finite_type' {x : ι → A}
    (hinj : Injective (algebraMap R A))
    (H : ∀ t : Set ι, t.Finite → ∀ i : ι, i ∉ t → Transcendental (adjoin R (x '' t)) (x i)) :
    AlgebraicIndependent R x := sorry

open Polynomial in
variable (R) in
theorem MvPolynomial.transcendental_supported_polynomial_aeval_X {i : σ} {s : Set σ} (h : i ∉ s)
    {f : R[X]} (hf : Transcendental R f) :
    Transcendental (supported R s) (Polynomial.aeval (X i : MvPolynomial σ R) f) := sorry

theorem Transcendental.of_tower_top_of_injective
    (hinj : Function.Injective (algebraMap R S)) {x : A}
    (h : Transcendental S x) : Transcendental R x := sorry

theorem MvPolynomial.algebraicIndependent_aeval_pointwise
    (f : ι → Polynomial R) (hf : ∀ i, Transcendental R (f i)) :
    AlgebraicIndependent R fun i ↦ Polynomial.aeval (X i : MvPolynomial ι R) (f i) := by
  set x := fun i ↦ Polynomial.aeval (X i : MvPolynomial ι R) (f i)
  refine algebraicIndependent_of_finite_type' (C_injective _ _) fun t _ i hi ↦ ?_
  have hle : adjoin R (x '' t) ≤ supported R t := by
    rw [Algebra.adjoin_le_iff, Set.image_subset_iff]
    intro _ h
    rw [Set.mem_preimage]
    refine Algebra.adjoin_mono ?_ (Polynomial.aeval_mem_adjoin_singleton R _)
    simp_rw [singleton_subset_iff, Set.mem_image_of_mem _ h]
  letI : Algebra (adjoin R (x '' t)) (supported R t) := (Subalgebra.inclusion hle).toAlgebra
  letI : Module (adjoin R (x '' t)) (supported R t) := Algebra.toModule
  letI : SMul (adjoin R (x '' t)) (supported R t) := Algebra.toSMul
  haveI : IsScalarTower (adjoin R (x '' t)) (supported R t) (MvPolynomial ι R) :=
    .of_algebraMap_eq fun _ ↦ rfl
  have h1 := transcendental_supported_polynomial_aeval_X R hi (hf i)
  have h2 := Subalgebra.inclusion_injective hle
  sorry
  -- out of memory
  exact (transcendental_supported_polynomial_aeval_X R hi (hf i)).of_tower_top_of_injective
    (Subalgebra.inclusion_injective hle)

example : True := by
  exact False

[Jz Pan]

Firstly there are 3 results which are already proved in #18433 . Then it's the problematic proof. If you don't comment sorry then there will be a red line on exact False. If you comment out sorry then the red line on exact False goes, which means that it never get compiled. In my computer, the proof just stuck at the last exact forever. I've commit the code to github (https://github.com/leanprover-community/mathlib4/pull/18433/commits/967933442168b322716601e4f24770f8edc1cdd7) and the CI just said Lean exited with code 137, google tells me it means "out of memory".

[Jz Pan]

Fixed by extracting intermediate results as lemmas :sweat_smile:

[Johan Commelin]

I've kicked #18433 on the merge queue

[Jz Pan]

Thank you! I'll working on remaining results.

[Jz Pan]

PR #18661 is ready for review, which adds IsLocalization.algEquivOfAlgEquiv and some other results, which will be used for construction of isomorphism between rational function fields and IntermediateField.adjoin for algebraically independent elements.

[Jz Pan]

PR #18648 is ready for review, which 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.