English
The Frobenius rotation yields a Witt vector b such that φ(b) a1 = b a2.
Русский
Вращение Фробениуса порождает Witt-вектор b так, что φ(b) a1 = b a2.
LaTeX
$$frobeniusRotation p ha1 ha2 : 𝕎 k and frobenius (frobeniusRotation p ha1 ha2) * a1 = frobeniusRotation p ha1 ha2 * a2$$
Lean4
theorem frobenius_frobeniusRotation {a₁ a₂ : 𝕎 k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) :
frobenius (frobeniusRotation p ha₁ ha₂) * a₁ = frobeniusRotation p ha₁ ha₂ * a₂ :=
by
ext n
rcases n with - | n
· simp only [WittVector.mul_coeff_zero, WittVector.coeff_frobenius_charP, frobeniusRotation, coeff_mk,
frobeniusRotationCoeff]
exact solution_spec' _ ha₁ _
· simp only [nthRemainder_spec, WittVector.coeff_frobenius_charP, frobeniusRotation, coeff_mk, frobeniusRotationCoeff]
have := succNthVal_spec' p n a₁ a₂ (fun i : Fin (n + 1) => frobeniusRotationCoeff p ha₁ ha₂ i.val) ha₁ ha₂
simp only [frobeniusRotationCoeff, Fin.val_zero] at this
convert this using 3; clear this
apply TruncatedWittVector.ext
intro i
simp only [WittVector.coeff_truncateFun, WittVector.coeff_frobenius_charP]
rfl
