English
Same as above: the union is closed under the same hypotheses.
Русский
То же самое: объединение замкнуто при тех же предпосылках.
LaTeX
$$$IsClosed (characterSpace 𝕜 A \\cup \\{0\\})$$$
Lean4
/-- In a unital algebra, elements of the character space are algebra homomorphisms. -/
instance instAlgHomClass : AlgHomClass (characterSpace 𝕜 A) 𝕜 A 𝕜 :=
haveI map_one' : ∀ φ : characterSpace 𝕜 A, φ 1 = 1 := fun φ =>
by
have h₁ : φ 1 * (1 - φ 1) = 0 := by rw [mul_sub, sub_eq_zero, mul_one, ← map_mul φ, one_mul]
rcases mul_eq_zero.mp h₁ with (h₂ | h₂)
· have : ∀ a, φ (a * 1) = 0 := fun a => by simp only [map_mul φ, h₂, mul_zero]
exact False.elim (φ.prop.1 <| ContinuousLinearMap.ext <| by simpa only [mul_one] using this)
· exact (sub_eq_zero.mp h₂).symm
{ CharacterSpace.instNonUnitalAlgHomClass with
map_one := map_one'
commutes := fun φ r =>
by
rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_self, RingHom.id_apply]
rw [map_smul, Algebra.id.smul_eq_mul, map_one' φ, mul_one] }
