feat(Algebra): Transcendence degree (#20887)

Define transcendence degree `Algebra.trdeg` and proves some basic properties:

In **AlgebraicIndependent/Basic.lean**: define `Algebra.trdeg` to be the supremum of the cardinalities of all AlgebraicIndependent sets, just like `Module.rank` is defined to be the supremum of the cardinalities of all LinearIndependent sets. Add some API lemmas and trivial results about `trdeg`, e.g. that injective/surjective AlgHoms induce inequalities between `trdeg`s, and AlgEquivs induce equalities.

In **AlgebraicIndependent/Transcendental.lean**: add API lemmas and show the inequality `trdeg R S + trdeg S A ≤ trdeg R A` (which does not require a domain).

In **AlgebraicIndependent/Defs.lean**: add Stacks tags and some trivial API lemmas about IsTranscendenceBasis.

Thanks to Chris Hughes and Jz Pan for preliminary works and Peter Nelson for the hint about Finitary and IndepMatroid.

TODO:

+ [The analogue of StrongRankCondition](https://mathoverflow.net/a/484564) in the setting of algebras, which implies `trdeg R (MvPolynomial (Fin n) R) = n` for all Nontrivial CommRing R.

Author: alreadydone

Mathlib/RingTheory/Algebraic/Integral.lean

@@ -187,7 +187,7 @@ theorem iff_exists_smul_integral [IsReduced R] :
   ⟨(exists_integral_multiple ·), fun ⟨_, hy, int⟩ ↦
     of_smul_isIntegral (by rwa [isNilpotent_iff_eq_zero]) int⟩
 
-section trans
+section restrictScalars
 
 variable (R) [NoZeroDivisors S]
 
@@ -247,7 +247,7 @@ theorem _root_.IsIntegral.trans_isAlgebraic [alg : Algebra.IsAlgebraic R S]
   · have := Module.nontrivial S A
     exact h.isAlgebraic.restrictScalars _
 
-end trans
+end restrictScalars
 
 variable [nzd : NoZeroDivisors R] {a b : S} (ha : IsAlgebraic R a) (hb : IsAlgebraic R b)
 include ha
@@ -323,6 +323,9 @@ def Subalgebra.algebraicClosure [IsDomain R] : Subalgebra R S where
   add_mem' ha hb := ha.add hb
   algebraMap_mem' := isAlgebraic_algebraMap
 
+theorem Subalgebra.mem_algebraicClosure [IsDomain R] {x : S} :
+    x ∈ algebraicClosure R S ↔ IsAlgebraic R x := Iff.rfl
+
 theorem integralClosure_le_algebraicClosure [IsDomain R] :
     integralClosure R S ≤ Subalgebra.algebraicClosure R S :=
   fun _ ↦ IsIntegral.isAlgebraic
@@ -361,6 +364,29 @@ theorem IsAlgebraic.of_mul [NoZeroDivisors R] {y z : S} (hy : y ∈ nonZeroDivis
   rw [mul_right_comm, eq, ← Algebra.smul_def] at this
   exact this.of_smul (mem_nonZeroDivisors_of_ne_zero hr)
 
+open Algebra in
+omit [Algebra R A] [IsScalarTower R S A] in
+theorem IsAlgebraic.adjoin_of_forall_isAlgebraic [NoZeroDivisors S] {s t : Set S}
+    (alg : ∀ x ∈ s \ t, IsAlgebraic (adjoin R t) x) {a : A}
+    (ha : IsAlgebraic (adjoin R s) a) : IsAlgebraic (adjoin R t) a := by
+  set Rs := adjoin R s
+  set Rt := adjoin R t
+  let Rts := adjoin Rt s
+  let _ : Algebra Rs Rts := (Subalgebra.inclusion
+    (T := Rts.restrictScalars R) <| adjoin_le <| by apply subset_adjoin).toAlgebra
+  have : IsScalarTower Rs Rts A := .of_algebraMap_eq fun ⟨a, _⟩ ↦ rfl
+  have : Algebra.IsAlgebraic Rt Rts := by
+    have := ha.nontrivial
+    have := Subtype.val_injective (p := (· ∈ Rs)).nontrivial
+    have := (isDomain_iff_noZeroDivisors_and_nontrivial Rt).mpr ⟨inferInstance, inferInstance⟩
+    rw [← Subalgebra.isAlgebraic_iff, isAlgebraic_adjoin_iff]
+    intro x hs
+    by_cases ht : x ∈ t
+    · exact isAlgebraic_algebraMap (⟨x, subset_adjoin ht⟩ : Rt)
+    exact alg _ ⟨hs, ht⟩
+  have : IsAlgebraic Rts a := ha.extendScalars (by apply Subalgebra.inclusion_injective)
+  exact this.restrictScalars Rt
+
 namespace Transcendental
 
 section

Mathlib/RingTheory/AlgebraicIndependent/Basic.lean

@@ -20,10 +20,6 @@ This file contains basic results on algebraic independence of a family of elemen
 
 * [Stacks: Transcendence](https://stacks.math.columbia.edu/tag/030D)
 
-## TODO
-Define the transcendence degree and show it is independent of the choice of a
-transcendence basis.
-
 ## Tags
 transcendence basis, transcendence degree, transcendence
 
@@ -34,9 +30,17 @@ noncomputable section
 
 open Function Set Subalgebra MvPolynomial Algebra
 
-variable {ι ι' R K A A' : Type*} {x : ι → A}
+universe u v v'
+
+variable {ι : Type u} {ι' R : Type*} {A : Type v} {A' : Type v'} {x : ι → A}
 variable [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A']
 
+variable (R A) in
+/-- The transcendence degree of a commutative algebra `A` over a commutative ring `R` is
+defined to be the maximal cardinality of an `R`-algebraically independent set in `A`. -/
+@[stacks 030G] def Algebra.trdeg : Cardinal.{v} :=
+  ⨆ ι : { s : Set A // AlgebraicIndepOn R _root_.id s }, Cardinal.mk ι.1
+
 theorem algebraicIndependent_iff_ker_eq_bot :
     AlgebraicIndependent R x ↔
       RingHom.ker (MvPolynomial.aeval x : MvPolynomial ι R →ₐ[R] A).toRingHom = ⊥ :=
@@ -47,6 +51,9 @@ 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]
 
+instance [FaithfulSMul R A] : Nonempty { s : Set A // AlgebraicIndepOn R id s } :=
+  ⟨∅, algebraicIndependent_empty_type_iff.mpr <| FaithfulSMul.algebraMap_injective R A⟩
+
 namespace AlgebraicIndependent
 
 variable (hx : AlgebraicIndependent R x)
@@ -114,6 +121,14 @@ theorem of_aeval {f : ι → MvPolynomial ι R}
 
 end AlgebraicIndependent
 
+theorem isEmpty_algebraicIndependent (h : ¬ Injective (algebraMap R A)) :
+    IsEmpty { s : Set A // AlgebraicIndepOn R id s } where
+  false s := h s.2.algebraMap_injective
+
+theorem trdeg_eq_zero_of_not_injective (h : ¬ Injective (algebraMap R A)) : trdeg R A = 0 := by
+  have := isEmpty_algebraicIndependent h
+  rw [trdeg, ciSup_of_empty, bot_eq_zero]
+
 theorem MvPolynomial.algebraicIndependent_X (σ R : Type*) [CommRing R] :
     AlgebraicIndependent R (X (R := R) (σ := σ)) := by
   rw [AlgebraicIndependent, aeval_X_left]
@@ -126,9 +141,30 @@ theorem AlgHom.algebraicIndependent_iff (f : A →ₐ[R] A') (hf : Injective f)
   ⟨fun h => h.of_comp f, fun h => h.map hf.injOn⟩
 
 @[nontriviality]
-theorem algebraicIndependent_of_subsingleton [Subsingleton R] : AlgebraicIndependent R x :=
+theorem AlgebraicIndependent.of_subsingleton [Subsingleton R] : AlgebraicIndependent R x :=
   algebraicIndependent_iff.2 fun _ _ => Subsingleton.elim _ _
 
+@[deprecated (since := "2025-02-07")] alias algebraicIndependent_of_subsingleton :=
+  AlgebraicIndependent.of_subsingleton
+
+theorem isTranscendenceBasis_iff_of_subsingleton [Subsingleton R] (x : ι → A) :
+    IsTranscendenceBasis R x ↔ Nonempty ι := by
+  have := Module.subsingleton R A
+  refine ⟨fun h ↦ ?_, fun h ↦ ⟨.of_subsingleton, fun s hs hx ↦
+    hx.antisymm fun a _ ↦ ⟨Classical.arbitrary _, Subsingleton.elim ..⟩⟩⟩
+  by_contra hι; rw [not_nonempty_iff] at hι
+  have := h.2 {0} .of_subsingleton
+  simp [range_eq_empty, eq_comm (a := ∅)] at this
+
+@[nontriviality] theorem IsTranscendenceBasis.of_subsingleton [Subsingleton R] [Nonempty ι] :
+    IsTranscendenceBasis R x :=
+  (isTranscendenceBasis_iff_of_subsingleton x).mpr ‹_›
+
+@[nontriviality] theorem trdeg_subsingleton [Subsingleton R] : trdeg R A = 1 :=
+  have := Module.subsingleton R A
+  (ciSup_le' fun s ↦ by simpa using Set.subsingleton_of_subsingleton).antisymm <| le_ciSup_of_le
+    (Cardinal.bddAbove_range _) ⟨{0}, .of_subsingleton⟩ (by simp)
+
 theorem algebraicIndependent_adjoin (hs : AlgebraicIndependent R x) :
     @AlgebraicIndependent ι R (adjoin R (range x))
       (fun i : ι => ⟨x i, subset_adjoin (mem_range_self i)⟩) _ _ _ :=
@@ -236,14 +272,83 @@ theorem algebraicIndependent_empty_iff :
 
 end Subtype
 
-theorem AlgebraicIndependent.to_subtype_range {ι} {f : ι → A} (hf : AlgebraicIndependent R f) :
-    AlgebraicIndependent R ((↑) : range f → A) := by
+theorem AlgebraicIndependent.to_subtype_range (hx : AlgebraicIndependent R x) :
+    AlgebraicIndependent R ((↑) : range x → A) := by
+  nontriviality R
+  rwa [algebraicIndependent_subtype_range hx.injective]
+
+theorem AlgebraicIndependent.to_subtype_range' (hx : AlgebraicIndependent R x) {t}
+    (ht : range x = t) :AlgebraicIndependent R ((↑) : t → A) :=
+  ht ▸ hx.to_subtype_range
+
+theorem IsTranscendenceBasis.to_subtype_range (hx : IsTranscendenceBasis R x) :
+    IsTranscendenceBasis R ((↑) : range x → A) := by
+  cases subsingleton_or_nontrivial R
+  · rw [isTranscendenceBasis_iff_of_subsingleton] at hx ⊢; infer_instance
+  · rwa [isTranscendenceBasis_subtype_range hx.1.injective]
+
+theorem IsTranscendenceBasis.to_subtype_range' (hx : IsTranscendenceBasis R x) {t}
+    (ht : range x = t) : IsTranscendenceBasis R ((↑) : t → A) :=
+  ht ▸ hx.to_subtype_range
+
+theorem AlgEquiv.isTranscendenceBasis (e : A ≃ₐ[R] A') (hx : IsTranscendenceBasis R x) :
+    IsTranscendenceBasis R (e ∘ x) := by
+  refine ⟨by apply hx.1.map' (id e.injective : Injective e.toAlgHom), fun s hs hxs ↦ ?_⟩
+  rw [AlgebraicIndepOn, ← e.symm.toAlgHom.algebraicIndependent_iff e.symm.injective] at hs
+  rw [range_comp, hx.2 _ hs.to_subtype_range, ← range_comp, ← comp_assoc, range_comp]
+  · convert s.image_id <;> (ext; simp)
+  rintro _ ⟨i, rfl⟩
+  exact ⟨⟨_, hxs ⟨i, rfl⟩⟩, by simp⟩
+
+theorem AlgEquiv.isTranscendenceBasis_iff (e : A ≃ₐ[R] A') :
+    IsTranscendenceBasis R (e ∘ x) ↔ IsTranscendenceBasis R x :=
+  ⟨fun hx ↦ by convert e.symm.isTranscendenceBasis hx; ext; simp, e.isTranscendenceBasis⟩
+
+section trdeg
+
+open Cardinal
+
+theorem AlgebraicIndependent.lift_cardinalMk_le_trdeg [Nontrivial R]
+    (hx : AlgebraicIndependent R x) : lift.{v} #ι ≤ lift.{u} (trdeg R A) := by
+  rw [lift_mk_eq'.mpr ⟨.ofInjective _ hx.injective⟩, lift_le]
+  exact le_ciSup_of_le (bddAbove_range _) ⟨_, hx.to_subtype_range⟩ le_rfl
+
+theorem AlgebraicIndependent.cardinalMk_le_trdeg [Nontrivial R] {ι : Type v} {x : ι → A}
+    (hx : AlgebraicIndependent R x) : #ι ≤ trdeg R A := by
+  rw [← (#ι).lift_id, ← (trdeg R A).lift_id]; exact hx.lift_cardinalMk_le_trdeg
+
+theorem lift_trdeg_le_of_injective (f : A →ₐ[R] A') (hf : Injective f) :
+    lift.{v'} (trdeg R A) ≤ lift.{v} (trdeg R A') := by
+  nontriviality R
+  rw [trdeg, lift_iSup (bddAbove_range _)]
+  exact ciSup_le' fun i ↦ (i.2.map' hf).lift_cardinalMk_le_trdeg
+
+theorem trdeg_le_of_injective {A' : Type v} [CommRing A'] [Algebra R A'] (f : A →ₐ[R] A')
+    (hf : Injective f) : trdeg R A ≤ trdeg R A' := by
+  rw [← (trdeg R A).lift_id, ← (trdeg R A').lift_id]; exact lift_trdeg_le_of_injective f hf
+
+theorem lift_trdeg_le_of_surjective (f : A →ₐ[R] A') (hf : Surjective f) :
+    lift.{v} (trdeg R A') ≤ lift.{v'} (trdeg R A) := by
   nontriviality R
-  rwa [algebraicIndependent_subtype_range hf.injective]
+  rw [trdeg, lift_iSup (bddAbove_range _)]
+  refine ciSup_le' fun i ↦ (lift_cardinalMk_le_trdeg (x := fun a : i.1 ↦ (⇑f).invFun a) <|
+    of_comp f ?_)
+  convert i.2; simp [invFun_eq (hf _)]
+
+theorem trdeg_le_of_surjective {A' : Type v} [CommRing A'] [Algebra R A'] (f : A →ₐ[R] A')
+    (hf : Surjective f) : trdeg R A' ≤ trdeg R A := by
+  rw [← (trdeg R A).lift_id, ← (trdeg R A').lift_id]; exact lift_trdeg_le_of_surjective f hf
+
+theorem AlgEquiv.lift_trdeg_eq (e : A ≃ₐ[R] A') :
+    lift.{v'} (trdeg R A) = lift.{v} (trdeg R A') :=
+  (lift_trdeg_le_of_injective e.toAlgHom e.injective).antisymm
+    (lift_trdeg_le_of_surjective e.toAlgHom e.surjective)
+
+theorem AlgEquiv.trdeg_eq {A' : Type v} [CommRing A'] [Algebra R A'] (e : A ≃ₐ[R] A') :
+    trdeg R A = trdeg R A' := by
+  rw [← (trdeg R A).lift_id, e.lift_trdeg_eq, lift_id]
 
-theorem AlgebraicIndependent.to_subtype_range' {ι} {f : ι → A} (hf : AlgebraicIndependent R f) {t}
-    (ht : range f = t) : AlgebraicIndependent R ((↑) : t → A) :=
-  ht ▸ hf.to_subtype_range
+end trdeg
 
 theorem algebraicIndependent_comp_subtype {s : Set ι} :
     AlgebraicIndependent R (x ∘ (↑) : s → A) ↔
@@ -299,8 +404,8 @@ theorem algebraicIndependent_sUnion_of_directed {s : Set (Set A)} (hsn : s.Nonem
   exact algebraicIndependent_iUnion_of_directed hs.directed_val (by simpa using h)
 
 theorem exists_maximal_algebraicIndependent (s t : Set A) (hst : s ⊆ t)
-    (hs : AlgebraicIndependent R ((↑) : s → A)) : ∃ u, s ⊆ u ∧
-      Maximal (fun (x : Set A) ↦ AlgebraicIndependent R ((↑) : x → A) ∧ x ⊆ t) u := by
+    (hs : AlgebraicIndepOn R id s) : ∃ u, s ⊆ u ∧
+      Maximal (fun (x : Set A) ↦ AlgebraicIndepOn R id x ∧ x ⊆ t) u := by
   refine zorn_subset_nonempty { u : Set A | AlgebraicIndependent R ((↑) : u → A) ∧ u ⊆ t}
     (fun c hc chainc hcn ↦ ⟨⋃₀ c, ⟨?_, ?_⟩, fun _ ↦ subset_sUnion_of_mem⟩) s ⟨hs, hst⟩
   · exact algebraicIndependent_sUnion_of_directed hcn chainc.directedOn (fun x hxc ↦ (hc hxc).1)
@@ -374,7 +479,7 @@ theorem AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin
 
 section Field
 
-variable [Field K] [Algebra K A]
+variable {K : Type*} [Field K] [Algebra K A]
 
 /- Porting note: removing `simp`, not in simp normal form. Could make `Function.Injective f` a
 simp lemma when `f` is a field hom, and then simp would prove this -/

Mathlib/RingTheory/AlgebraicIndependent/Defs.lean

@@ -47,9 +47,13 @@ variable [CommRing R] [CommRing A] [CommRing A'] [Algebra R A] [Algebra R A']
 /-- `AlgebraicIndependent R x` states the family of elements `x`
   is algebraically independent over `R`, meaning that the canonical
   map out of the multivariable polynomial ring is injective. -/
-def AlgebraicIndependent : Prop :=
+@[stacks 030E "(1)"] def AlgebraicIndependent : Prop :=
   Injective (MvPolynomial.aeval x : MvPolynomial ι R →ₐ[R] A)
 
+/-- `AlgebraicIndepOn R v s` states that the elements in the family `v` that are indexed by the
+elements of `s` are algebraically independent over `R`. -/
+abbrev AlgebraicIndepOn (s : Set ι) : Prop := AlgebraicIndependent R fun i : s ↦ x i
+
 variable {R} {x}
 
 theorem algebraicIndependent_iff :
@@ -145,9 +149,30 @@ end repr
 
 end AlgebraicIndependent
 
-variable (R)
-
+variable (R) in
 /-- A family is a transcendence basis if it is a maximal algebraically independent subset. -/
-def IsTranscendenceBasis (x : ι → A) : Prop :=
+@[stacks 030E "(4)"] def IsTranscendenceBasis (x : ι → A) : Prop :=
   AlgebraicIndependent R x ∧
-    ∀ (s : Set A) (_ : AlgebraicIndependent R ((↑) : s → A)) (_ : range x ≤ s), range x = s
+    ∀ (s : Set A) (_ : AlgebraicIndepOn R id s) (_ : range x ⊆ s), range x = s
+
+theorem isTranscendenceBasis_iff_maximal {s : Set A} :
+    IsTranscendenceBasis R ((↑) : s → A) ↔ Maximal (AlgebraicIndepOn R id) s := by
+  rw [IsTranscendenceBasis, maximal_iff, Subtype.range_val]; rfl
+
+theorem isTranscendenceBasis_equiv (e : ι ≃ ι') {f : ι' → A} :
+    IsTranscendenceBasis R (f ∘ e) ↔ IsTranscendenceBasis R f := by
+  simp_rw [IsTranscendenceBasis, algebraicIndependent_equiv, EquivLike.range_comp]
+
+theorem isTranscendenceBasis_equiv' (e : ι ≃ ι') {f : ι' → A} {g : ι → A} (h : f ∘ e = g) :
+    IsTranscendenceBasis R g ↔ IsTranscendenceBasis R f :=
+  h ▸ isTranscendenceBasis_equiv e
+
+theorem isTranscendenceBasis_subtype_range {ι} {f : ι → A} (hf : Injective f) :
+    IsTranscendenceBasis R ((↑) : range f → A) ↔ IsTranscendenceBasis R f :=
+  .symm <| isTranscendenceBasis_equiv' (Equiv.ofInjective f hf) rfl
+
+alias ⟨IsTranscendenceBasis.of_subtype_range, _⟩ := isTranscendenceBasis_subtype_range
+
+theorem isTranscendenceBasis_image {ι} {s : Set ι} {f : ι → A} (hf : Set.InjOn f s) :
+    IsTranscendenceBasis R (fun x : s ↦ f x) ↔ IsTranscendenceBasis R fun x : f '' s ↦ (x : A) :=
+  isTranscendenceBasis_equiv' (Equiv.Set.imageOfInjOn _ _ hf) rfl

Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean

@@ -81,7 +81,7 @@ theorem IsTranscendenceBasis.isAlgebraic [Nontrivial R] (hx : IsTranscendenceBas
     Algebra.IsAlgebraic (adjoin R (range x)) A := by
   constructor
   intro a
-  rw [← not_iff_comm.1 (hx.1.option_iff _).symm]
+  rw [← not_iff_comm.1 (hx.1.option_iff_transcendental _).symm]
   intro ai
   have h₁ : range x ⊆ range fun o : Option ι => o.elim a x := by
     rintro x ⟨y, rfl⟩