English
In the Witt vector ring 𝕎 k, the element p (viewed as the Witt vector corresponding to the prime p) is irreducible.
Русский
В кольце Witt векторов 𝕎 k элемент p (как Witt-вектор, соответствующий простому p) неразложим.
LaTeX
$$$\text{IsIrreducible}(p : 𝕎 k)$$$
Lean4
theorem irreducible : Irreducible (p : 𝕎 k) :=
by
have hp : ¬IsUnit (p : 𝕎 k) := by
intro hp
simpa only [constantCoeff_apply, coeff_p_zero, not_isUnit_zero] using
(constantCoeff : WittVector p k →+* _).isUnit_map hp
refine ⟨hp, fun a b hab => ?_⟩
obtain ⟨ha0, hb0⟩ : a ≠ 0 ∧ b ≠ 0 := by rw [← mul_ne_zero_iff]; intro h; rw [h] at hab; exact p_nonzero p k hab
obtain ⟨m, a, ha, rfl⟩ := verschiebung_nonzero ha0
obtain ⟨n, b, hb, rfl⟩ := verschiebung_nonzero hb0
cases m; · exact Or.inl (isUnit_of_coeff_zero_ne_zero a ha)
rcases n with - | n; · exact Or.inr (isUnit_of_coeff_zero_ne_zero b hb)
rw [iterate_verschiebung_mul] at hab
apply_fun fun x => coeff x 1 at hab
simp only [coeff_p_one, Nat.add_succ, add_comm _ n, Function.iterate_succ', Function.comp_apply,
verschiebung_coeff_add_one, verschiebung_coeff_zero] at hab
exact (one_ne_zero hab).elim
