English
If c2 = 0, there is a natural algebra isomorphism swapping the first and third coefficients: ℍ[R,c1,0,c3] ≃_R ℍ[R,c3,0,c1] given by t ↦ ⟨t1, t3, t2, -t4⟩.
Русский
Если c2 = 0, существует естественное алгебраическое изоморфизм, меняющий первый и третий коэффициенты: ℍ[R,c1,0,c3] ≃_R ℍ[R,c3,0,c1] по правилу t ↦ ⟨t1, t3, t2, −t4⟩.
LaTeX
$$$\text{If } c_2 = 0,\quad \mathbb{H}(R;c_1,0,c_3) \cong_R \mathbb{H}(R;c_3,0,c_1) \text{ via } t=(t_1,t_2,t_3,t_4) \mapsto (t_1,t_3,t_2,-t_4).$$$
Lean4
/-- There is a natural equivalence when swapping the first and third coefficients of a
quaternion algebra if `c₂` is 0. -/
@[simps]
def swapEquiv : ℍ[R,c₁,0,c₃] ≃ₐ[R] ℍ[R,c₃,0,c₁]
where
toFun t := ⟨t.1, t.3, t.2, -t.4⟩
invFun t := ⟨t.1, t.3, t.2, -t.4⟩
left_inv _ := by simp
right_inv _ := by simp
map_mul' _ _ := by ext <;> simp <;> ring
map_add' _ _ := by ext <;> simp [add_comm]
commutes' _ := by simp [algebraMap_eq]
