English
The natural map to ZMod(p) is compatible with the residue construction coming from the local ring.
Русский
Естественное отображение в ZMod(p) совместимо с остаточным отображением локального поля/кольца.
LaTeX
$$toZMod_p = residueField.toRingHom \circ IsLocalRing.residue_p$$
Lean4
theorem appr_spec (n : ℕ) : ∀ x : ℤ_[p], x - appr x n ∈ Ideal.span {(p : ℤ_[p]) ^ n} :=
by
simp only [Ideal.mem_span_singleton]
induction n with
| zero => simp only [_root_.pow_zero, isUnit_one, IsUnit.dvd, forall_const]
| succ n ih =>
intro x
dsimp only [appr]
split_ifs with h
· rw [h]
apply dvd_zero
push_cast
rw [sub_add_eq_sub_sub]
obtain ⟨c, hc⟩ := ih x
simp only [map_natCast, ZMod.natCast_self, RingHom.map_pow, RingHom.map_mul, ZMod.natCast_val]
have hc' : c ≠ 0 := by
rintro rfl
simp only [mul_zero] at hc
contradiction
conv_rhs =>
congr
simp only [hc]
rw [show (x - (appr x n : ℤ_[p])).valuation = ((p : ℤ_[p]) ^ n * c).valuation by rw [hc]]
rw [valuation_p_pow_mul _ _ hc', Nat.cast_add, add_sub_cancel_left, _root_.pow_succ, ← mul_sub]
apply mul_dvd_mul_left
obtain hc0 | hc0 := eq_or_ne c.valuation 0
· simp only [hc0, mul_one, _root_.pow_zero, Nat.cast_zero, Int.natAbs_zero]
rw [mul_comm, unitCoeff_spec h] at hc
suffices c = unitCoeff h
by
rw [← this, ← Ideal.mem_span_singleton, ← maximalIdeal_eq_span_p]
apply toZMod_spec
lift c to ℤ_[p]ˣ using by simp [isUnit_iff, norm_eq_zpow_neg_valuation hc', hc0]
rw [IsDiscreteValuationRing.unit_mul_pow_congr_unit _ _ _ _ _ hc]
exact irreducible_p
· simp only [Int.natAbs_natCast, zero_pow hc0, sub_zero, ZMod.cast_zero, mul_zero]
rw [unitCoeff_spec hc']
exact (dvd_pow_self (p : ℤ_[p]) hc0).mul_left _
