From 61e165bd538a53cb1212417246b1c54cef6076fd Mon Sep 17 00:00:00 2001
From: acmepjz <acme_pjz@hotmail.com>
Date: Fri, 1 Nov 2024 01:29:04 +0800
Subject: [PATCH] move `MvPolynomial.transcendental_X` to earlier file

---
 Mathlib/RingTheory/Algebraic.lean            | 40 ++++++++++++++++++++
 Mathlib/RingTheory/AlgebraicIndependent.lean |  4 --
 2 files changed, 40 insertions(+), 4 deletions(-)

diff --git a/Mathlib/RingTheory/Algebraic.lean b/Mathlib/RingTheory/Algebraic.lean
index 96cdbf5fafdbc..25a9faffb7d2a 100644
--- a/Mathlib/RingTheory/Algebraic.lean
+++ b/Mathlib/RingTheory/Algebraic.lean
@@ -7,6 +7,7 @@ import Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
 import Mathlib.RingTheory.Polynomial.IntegralNormalization
 import Mathlib.RingTheory.LocalRing.Basic
 import Mathlib.Algebra.Polynomial.Lifts
+import Mathlib.Algebra.MvPolynomial.Supported
 
 /-!
 # Algebraic elements and algebraic extensions
@@ -697,3 +698,42 @@ theorem Polynomial.algebraMap_pi_self_eq_eval :
   rfl
 
 end Pi
+
+namespace MvPolynomial
+
+variable {σ : Type*} (R : Type*) [CommRing R]
+
+theorem transcendental_supported_X {i : σ} {s : Set σ} (h : i ∉ s) :
+    Transcendental (supported R s) (X i : MvPolynomial σ R) := by
+  rw [transcendental_iff_injective]
+  let f := (Subalgebra.val _).comp ((optionEquivLeft R s).symm |>.trans
+    (renameEquiv R (Set.subtypeInsertEquivOption h)).symm |>.trans
+    (supportedEquivMvPolynomial _).symm).toAlgHom
+  let g := ((Polynomial.aeval (R := supported R s) (X i : MvPolynomial σ R)).restrictScalars R).comp
+    (Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm).toAlgHom
+  have hinj : Function.Injective f := by
+    simp only [f, AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_comp, AlgHom.coe_coe, Subalgebra.coe_val,
+      EquivLike.injective_comp, Subtype.val_injective]
+  have hfg : f = g := by
+    ext1
+    · ext1
+      simp [f, g, Set.subtypeInsertEquivOption, Subalgebra.algebraMap_eq]
+    · simp [f, g, Set.subtypeInsertEquivOption]
+  simpa only [hfg, g, AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_comp, AlgHom.coe_coe,
+    EquivLike.injective_comp, AlgHom.coe_restrictScalars'] using hinj
+
+theorem transcendental_X (i : σ) : Transcendental R (X i : MvPolynomial σ R) := by
+  have := transcendental_supported_X R (Set.not_mem_empty i)
+  let f := (Algebra.botEquivOfInjective (MvPolynomial.C_injective σ R)).symm.trans
+    (Subalgebra.equivOfEq _ _ supported_empty).symm |>.toRingEquiv
+  rwa [Transcendental, ← isAlgebraic_ringHom_iff f (RingHom.id (MvPolynomial σ R))
+    Function.injective_id (by ext1; rfl), RingHom.id_apply, ← Transcendental]
+
+theorem transcendental_supported_X_iff [Nontrivial R] {i : σ} {s : Set σ} :
+    Transcendental (supported R s) (X i : MvPolynomial σ R) ↔ i ∉ s := by
+  refine ⟨?_, transcendental_supported_X R⟩
+  rw [Transcendental, not_imp_not]
+  exact fun h ↦ isAlgebraic_algebraMap
+    (⟨X i, Algebra.subset_adjoin (Set.mem_image_of_mem _ h)⟩ : supported R s)
+
+end MvPolynomial
diff --git a/Mathlib/RingTheory/AlgebraicIndependent.lean b/Mathlib/RingTheory/AlgebraicIndependent.lean
index 74b086dc8a41c..80a62eb38f8cc 100644
--- a/Mathlib/RingTheory/AlgebraicIndependent.lean
+++ b/Mathlib/RingTheory/AlgebraicIndependent.lean
@@ -173,10 +173,6 @@ theorem algebraicIndependent_X : AlgebraicIndependent R (X (R := R) (σ := σ))
   rw [AlgebraicIndependent, aeval_X_left]
   exact injective_id
 
-variable {σ} in
-theorem transcendental_X (i : σ) : Transcendental R (X (R := R) i) :=
-  (algebraicIndependent_X σ R).transcendental i
-
 end MvPolynomial
 
 open AlgebraicIndependent