ker_Pi_Quotient_mk — Mathlib

English

The kernel of the Pi‑ring homomorphism that maps each i to the quotient by I_i equals the infimum of all I_i.

Русский

Ядро биективного отображения Pi, отправляющего каждую координату в фактор‑картину по I_i, равно пересечению всех I_i.

LaTeX

$$$\ker\big(\Pi\text{-ringHom } i \mapsto \operatorname{Quotient.mk}(I_i)\big) = \bigcap_i I_i$$$

Lean4

theorem ker_Pi_Quotient_mk {ι : Type*} (I : ι → Ideal R) [∀ i, (I i).IsTwoSided] :
    ker (Pi.ringHom fun i : ι ↦ Quotient.mk (I i)) = ⨅ i, I i := by simp [Pi.ker_ringHom, mk_ker]

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