snd_comp_quotientMulEquivQuotientProd

English

With the same setup as the previous statement, the second projection π2: (R/I) × (R/J) → R/J composed with φ equals the canonical quotient ψJ: R/(IJ) → R/J.

Русский

При той же постановке, вторая проекция π2: (R/I) × (R/J) → R/J, составленная с φ, равна естественному отображению ψJ: R/(IJ) → R/J.

LaTeX

$$$ \pi_2 \circ \varphi_{I,J} = \psi_J $,$$

Lean4

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

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