pNilradical_le_ker_of_perfectRing

English

If i: K →* L has ExpChar L p and L is a PerfectRing of p, then the p-nilradical of K maps into ker i.

Русский

Если i: K →* L имеет ExpChar L p и L —PerfectRing p, то p-нилрадикал K вложен в ядро i.

LaTeX

$$$pNilradical(K,p) \\leq \\ker(i)$$$

Lean4

/-- If `i : K →+* L` is a ring homomorphism of exponential characteristic `p` rings, such that `L`
is perfect, then the `p`-nilradical of `K` is contained in the kernel of `i`. -/
theorem pNilradical_le_ker_of_perfectRing [ExpChar L p] [PerfectRing L p] : pNilradical K p ≤ RingHom.ker i := fun x h ↦
  by
  obtain ⟨n, h⟩ := mem_pNilradical.1 h
  replace h := congr((iterateFrobeniusEquiv L p n).symm (i $h))
  rwa [map_pow, ← iterateFrobenius_def, ← iterateFrobeniusEquiv_apply, RingEquiv.symm_apply_apply, map_zero,
    map_zero] at h

Похожие утверждения