English
If f is surjective, then map f of Jacobson(I) equals the Jacobson of map f I, provided the kernel condition holds.
Русский
Если отображение f сюръективно, то образ Якобиона I по f равен Якобиану образа I по f, при условии, что ядро удовлетворяет условию.
LaTeX
$$$\operatorname{map}_f I^{\mathrm{jacobson}} = (\operatorname{map}_f I)^{\mathrm{jacobson}}$$$
Lean4
theorem map_jacobson_of_surjective {f : R →+* S} (hf : Function.Surjective f) :
RingHom.ker f ≤ I → map f I.jacobson = (map f I).jacobson :=
by
intro h
unfold Ideal.jacobson
have : ∀ J ∈ {J : Ideal R | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J := fun J hJ => le_trans h hJ.left
refine Trans.trans (map_sInf hf this) (le_antisymm ?_ ?_)
· refine sInf_le_sInf fun J hJ => ⟨comap f J, ⟨⟨le_comap_of_map_le hJ.1, ?_⟩, map_comap_of_surjective f hf J⟩⟩
haveI : J.IsMaximal := hJ.right
exact comap_isMaximal_of_surjective f hf
· refine sInf_le_sInf_of_subset_insert_top fun j hj => hj.recOn fun J hJ => ?_
rw [← hJ.2]
rcases map_eq_top_or_isMaximal_of_surjective f hf hJ.left.right with htop | hmax
· exact htop.symm ▸ Set.mem_insert ⊤ _
· exact Set.mem_insert_of_mem ⊤ ⟨map_mono hJ.1.1, hmax⟩
