exists_pow_mem_range_tensorProduct

English

Let k ⊆ K and R be as above with IsPurelyInseparable k K. For any q and x ∈ R ⊗_k K, there exists n with x^{q^n} in the range of algebraMap R (R ⊗_k K).

Русский

Пусть k ⊆ K и R как выше, и IsPurelyInseparable k K. Для любого q и x ∈ R ⊗_k K существует n, такое что x^{q^n} ∈ образ алгебраMap R (R ⊗_k K).

LaTeX

$$$\exists n, x^{q^n} \in \operatorname{range}(\operatorname{algebraMap} R (R \otimes_k K))$$$

Lean4

theorem exists_pow_mem_range_tensorProduct [IsPurelyInseparable k K] (x : R ⊗[k] K) :
    ∃ n > 0, x ^ n ∈ (algebraMap R (R ⊗[k] K)).range :=
  by
  let q := ringExpChar k
  obtain ⟨n, hr⟩ := exists_pow_pow_mem_range_tensorProduct_of_expChar q x
  refine ⟨q ^ n, pow_pos ?_ _, hr⟩
  obtain (hq | hq) := expChar_is_prime_or_one k q <;> simp [hq, Nat.Prime.pos]

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