injective_comp_of_perfect — Mathlib

English

If i is p-radical and M is perfect, then precomposition with i is injective.

Русский

Если i p-радикал и M совершенный, то композиция f ↦ f ∘ i инъективна.

LaTeX

$$Injective(\$ f \\mapsto f \\circ i \$)$$

Lean4

/-- If `i : K →+* L` is `p`-radical, then for any perfect ring `M` of exponential charactistic `p`,
the map `(L →+* M) → (K →+* M)` induced by `i` is injective.
A special case of `IsPRadical.injective_comp_of_pNilradical_eq_bot`. -/
theorem injective_comp_of_perfect [IsPRadical i p] [PerfectRing M p] : Function.Injective fun f : L →+* M ↦ f.comp i :=
  injective_comp_of_pNilradical_eq_bot i p (PerfectRing.pNilradical_eq_bot M p)

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