ext_ker — Mathlib

English

If two characters φ and ψ have the same kernel, then they are equal: ker φ = ker ψ implies φ = ψ.

Русский

Если ядра двух характеристических отображений совпадают, то сами отображения совпадают: ker φ = ker ψ ⇒ φ = ψ.

LaTeX

$$$\forall \phi,\psi:\, \ker\phi = \ker\psi \Rightarrow \phi = \psi.$$$

Lean4

theorem ext_ker {φ ψ : characterSpace 𝕜 A} (h : RingHom.ker φ = RingHom.ker ψ) : φ = ψ :=
  by
  ext x
  have : x - algebraMap 𝕜 A (ψ x) ∈ RingHom.ker φ := by
    simpa only [h, RingHom.mem_ker, map_sub, AlgHomClass.commutes] using sub_self (ψ x)
  rwa [RingHom.mem_ker, map_sub, AlgHomClass.commutes, sub_eq_zero] at this

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