English
Another form of the finite-type criterion using an injective algebra map, transferring finite-subset independence to the whole set.
Русский
Еще одна форма критерия по конечному множеству через инъективное отображение алгебраической карты, передающая независимость из конечного множества на всё множество.
LaTeX
$$$Function.Injective (algebraMap R A) \to ( \forall t, t.Finite \to AlgebraicIndependent R (fun i => x i) \to \forall a, a \in s, a \notin t \to Transcendental (adjoin R t) a) \to AlgebraicIndependent R (Subtype.val)$$
Lean4
/-- Variant of `algebraicIndependent_of_finite_type` using `Transcendental`. -/
theorem algebraicIndependent_of_finite_type' (hinj : Injective (algebraMap R A))
(H :
∀ t : Set ι,
t.Finite → AlgebraicIndependent R (fun i : t ↦ x i) → ∀ i ∉ t, Transcendental (adjoin R (x '' t)) (x i)) :
AlgebraicIndependent R x :=
algebraicIndependent_of_set_of_finite ∅ (algebraicIndependent_empty_type_iff.mpr hinj) fun t ht ind i _ ↦ H t ht ind i
