English
There is a canonical ring homomorphism from K into the perfect closure of K at p, sending each x in K to the equivalence class of (0, x). This map preserves addition and multiplication and sends 1 to 1.
Русский
Существует каноническое кольцеподобие из K в PerfectClosure(K, p), отправляющее x ∈ K в эквивалентность mk(0, x). Это отображение сохраняет сложение и умножение и отправляет 1 в 1.
LaTeX
$$$\exists \iota: K \to^+ \mathrm{PerfectClosure}(K,p)\quad\text{таким, что}\quad \iota(x)=\mathrm{mk}(K,p)(0,x)\quad\text{для всех }x\in K.$$$
Lean4
/-- Embedding of `K` into `PerfectClosure K p` -/
def of : K →+* PerfectClosure K p where
toFun x := mk _ _ (0, x)
map_one' := rfl
map_mul' _ _ := rfl
map_zero' := rfl
map_add' _ _ := rfl
