English
A refined auxiliary statement supporting the existence of Frobenius-compatible solutions in the fraction field.
Русский
Уточненная вспомогательная формулировка, поддерживающая существование решений, совместимых с Фробениусом в дробной области.
LaTeX
$$exists_frobenius_solution_fractionRing_aux (continued)$$
Lean4
theorem exists_frobenius_solution_fractionRing_aux (m n : ℕ) (r' q' : 𝕎 k) (hr' : r'.coeff 0 ≠ 0) (hq' : q'.coeff 0 ≠ 0)
(hq : (p : 𝕎 k) ^ n * q' ∈ nonZeroDivisors (𝕎 k)) :
let b : 𝕎 k := frobeniusRotation p hr' hq'
IsFractionRing.ringEquivOfRingEquiv (frobeniusEquiv p k) (algebraMap (𝕎 k) (FractionRing (𝕎 k)) b) *
Localization.mk ((p : 𝕎 k) ^ m * r') ⟨(p : 𝕎 k) ^ n * q', hq⟩ =
(p : Localization (nonZeroDivisors (𝕎 k))) ^ (m - n : ℤ) * algebraMap (𝕎 k) (FractionRing (𝕎 k)) b :=
by
intro b
have key : WittVector.frobenius b * r' = q' * b := by linear_combination frobenius_frobeniusRotation p hr' hq'
have hq'' : algebraMap (𝕎 k) (FractionRing (𝕎 k)) q' ≠ 0 :=
by
have hq''' : q' ≠ 0 := fun h => hq' (by simp [h])
simpa only [Ne, map_zero] using (IsFractionRing.injective (𝕎 k) (FractionRing (𝕎 k))).ne hq'''
rw [zpow_sub₀ (FractionRing.p_nonzero p k)]
simp [field, FractionRing.p_nonzero p k]
convert congr_arg (fun x => algebraMap (𝕎 k) (FractionRing (𝕎 k)) x) key using 1
· simp only [RingHom.map_mul]
· simp only [RingHom.map_mul]
