English
Every polynomial over the direct limit comes from some component via the canonical map; i.e., there exists i and p such that the map of i sends p to q.
Русский
Каждый полином над прямым пределом исходит из некоторой компоненты через каноническое отображение.
LaTeX
$$$\exists i\, p: \text{Polynomial.map} (\text{of} \; i)\, p = q$$$
Lean4
nonrec theorem exists_of [Nonempty ι] [IsDirected ι (· ≤ ·)] (q : Polynomial (DirectLimit G fun i j h ↦ f' i j h)) :
∃ i p, Polynomial.map (of G (fun i j h ↦ f' i j h) i) p = q :=
Polynomial.induction_on q
(fun z ↦
let ⟨i, x, h⟩ := exists_of z
⟨i, C x, by rw [map_C, h]⟩)
(fun q₁ q₂ ⟨i₁, p₁, ih₁⟩ ⟨i₂, p₂, ih₂⟩ ↦
let ⟨i, h1, h2⟩ := exists_ge_ge i₁ i₂
⟨i, p₁.map (f' i₁ i h1) + p₂.map (f' i₂ i h2),
by
rw [Polynomial.map_add, map_map, map_map, ← ih₁, ← ih₂]
congr 2 <;> ext x <;> simp_rw [RingHom.comp_apply, of_f]⟩)
fun n z _ ↦
let ⟨i, x, h⟩ := exists_of z
⟨i, C x * X ^ (n + 1), by rw [Polynomial.map_mul, map_C, h, Polynomial.map_pow, map_X]⟩
