range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk

English

Equality of ranges for comaps after localization and quotient maps with respect to span{c} holds in Prime Spectrum context.

Русский

Согласованность образов отображений через локализацию и фактор-множество относительно span{c} в контексте Prime Spectrum.

LaTeX

$$$\\text{range}(\\text{comap}(\\text{algebraMap } R[X] (Away c)[X]))^c = \\text{range}(\\text{comap}(\\text{mapRingHom}(\\text{Ideal.Quotient.mk}(\\text{span}(\\{c\\}))))).$$$

Lean4

theorem range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk {R : Type*} [CommRing R] (c : R) :
    letI := (mapRingHom (algebraMap R (Away c))).toAlgebra
    (range (comap (algebraMap R[X] (Away c)[X])))ᶜ = range (comap (mapRingHom (Ideal.Quotient.mk (.span { c })))) :=
  by
  letI := (mapRingHom (algebraMap R (Away c))).toAlgebra
  have := Polynomial.isLocalization (.powers c) (Away c)
  rw [Submonoid.map_powers] at this
  have surj : Function.Surjective (mapRingHom (Ideal.Quotient.mk (.span { c }))) :=
    Polynomial.map_surjective _ Ideal.Quotient.mk_surjective
  rw [range_comap_of_surjective _ _ surj, localization_away_comap_range _ (C c)]
  simp [Polynomial.ker_mapRingHom, Ideal.map_span]

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