Theorems · Theorem · field theory

IsPRadical.injective_comp_of_perfect

∀ {K : Type u_1} {L : Type u_2} (M : Type u_3) [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (p : ℕ) [ExpChar M p] [IsPRadical i p] [PerfectRing M p], Function.Injective fun f => f.comp i

If i : K →+* L is p-radical, then for any perfect ring M of exponential characteristic p, the map (L →+* M) → (K →+* M) induced by i is injective. A special case of IsPRadical.injective_comp_of_pNilradical_eq_bot.

Defined in

Mathlib.FieldTheory.IsPerfectClosure

Cited by

3 results in Mathlib

Foundations

Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingCommRingExpCharIsPRadicalPerfectRing