feat(RingTheory/AlgebraicIndependent): add some results on AlgebraicIndependent (#18378)

- `algebraicIndependent_unique_type_iff`, `algebraicIndependent_iff_transcendental`: equivalency of `AlgebraicIndependent` and `Transcendental` for one-element family
- `AlgebraicIndependent.transcendental`: f a family `x` is algebraically independent, then any of its element is transcendental
- `MvPolynomial.(algebraicIndependent|transcendental)_X`: algebraic independent properties of intermediates of `MvPolynomial`
- `algebraicIndependent_of_finite'`: variant of `algebraicIndependent_of_finite` using `Transcendental`
- `exists_isTranscendenceBasis'`: `Type` version of `exists_isTranscendenceBasis`

Also changed one `¬IsAlgebraic` to `Transcendental`.

Also add `Set.subtypeInsertEquivOption` (used in the proof of `algebraicIndependent_of_finite'`) which is similar to `Finset.subtypeInsertEquivOption`. Note that it does not have simp lemmas yet, as the existing `Finset` one has no simp lemmas, either.

Author: acmepjz

Mathlib/Data/Set/Basic.lean

@@ -986,6 +986,24 @@ theorem forall_mem_insert {P : α → Prop} {a : α} {s : Set α} :
   forall₂_or_left.trans <| and_congr_left' forall_eq
 @[deprecated (since := "2024-03-23")] alias ball_insert_iff := forall_mem_insert
 
+/-- Inserting an element to a set is equivalent to the option type. -/
+def subtypeInsertEquivOption
+    [DecidableEq α] {t : Set α} {x : α} (h : x ∉ t) :
+    { i // i ∈ insert x t } ≃ Option { i // i ∈ t } where
+  toFun y := if h : ↑y = x then none else some ⟨y, (mem_insert_iff.mp y.2).resolve_left h⟩
+  invFun y := (y.elim ⟨x, mem_insert _ _⟩) fun z => ⟨z, mem_insert_of_mem _ z.2⟩
+  left_inv y := by
+    by_cases h : ↑y = x
+    · simp only [Subtype.ext_iff, h, Option.elim, dif_pos, Subtype.coe_mk]
+    · simp only [h, Option.elim, dif_neg, not_false_iff, Subtype.coe_eta, Subtype.coe_mk]
+  right_inv := by
+    rintro (_ | y)
+    · simp only [Option.elim, dif_pos]
+    · have : ↑y ≠ x := by
+        rintro ⟨⟩
+        exact h y.2
+      simp only [this, Option.elim, Subtype.eta, dif_neg, not_false_iff, Subtype.coe_mk]
+
 /-! ### Lemmas about singletons -/
 
 /- porting note: instance was in core in Lean3 -/

Mathlib/RingTheory/AlgebraicIndependent.lean

@@ -9,6 +9,7 @@ import Mathlib.LinearAlgebra.LinearIndependent
 import Mathlib.RingTheory.Adjoin.Basic
 import Mathlib.RingTheory.Algebraic
 import Mathlib.RingTheory.MvPolynomial.Basic
+import Mathlib.Data.Fin.Tuple.Reflection
 
 /-!
 # Algebraic Independence
@@ -82,6 +83,24 @@ theorem algebraicIndependent_empty_type_iff [IsEmpty ι] :
     AlgebraicIndependent R x ↔ Injective (algebraMap R A) := by
   rw [algebraicIndependent_iff_injective_aeval, MvPolynomial.aeval_injective_iff_of_isEmpty]
 
+/-- A one-element family `x` is algebraically independent if and only if
+its element is transcendental. -/
+@[simp]
+theorem algebraicIndependent_unique_type_iff [Unique ι] :
+    AlgebraicIndependent R x ↔ Transcendental R (x default) := by
+  rw [transcendental_iff_injective, algebraicIndependent_iff_injective_aeval]
+  let i := (renameEquiv R (Equiv.equivPUnit.{_, 1} ι)).trans (pUnitAlgEquiv R)
+  have key : aeval (R := R) x = (Polynomial.aeval (R := R) (x default)).comp i := by
+    ext y
+    simp [i, Subsingleton.elim y default]
+  simp [key]
+
+/-- The one-element family `![x]` is algebraically independent if and only if
+`x` is transcendental. -/
+theorem algebraicIndependent_iff_transcendental {x : A} :
+    AlgebraicIndependent R ![x] ↔ Transcendental R x := by
+  simp
+
 namespace AlgebraicIndependent
 
 theorem of_comp (f : A →ₐ[R] A') (hfv : AlgebraicIndependent R (f ∘ x)) :
@@ -138,8 +157,28 @@ theorem map {f : A →ₐ[R] A'} (hf_inj : Set.InjOn f (adjoin R (range x))) :
 theorem map' {f : A →ₐ[R] A'} (hf_inj : Injective f) : AlgebraicIndependent R (f ∘ x) :=
   hx.map hf_inj.injOn
 
+/-- If a family `x` is algebraically independent, then any of its element is transcendental. -/
+theorem transcendental (i : ι) : Transcendental R (x i) := by
+  have := hx.comp ![i] (Function.injective_of_subsingleton _)
+  have : AlgebraicIndependent R ![x i] := by rwa [← FinVec.map_eq] at this
+  rwa [← algebraicIndependent_iff_transcendental]
+
 end AlgebraicIndependent
 
+namespace MvPolynomial
+
+variable (σ R : Type*) [CommRing R]
+
+theorem algebraicIndependent_X : AlgebraicIndependent R (X (R := R) (σ := σ)) := by
+  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
 
 theorem AlgHom.algebraicIndependent_iff (f : A →ₐ[R] A') (hf : Injective f) :
@@ -409,13 +448,26 @@ theorem AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin
 
 theorem AlgebraicIndependent.option_iff (hx : AlgebraicIndependent R x) (a : A) :
     (AlgebraicIndependent R fun o : Option ι => o.elim a x) ↔
-      ¬IsAlgebraic (adjoin R (Set.range x)) a := by
-  rw [algebraicIndependent_iff_injective_aeval, isAlgebraic_iff_not_injective, Classical.not_not, ←
-    AlgHom.coe_toRingHom, ← hx.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin,
+      Transcendental (adjoin R (Set.range x)) a := by
+  rw [algebraicIndependent_iff_injective_aeval, transcendental_iff_injective,
+    ← AlgHom.coe_toRingHom, ← hx.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin,
     RingHom.coe_comp]
   exact Injective.of_comp_iff' (Polynomial.aeval a)
     (mvPolynomialOptionEquivPolynomialAdjoin hx).bijective
 
+/-- Variant of `algebraicIndependent_of_finite` using `Transcendental`. -/
+theorem algebraicIndependent_of_finite' (s : Set A)
+    (hinj : Injective (algebraMap R A))
+    (H : ∀ t ⊆ s, t.Finite → ∀ a ∈ s, a ∉ t → Transcendental (adjoin R t) a) :
+    AlgebraicIndependent R ((↑) : s → A) := by
+  classical
+  refine algebraicIndependent_of_finite s fun t hts hfin ↦ hfin.induction_on'
+    ((algebraicIndependent_empty_iff R A).2 hinj) fun {a} {u} ha hu ha' h ↦ ?_
+  convert ((Subtype.range_coe ▸ h.option_iff a).2 <| H u (hu.trans hts) (hfin.subset hu)
+    a (hts ha) ha').comp _ (Set.subtypeInsertEquivOption ha').injective
+  ext x
+  by_cases h : ↑x = a <;> simp [h, Set.subtypeInsertEquivOption]
+
 variable (R)
 
 /-- A family is a transcendence basis if it is a maximal algebraically independent subset. -/
@@ -432,6 +484,13 @@ theorem exists_isTranscendenceBasis (h : Injective (algebraMap R A)) :
   simp only [Subtype.range_coe_subtype, setOf_mem_eq] at *
   exact hs.2.eq_of_le ⟨ht, subset_univ _⟩ hst
 
+/-- `Type` version of `exists_isTranscendenceBasis`. -/
+theorem exists_isTranscendenceBasis' (R : Type u) {A : Type v} [CommRing R] [CommRing A]
+    [Algebra R A] (h : Injective (algebraMap R A)) :
+    ∃ (ι : Type v) (x : ι → A), IsTranscendenceBasis R x := by
+  obtain ⟨s, h⟩ := exists_isTranscendenceBasis R h
+  exact ⟨s, Subtype.val, h⟩
+
 variable {R}
 
 theorem AlgebraicIndependent.isTranscendenceBasis_iff {ι : Type w} {R : Type u} [CommRing R]