English
If the multiplication map mul 𝕜 A is injective, then the splitMul 𝕜 A map is injective.
Русский
Если отображение умножения mul 𝕜 A инъективно, то и отображение splitMul 𝕜 A инъективно.
LaTeX
$$$$\\text{Injective}(\\,splitMul\\ 𝕜 A\\,)\\Leftarrow\\text{Injective}(\\,mul\\ 𝕜 A\\!).$$$$
Lean4
/-- this lemma establishes that if `ContinuousLinearMap.mul 𝕜 A` is injective, then so is
`Unitization.splitMul 𝕜 A`. When `A` is a `RegularNormedAlgebra`, then
`ContinuousLinearMap.mul 𝕜 A` is an isometry, and is therefore automatically injective. -/
theorem splitMul_injective_of_clm_mul_injective (h : Function.Injective (mul 𝕜 A)) :
Function.Injective (splitMul 𝕜 A) := by
rw [injective_iff_map_eq_zero]
intro x hx
induction x
rw [map_add] at hx
simp only [splitMul_apply, fst_inl, snd_inl, map_zero, add_zero, fst_inr, snd_inr, zero_add, Prod.mk_add_mk,
Prod.mk_eq_zero] at hx
obtain ⟨rfl, hx⟩ := hx
simp only [map_zero, zero_add, inl_zero] at hx ⊢
rw [← map_zero (mul 𝕜 A)] at hx
rw [h hx, inr_zero]
