instIsLocalHomResidueFieldRingHomResidue

English

The residue map from a local ring to its residue field admits an IsLocalHom instance, i.e., it is a local homomorphism.

Русский

Отображение остатка из локального кольца к его остаточному полю допускает свойство IsLocalHom, то есть является локальным гомоморфизмом.

LaTeX

$$$\\text{instance } IsLocalHom (\\mathrm{residue} R)$$$

Lean4

instance : IsLocalHom (IsLocalRing.residue R) :=
  ⟨fun _ ha => Classical.not_not.mp (Ideal.Quotient.eq_zero_iff_mem.not.mp (isUnit_iff_ne_zero.mp ha))⟩

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