English
For IsPRadical i, pNilradical L p comapped along i equals pNilradical K p: (pNilradical L p).comap i = pNilradical K p.
Русский
Если i удовлетворяет IsPRadical, то pNilradical L p сопряжено по i равно pNilradical K p.
LaTeX
$$$$ (pNilradical\\ L\\ p).comap\\ i = pNilradical\\ K\\ p. $$$$
Lean4
theorem comap_pNilradical [IsPRadical i p] : (pNilradical L p).comap i = pNilradical K p :=
by
refine le_antisymm (fun x h ↦ mem_pNilradical.2 ?_) (fun x h ↦ ?_)
· obtain ⟨n, h⟩ := mem_pNilradical.1 <| Ideal.mem_comap.1 h
obtain ⟨m, h⟩ := mem_pNilradical.1 <| ker_le i p ((map_pow i x _).symm ▸ h)
exact ⟨n + m, by rwa [pow_add, pow_mul]⟩
simp only [Ideal.mem_comap, mem_pNilradical] at h ⊢
obtain ⟨n, h⟩ := h
exact ⟨n, by simpa only [map_pow, map_zero] using congr(i $h)⟩
