eq_set_map_one_map_mul — Mathlib

English

The character space equals the set of multiplicative linear functionals φ : A → 𝕜 such that φ(1)=1 and φ(xy)=φ(x)φ(y) for all x,y ∈ A.

Русский

Множество характеристических отображений равно множеству линейных функционалов φ: A → 𝕜, удовлетворяющих φ(1)=1 и φ(xy)=φ(x)φ(y) для всех x,y ∈ A.

LaTeX

$$$\mathrm{Char}_{\mathbb{k}}(A) = \{ \phi: A \to \mathbb{k} \mid \phi(1)=1 \ \&\ \forall x,y\in A:\ \phi(xy)=\phi(x)\phi(y) \}$$$

Lean4

theorem eq_set_map_one_map_mul [Nontrivial 𝕜] :
    characterSpace 𝕜 A = {φ : WeakDual 𝕜 A | φ 1 = 1 ∧ ∀ x y : A, φ (x * y) = φ x * φ y} :=
  by
  ext φ
  refine ⟨?_, ?_⟩
  · rintro hφ
    lift φ to characterSpace 𝕜 A using hφ
    exact ⟨map_one φ, map_mul φ⟩
  · rintro ⟨hφ₁, hφ₂⟩
    refine ⟨?_, hφ₂⟩
    rintro rfl
    exact zero_ne_one hφ₁

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