English
A variant of the finite-type criterion with a specified inj and a universal transcendence condition for finite subsets implies global algebraic independence.
Русский
Вариант критерия по конечному множеству с заданной инъекцией и всеобщим условием трансцендентности для конечных подмножеств влечет глобальную алгебраическую независимость.
LaTeX
$$$Function.Injective (algebraMap R A) \to ( \forall t, t.Finite \to AlgebraicIndependent R (fun i : t => x i) \to \forall a, a \in s, a \notin t \to Transcendental (adjoin R t) a) \to AlgebraicIndependent R ((↑) : s → A)$$
Lean4
theorem algebraicIndependent_of_set_of_finite (s : Set ι) (ind : AlgebraicIndependent R fun i : s ↦ x i)
(H :
∀ t : Set ι,
t.Finite →
AlgebraicIndependent R (fun i : t ↦ x i) → ∀ i ∉ s, i ∉ t → Transcendental (adjoin R (x '' t)) (x i)) :
AlgebraicIndependent R x := by
classical
refine algebraicIndependent_of_finite_type fun t hfin ↦ ?_
suffices AlgebraicIndependent R fun i : ↥(t ∩ s ∪ t \ s) ↦ x i from
this.comp (Equiv.setCongr (t.inter_union_diff s).symm) (Equiv.injective _)
refine
hfin.diff.induction_on_subset _ (ind.comp (inclusion <| by simp) (inclusion_injective _)) fun {a u} ha hu ha' h ↦ ?_
have : a ∉ t ∩ s ∪ u := (·.elim (ha.2 ·.2) ha')
convert
(((image_eq_range .. ▸ h.option_iff_transcendental <| x a).2 <|
H _ (hfin.subset (union_subset inter_subset_left <| hu.trans diff_subset)) h a ha.2 this).comp
_ (subtypeInsertEquivOption this).injective).comp
(Equiv.setCongr union_insert) (Equiv.injective _) with
x
by_cases h : ↑x = a <;> simp [h, Set.subtypeInsertEquivOption]
