English
Let R be a commutative ring and I an ideal. Then CharP (R/I) n holds if and only if the comap of I along the natural cast map is contained in the kernel of the natural cast map.
Русский
Пусть R — коммутативное кольцо и I — идеал. Тогда CharP (R/I) n выполняется тогда и только тогда, когда обратимая загрузка I вдоль естественного отображения natCast содержится в ядре этого отображения.
LaTeX
$$$\\mathrm{CharP}(R/I)\\; n \\iff I.\\mathrm{comap}(\\mathrm{Nat.castR}) \\le \\mathrm{ker}(\\mathrm{Nat.castR})$$$
Lean4
/-- `CharP.quotient_iff`, but stated in terms of inclusions of ideals. -/
theorem quotient_iff_le_ker_natCast {R : Type*} [CommRing R] (n : ℕ) [CharP R n] (I : Ideal R) :
CharP (R ⧸ I) n ↔ I.comap (Nat.castRingHom R) ≤ RingHom.ker (Nat.castRingHom R) := by
rw [CharP.quotient_iff, RingHom.ker_eq_comap_bot]; rfl
