ker_toSpanSingleton_eq_span — Mathlib

English

For an idempotent element e in a commutative ring, the kernel of the map a ↦ a e equals the ideal generated by (1 − e).

Русский

Для идемпотентного элемента e в коммутативном кольце ядро отображения a ↦ a e равно идеалу, порожденному (1 − e).

LaTeX

$$$$ \ker(\text{toSpanSingleton}(R,R,e)) = \operatorname{span}\{1 - e\} $$$$

Lean4

theorem ker_toSpanSingleton_eq_span : LinearMap.ker (LinearMap.toSpanSingleton R R e) = Ideal.span {1 - e} :=
  SetLike.ext fun x ↦ by
    rw [Ideal.mem_span_singleton']
    refine ⟨fun h ↦ ⟨x, by rw [mul_sub, show x * e = 0 from h, mul_one, sub_zero]⟩, fun h ↦ ?_⟩
    obtain ⟨x, rfl⟩ := h
    change x * (1 - e) * e = 0
    rw [mul_assoc, sub_mul, one_mul, he, sub_self, mul_zero]

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