English
One can define a map sending a quadratic map Isometry f between Q1 and Q2 to an algebra homomorphism Clifford(Q1) → Clifford(Q2) by lifting f via Clifford.lift.
Русский
Можно определить отображение, отправляющее изометрическое отображение f между Q1 и Q2 в алгебра-гомоморфизм Clifford(Q1) → Clifford(Q2) через подъем через Clifford.lift.
LaTeX
$$$\\mathrm{map}(f): Clifford(Q_1) \\to_ R Clifford(Q_2)$ is defined by lifting $\\iota_{Q_2} \\circ f$ via Clifford.lift.$$
Lean4
/-- Any linear map that preserves the quadratic form lifts to an `AlgHom` between algebras.
See `CliffordAlgebra.equivOfIsometry` for the case when `f` is a `QuadraticForm.IsometryEquiv`. -/
def map (f : Q₁ →qᵢ Q₂) : CliffordAlgebra Q₁ →ₐ[R] CliffordAlgebra Q₂ :=
CliffordAlgebra.lift Q₁
⟨ι Q₂ ∘ₗ f.toLinearMap, fun m => (ι_sq_scalar _ _).trans <| RingHom.congr_arg _ <| f.map_app m⟩
