English
For a basis q and an algebra hom F : A → B, the induced basis on B has its structure maps determined by the images F(i), F(j), F(k).
Русский
Для данного базиса q и алгебра-гомоморфизма F : A → B структура базиса на B определяется изображениями F(i), F(j), F(k).
LaTeX
$$$\\text{compHom}(F) : \\text{Basis } B c_1 c_2 c_3 \\;\\text{где } i := F(q.i),\\; j := F(q.j),\\; k := F(q.k)$$$
Lean4
/-- Transform a `QuaternionAlgebra.Basis` through an `AlgHom`. -/
@[simps i j k]
def compHom (F : A →ₐ[R] B) : Basis B c₁ c₂ c₃ where
i := F q.i
i_mul_i := by rw [← map_mul, q.i_mul_i, map_add, map_smul, map_smul, map_one]
j := F q.j
j_mul_j := by rw [← map_mul, q.j_mul_j, map_smul, map_one]
k := F q.k
i_mul_j := by rw [← map_mul, q.i_mul_j]
j_mul_i := by rw [← map_mul, q.j_mul_i, map_sub, map_smul]
