English
The canonical embedding r ↦ single 1 r from R into MonoidAlgebra R M is a local hom, i.e., if its image is a nonunit, then r itself is a nonunit in R.
Русский
Каноническое вложение r ↦ single 1 r из R в MonoidAlgebra R M является локальным гомом, то есть если образ элемента r не является единицей, то сам r не является единицей в R.
LaTeX
$$$\\forall r \\in R,\\ \\neg \\mathrm{IsUnit}(\\mathrm{single}\\, 1\\, r) \\\\Rightarrow \\neg \\mathrm{IsUnit}(r).$$$
Lean4
@[to_additive (dont_translate := R)]
instance isLocalHom_singleOneRingHom : IsLocalHom (singleOneRingHom (R := R) (M := M)) where
map_nonunit x
hx := by
obtain ⟨⟨x, xi, hx, hxi⟩, rfl⟩ := hx
simp_rw [MonoidAlgebra.ext_iff, singleOneRingHom_apply] at hx hxi ⊢
specialize hx 1
specialize hxi 1
classical
simp_rw [single_one_mul_apply, one_def, single_apply, if_pos] at hx
simp_rw [mul_single_one_apply, one_def, single_apply, if_pos] at hxi
exact ⟨⟨x, xi 1, hx, hxi⟩, rfl⟩
