English
There exists a nonzero b in the fraction field giving a Frobenius-compatible relation with a and the Witt-rotation construct.
Русский
Существуют не нулевые элементы b в дробной области, дающие отношение совместимое с Фробениусом через вращение Witt.
LaTeX
$$exists_frobenius_solution_fractionRing {a} : ∃ b ≠ 0, ∃ m, φ b * a = p^{m} * b$$
Lean4
theorem exists_frobenius_solution_fractionRing {a : FractionRing (𝕎 k)} (ha : a ≠ 0) :
∃ᵉ (b ≠ 0) (m : ℤ), φ b * a = (p : FractionRing (𝕎 k)) ^ m * b :=
by
revert ha
refine Localization.induction_on a ?_
rintro ⟨r, q, hq⟩ hrq
have hq0 : q ≠ 0 := mem_nonZeroDivisors_iff_ne_zero.1 hq
have hr0 : r ≠ 0 := fun h => hrq (by simp [h])
obtain ⟨m, r', hr', rfl⟩ := exists_eq_pow_p_mul r hr0
obtain ⟨n, q', hq', rfl⟩ := exists_eq_pow_p_mul q hq0
let b := frobeniusRotation p hr' hq'
refine ⟨algebraMap (𝕎 k) (FractionRing (𝕎 k)) b, ?_, m - n, ?_⟩
·
simpa only [map_zero] using
(IsFractionRing.injective (WittVector p k) (FractionRing (WittVector p k))).ne
(frobeniusRotation_nonzero p hr' hq')
exact exists_frobenius_solution_fractionRing_aux p m n r' q' hr' hq' hq
