English
There is an equivalence between the category of quaternion bases on A and the algebra homomorphisms from the quaternion algebra to A, given by the lift and its inverse Basis.self ∘ liftHom.
Русский
Существует эквивалентность между базисами кватернионной алгебры на A и алгебра-гомоморфизмами из этой алгебры в A, задаваемая отображениями lift и обратной связью Basis.self ∘ liftHom.
LaTeX
$$$\\text{lift}: \\text{Basis}(A,c_1,c_2,c_3) \\simeq (\\mathbb{H}(R,c_1,c_2,c_3) \\to_{R} A)$$$
Lean4
/-- A quaternionic basis on `A` is equivalent to a map from the quaternion algebra to `A`. -/
@[simps]
def lift : Basis A c₁ c₂ c₃ ≃ (ℍ[R,c₁,c₂,c₃] →ₐ[R] A)
where
toFun := Basis.liftHom
invFun := (Basis.self R).compHom
left_inv q := by ext <;> simp [Basis.lift]
right_inv
F := by
ext
dsimp [Basis.lift]
rw [← F.commutes]
simp only [← map_smul, ← map_add, mk_add_mk, smul_mk, smul_zero, algebraMap_eq]
congr <;> simp
