English
Frobenius acts on mk(x) by applying Frobenius to the second coordinates, leaving the first coordinate unchanged: frobenius.mk(x) = mk(x.fst, x.snd^p).
Русский
Фробениус действует на mk(x) тем образом: первый компонент не меняется, второй возводится в p-ую степень через Фробениуса.
LaTeX
$$$\\text{frobenius} (\\mathrm{PerfectClosure}\\,K\\,p)\\; p\\; (\\mathrm{mk}\\,K\\,p\\;x) = \\mathrm{mk}\\,K\\,p( x.1, x.2^{p})$$$
Lean4
theorem mk_eq_iff (x y : ℕ × K) :
mk K p x = mk K p y ↔ ∃ z, (frobenius K p)^[y.1 + z] x.2 = (frobenius K p)^[x.1 + z] y.2 :=
by
constructor
· intro H
replace H := Quot.eqvGen_exact H
induction H with
| rel x y H => obtain ⟨n, x⟩ := H; exact ⟨0, rfl⟩
| refl H => exact ⟨0, rfl⟩
| symm x y H ih => obtain ⟨w, ih⟩ := ih; exact ⟨w, ih.symm⟩
| trans x y z H1 H2 ih1 ih2 =>
obtain ⟨z1, ih1⟩ := ih1
obtain ⟨z2, ih2⟩ := ih2
exists z2 + (y.1 + z1)
rw [← add_assoc, iterate_add_apply, ih1]
rw [← iterate_add_apply, add_comm, iterate_add_apply, ih2]
rw [← iterate_add_apply]
simp only [add_comm, add_left_comm]
intro H
obtain ⟨m, x⟩ := x
obtain ⟨n, y⟩ := y
obtain ⟨z, H⟩ := H; dsimp only at H
rw [R.sound K p (n + z) m x _ rfl, R.sound K p (m + z) n y _ rfl, H]
rw [add_assoc, add_comm, add_comm z]
