exists_algebraMap_eq_of_pow_mem_subalgebra

English

Let S be a subalgebra of A with IsIntegrallyClosedIn S A. If x^n ∈ S for some n>0, then x ∈ S (in the sense that x is the image of some element of S).

Русский

Пусть S — подалгебра A, и IsIntegrallyClosedIn S A. Если x^n ∈ S для некоторого n>0, то x ∈ S (то есть x есть образ элемента из S).

LaTeX

$$$\forall x\in A,\; \forall n>0,\; x^n\in S \Rightarrow \exists y\in S, algebraMap S A y = x$$$

Lean4

theorem exists_algebraMap_eq_of_pow_mem_subalgebra {A : Type*} [CommRing A] [Algebra R A] {S : Subalgebra R A}
    [IsIntegrallyClosedIn S A] {x : A} {n : ℕ} (hn : 0 < n) (hx : x ^ n ∈ S) : ∃ y : S, algebraMap S A y = x :=
  exists_algebraMap_eq_of_isIntegral_pow hn <| isIntegral_iff.mpr ⟨⟨x ^ n, hx⟩, rfl⟩

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