localRingHom_comp — Mathlib

English

The composition of localRingHoms equals the corresponding localRingHom of a composed map.

Русский

Состав локальных гомоморфизмов равен локальному гомоморфизму от композиции функций.

LaTeX

$$$\mathrm{localRingHom}\ I K (\,g.\!\text{comp } f) = (\mathrm{localRingHom}\ J K g) \circ (\mathrm{localRingHom}\ I J f).$$$

Lean4

theorem localRingHom_comp {S : Type*} [CommSemiring S] (J : Ideal S) [hJ : J.IsPrime] (K : Ideal P) [hK : K.IsPrime]
    (f : R →+* S) (hIJ : I = J.comap f) (g : S →+* P) (hJK : J = K.comap g) :
    localRingHom I K (g.comp f) (by rw [hIJ, hJK, Ideal.comap_comap f g]) =
      (localRingHom J K g hJK).comp (localRingHom I J f hIJ) :=
  localRingHom_unique _ _ _ _ fun r => by simp only [Function.comp_apply, RingHom.coe_comp, localRingHom_to_map]

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