English
For a local ring R, a property P that holds for all p>0 with MixedCharZero(R,p) is equivalent to P holding for all prime p with MixedCharZero(R,p).
Русский
Для локальной кольца R свойство P, которое выполняется для всех p>0 при MixedCharZero(R,p), эквивалентно тому, что P выполняется для всех простых p при MixedCharZero(R,p).
LaTeX
$$$\\big(\\forall p>0,\\ MixedCharZero(R,p) \\to P\\big) \\iff \\big(\\forall p,\\text{Prime}(p) \\to MixedCharZero(R,p) \\to P\\big).$$$
Lean4
/-- Reduction to `p` prime: When proving any statement `P` about mixed characteristic rings we
can always assume that `p` is prime.
-/
theorem reduce_to_p_prime {P : Prop} : (∀ p > 0, MixedCharZero R p → P) ↔ ∀ p : ℕ, p.Prime → MixedCharZero R p → P :=
by
constructor
· intro h q q_prime q_mixedChar
exact h q (Nat.Prime.pos q_prime) q_mixedChar
· intro h q q_pos q_mixedChar
rcases q_mixedChar.charP_quotient with
⟨I, hI_ne_top, _⟩
-- Krull's Thm: There exists a prime ideal `P` such that `I ≤ P`
rcases Ideal.exists_le_maximal I hI_ne_top with ⟨M, hM_max, h_IM⟩
let r := ringChar (R ⧸ M)
have r_pos : r ≠ 0 :=
by
have q_zero := congr_arg (Ideal.Quotient.factor h_IM) (CharP.cast_eq_zero (R ⧸ I) q)
simp only [map_natCast, map_zero] at q_zero
apply ne_zero_of_dvd_ne_zero (ne_of_gt q_pos)
exact (CharP.cast_eq_zero_iff (R ⧸ M) r q).mp q_zero
have r_prime : Nat.Prime r := or_iff_not_imp_right.1 (CharP.char_is_prime_or_zero (R ⧸ M) r) r_pos
apply h r r_prime
have : CharZero R := q_mixedChar.toCharZero
exact ⟨⟨M, hM_max.ne_top, ringChar.of_eq rfl⟩⟩
