English
The perfect closure of R in A consists of those x ∈ A for which there exists n ∈ ℕ with x^{p^n} lying in the image of R
Русский
Совершенное замыкание R в A состоит из тех элементов x ∈ A, для которых существует n ∈ ℕ такое, что x^{p^n} лежит в образе R в A
LaTeX
$$\operatorname{perfectClosure} R A p = { x ∈ A ∣ ∃ n ∈ ℕ, x^{p^n} ∈ \operatorname{range}(\operatorname{algebraMap} R A) }$$
Lean4
/-- The perfect closure of `R` in `A` are the elements `x : A` such that `x ^ p ^ n`
is in `R` for some `n`, where `p` is the exponential characteristic of `R`. -/
def perfectClosure : Subalgebra R A
where
carrier := {x : A | ∃ n : ℕ, x ^ p ^ n ∈ (algebraMap R A).rangeS}
add_mem' := by
rintro x y ⟨n, hx⟩ ⟨m, hy⟩
use n + m
rw [add_pow_expChar_pow, pow_add, pow_mul, mul_comm (_ ^ n), pow_mul]
exact add_mem (pow_mem hx _) (pow_mem hy _)
mul_mem' := by
rintro x y ⟨n, hx⟩ ⟨m, hy⟩
use n + m
rw [mul_pow, pow_add, pow_mul, mul_comm (_ ^ n), pow_mul]
exact mul_mem (pow_mem hx _) (pow_mem hy _)
algebraMap_mem' := fun x ↦ ⟨0, by rw [pow_zero, pow_one]; exact ⟨x, rfl⟩⟩
