comap_quotientMk_bijective_of_le_nilradical

English

For any ideal I with I ≤ nilradical(R), the comap map to Spec(R) induced by the quotient by I is bijective on prime spectra.

Русский

Для любого I ≤ нильрадикал(R) отображение comap, соответствующее факторизации по I, биективно на спектрах.

LaTeX

$$comap_quotientMk_bijective_of_le_nilradical$$

Lean4

theorem comap_quotientMk_bijective_of_le_nilradical {I : Ideal R} (hle : I ≤ nilradical R) :
    Function.Bijective (comap <| Ideal.Quotient.mk I) :=
  by
  refine ⟨comap_injective_of_surjective _ Ideal.Quotient.mk_surjective, ?_⟩
  simpa [← Set.range_eq_univ, range_comap_of_surjective _ _ Ideal.Quotient.mk_surjective, zeroLocus_eq_univ_iff]

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