English
If x is a finite family in A, and A is algebraic over adjoin_R range x, and trdeg R A is finite, and certain size constraints hold, then x forms a transcendence basis of A over R.
Русский
Если x — конечный набор в A, A алгебраичен над adjoin_R range x и трансцендентный размер ограничен, тогда x образует трансцендентный базис A над R.
LaTeX
$$$ [Finite ι] [Algebra.IsAlgebraic (adjoin R (Set.range x)) A] (le : Cardinal.mk ι \\le trdeg R A) : IsTranscendenceBasis R x $$$
Lean4
theorem isTranscendenceBasis_of_lift_le_trdeg_of_finite [Finite ι] [alg : Algebra.IsAlgebraic (adjoin R (range x)) A]
(le : lift.{w} #ι ≤ lift.{u} (trdeg R A)) : IsTranscendenceBasis R x :=
by
have ⟨_, h⟩ := lift_mk_le'.mp (le.trans <| lift_le.mpr <| trdeg_le_cardinalMk R (range x))
have := rangeFactorization_surjective.bijective_of_nat_card_le (Nat.card_le_card_of_injective _ h)
refine .of_subtype_range (fun _ _ ↦ (this.1 <| Subtype.ext ·)) ?_
have := isDomain_of_adjoin_range R (range x)
rw [← matroid_spanning_iff, ← matroid_cRank_eq] at *
exact alg.isBase_of_le_cRank_of_finite (lift_le.mp <| mk_range_le_lift.trans le) (finite_range x)
