English
If i is p-radical and M is reduced, then the map sending f to f ∘ i is injective on L →* M.
Русский
Если i p-радикал и M редуктивен, то отображение f ↦ f ∘ i на множестве гомоморфизмов L →* M инъективно.
LaTeX
$$Function.Injective (\\, f \\mapsto f ∘ i\\,)$$
Lean4
/-- If `i : K →+* L` is `p`-radical, then for any reduced 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`
and a generalization of `IsPurelyInseparable.injective_comp_algebraMap`. -/
theorem injective_comp [IsPRadical i p] [IsReduced M] : Function.Injective fun f : L →+* M ↦ f.comp i :=
injective_comp_of_pNilradical_eq_bot i p <| bot_unique <| pNilradical_le_nilradical.trans (nilradical_eq_zero M).le
