English
The map w ↦ char he hL w defines a monoid homomorphism from Multiplicative W to the bounded continuous functions V → ℂ, sending 1 to the constant function 1 and respecting multiplication.
Русский
Отображение w ↦ char(he,hL,w) задаёт гомоморфизм моноидов от (W,·) к (V →ᵇ ℂ), отображение единицы идёт в константную единицу, и сохраняет произведение.
LaTeX
$$$\\text{charMonoidHom}(he,hL) : \\operatorname{Multiplicative} W \\to_* (V \\to_b \\mathbb{C}),\\quad w \\mapsto (v \\mapsto e(L(v,w)));\\quad \\text{map_one'}\\equiv \\text{char\_zero\_eq\_one},\\quad \\text{map\_mul'}\\equiv \\text{char\_add\_eq\_mul}.$$$
Lean4
/-- If `e` and `L` are non-trivial, then `char he hL w, w : W` separates points in `V`. -/
theorem ext_of_char_eq (he : Continuous e) (he' : e ≠ 1) (hL : Continuous fun p : V × W ↦ L p.1 p.2)
(hL' : ∀ v ≠ 0, L v ≠ 0) {v v' : V} (h : ∀ w, char he hL w v = char he hL w v') : v = v' :=
by
contrapose! h
obtain ⟨w, hw⟩ := DFunLike.ne_iff.mp (hL' (v - v') (sub_ne_zero_of_ne h))
obtain ⟨a, ha⟩ := DFunLike.ne_iff.mp he'
use (a / (L (v - v') w)) • w
simp only [map_sub, LinearMap.sub_apply, char_apply, ne_eq]
rw [← div_eq_one_iff_eq (Circle.coe_ne_zero _), div_eq_inv_mul, ← Metric.unitSphere.coe_inv, ← e.map_neg_eq_inv, ←
Submonoid.coe_mul, ← e.map_add_eq_mul, OneMemClass.coe_eq_one]
calc
e (-L v' ((a / (L v w - L v' w)) • w) + L v ((a / (L v w - L v' w)) • w))
_ = e (-(a / (L v w - L v' w)) • L v' w + (a / (L v w - L v' w)) • L v w) :=
by
congr
· rw [neg_smul, ← LinearMap.map_smul (L v')]
· rw [← LinearMap.map_smul (L v)]
_ = e ((a / (L (v - v') w)) • (L (v - v') w)) :=
by
simp only [map_sub, LinearMap.sub_apply]
congr
module
_ = e a := by
congr
exact div_mul_cancel₀ a hw
_ ≠ 1 := ha
