English
Same as above: x ∈ perfectClosure R A p iff ∃ n, x^{p^n} ∈ range(algebraMap R A).
Русский
То же самое: x ∈ perfectClosure R A p тогда и только тогда, когда ∃ n, x^{p^n} ∈ образ(алгебраMap R A).
LaTeX
$$x ∈ \operatorname{perfectClosure} R A p ↔ ∃ n ∈ ℕ, x^{p^n} ∈ \operatorname{range}(\operatorname{algebraMap} R A)$$
Lean4
theorem exists_pow_pow_mem_range_tensorProduct_of_expChar [IsPurelyInseparable k K] (q : ℕ) [ExpChar k q]
(x : R ⊗[k] K) : ∃ n, x ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range :=
by
nontriviality (R ⊗[k] K)
obtain (hq | hq) := expChar_is_prime_or_one k q
induction x with
| zero => exact ⟨0, 0, by simp⟩
| add x y h
h' =>
have : ExpChar (R ⊗[k] K) q := expChar_of_injective_ringHom (algebraMap k _).injective q
simp_rw [RingHom.mem_range, ← RingHom.mem_rangeS, ← Subalgebra.mem_perfectClosure_iff] at h h' ⊢
exact add_mem h h'
| tmul x y =>
obtain ⟨n, a, ha⟩ := IsPurelyInseparable.pow_mem k q y
use n
have : (x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n) = (x ^ q ^ n) ⊗ₜ[k] (1 : K) * (1 : R) ⊗ₜ[k] (y ^ q ^ n) := by
rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]
rw [Algebra.TensorProduct.tmul_pow, this]
refine Subring.mul_mem _ ⟨x ^ q ^ n, rfl⟩ ⟨algebraMap k R a, ?_⟩
rw [← IsScalarTower.algebraMap_apply, Algebra.TensorProduct.algebraMap_apply,
Algebra.TensorProduct.tmul_one_eq_one_tmul, ha]
· subst hq
have : CharZero k := charZero_of_expChar_one' k
exact
⟨0,
(Algebra.TensorProduct.includeLeft_surjective R _ <|
IsPurelyInseparable.surjective_algebraMap_of_isSeparable k K)
_⟩
