exists_mem_adjoin_mul_eq_pow_natDegree_le

English

In the same setting as above, for every i, if the degree of f.map R→S is at most i, there exists y in adjoin R({x}) such that (algebraMap p) y = x^{i}.

Русский

В той же постановке для каждого i существует y в адьойн R({x}) такое, что $a_p y = x^i$ при условии, что deg(f.map) ≤ i.

LaTeX

$$∀ i, (f.map (algebraMap R S)).natDegree ≤ i → ∃ y ∈ adjoin R ({ x } : Set S), (algebraMap R S) p * y = x ^ i$$

Lean4

theorem exists_mem_adjoin_mul_eq_pow_natDegree_le {x : S} (hx : aeval x f = 0) (hmo : f.Monic)
    (hf : f.IsWeaklyEisensteinAt (Submodule.span R { p })) :
    ∀ i, (f.map (algebraMap R S)).natDegree ≤ i → ∃ y ∈ adjoin R ({ x } : Set S), (algebraMap R S) p * y = x ^ i :=
  by
  intro i hi
  obtain ⟨k, hk⟩ := exists_add_of_le hi
  rw [hk, pow_add]
  obtain ⟨y, hy, H⟩ := exists_mem_adjoin_mul_eq_pow_natDegree hx hmo hf
  refine ⟨y * x ^ k, ?_, ?_⟩
  · exact Subalgebra.mul_mem _ hy (Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton x)) _)
  · rw [← mul_assoc _ y, H]

Похожие утверждения