fst_comp_quotientMulEquivQuotientProd

English

Let R be a ring and I, J ideals with I and J coprime. Consider the canonical map φ: R/(IJ) → (R/I) × (R/J) and the first projection π1: (R/I) × (R/J) → R/I. Then π1 ∘ φ equals the natural quotient map ψI: R/(IJ) → R/I.

Русский

Пусть R — кольцо, I и J — идеалы, взаимно простые. Рассмотрим каноническое отображение φ: R/(IJ) → (R/I) × (R/J) и первую проекцию π1: (R/I) × (R/J) → R/I. Тогда π1 ∘ φ совпадает с естественным отображением ψI: R/(IJ) → R/I.

LaTeX

$$$ \pi_1 \circ \varphi_{I,J} = \psi_I $,$$

Lean4

@[simp]
theorem fst_comp_quotientMulEquivQuotientProd (I J : Ideal R) (coprime : IsCoprime I J) :
    (RingHom.fst _ _).comp (quotientMulEquivQuotientProd I J coprime : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J) =
      Ideal.Quotient.factor mul_le_right :=
  by apply Quotient.ringHom_ext; ext; rfl

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