isLocalHom_residue — Mathlib

English

The canonical residue map IsLocalRing.residue R is a local homomorphism: it preserves local structure when passing to the residue field.

Русский

Каноническое отображение резидуального поля IsLocalRing.residue R является локальным гомоморфизмом: сохраняет локальную структуру в поле остатка.

LaTeX

$$IsLocalRing.isLocalHom_residue$$

Lean4

theorem isLocalHom_residue : IsLocalHom (IsLocalRing.residue R) :=
  by
  constructor
  intro a ha
  by_contra h
  rw [residue_def, Ideal.Quotient.eq_zero_iff_mem.mpr ((IsLocalRing.mem_maximalIdeal _).mpr h)] at ha
  exact ha.ne_zero rfl

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