English
Let K be a commutative ring and p a prime with Char_p K p. For any type L and any function f: N × K → L which is constant on the equivalence relation R_K_p, there exists a unique extension F: PerfectClosure(K, p) → L such that F(mk(K, p, x)) = f(x) for all x ∈ N × K. In other words, functions respecting the relation R descend to the quotient PerfectClosure(K, p).
Русский
Пусть K — коммутативное кольцо, p — простое число, выполнены условия CharP(K, p). Для любого множества L и любой функции f: N × K → L, которая однозначно постоянна на эквивалентности, порожденной отношением R_K_p, существует единственное продолжение F: PerfectClosure(K, p) → L такое, что F(mk(K, p, x)) = f(x) для всех x ∈ N × K. Другими словами, функция, сохраняющая отношение R, спускается на фактор-множество PerfectClosure(K, p).
LaTeX
$$$\\forall K [\\text{CommRing }K], p [\\text{Prime }p], [\\text{CharP }K p], \\forall L, \\forall f: \\mathbb{N} \\times K \\to L, (\\forall x,y, R\,K\,p\,x\,y \\to f(x)=f(y)) \\Rightarrow \\exists! F: (\\mathrm{PerfectClosure}\\,K\\,p) \\to L, F\\circ \\mathrm{mk}\\,K\\,p = f$$$
Lean4
/-- Lift a function `ℕ × K → L` to a function on `PerfectClosure K p`. -/
def liftOn {L : Type*} (x : PerfectClosure K p) (f : ℕ × K → L) (hf : ∀ x y, R K p x y → f x = f y) : L :=
Quot.liftOn x f hf
