English
The perfect closure is equipped with a bilinear multiplication defined by lifting the product of representatives; the product of mk x and mk y is mk of the appropriate sum of the first components and a product of the second components after Frobenius shifts.
Русский
Совершенное замыкание оснащено умножением, определяемым поLift: произведение mk x и mk y равно mk суммы первых координат и произведения вторых координат после смещений Фробениуса.
LaTeX
$$$\\forall x,y:\\mathbb{N}\\times K,\\; mk\\,K\\,p\\,x * mk\\,K\\,p\\,y = mk\\,K\\,p\\big( x.1+y.1, (\\mathrm{frobenius}\\,K\\,p)^{[y.1]} x.2 \\cdot (\\mathrm{frobenius}\\,K\\,p)^{[x.1]} y.2 \\big)$$$
Lean4
instance instMul : Mul (PerfectClosure K p) :=
⟨Quot.lift
(fun x : ℕ × K =>
Quot.lift (fun y : ℕ × K => mk K p (x.1 + y.1, (frobenius K p)^[y.1] x.2 * (frobenius K p)^[x.1] y.2))
(mul_aux_right K p x))
fun x1 x2 (H : R K p x1 x2) => funext fun e => Quot.inductionOn e fun y => mul_aux_left K p x1 x2 y H⟩
