English
Auxiliary contraction operator contractLeftAux(d) is a linear map assigning to each vector m ∈ M a linear map from Clifford(Q) × Clifford(Q) to Clifford(Q), defined using the dual d and the canonical embedding ι_Q, together with left Clifford multiplication.
Русский
Вводимое вспомогательное оператор свёртывания contractLeftAux(d) является линейным отображением, которому каждому вектору m ∈ M ставится в соответствие линейный отображение из Clifford(Q) × Clifford(Q) в Clifford(Q); оно определяется через дуальное приложение d и каноническое вложение ι_Q, с учётом левого умножения Клиффорда.
LaTeX
$$$ contractLeftAux(d) : M \\to ( Clifford(Q) \\times Clifford(Q) \\to Clifford(Q) ), \\quad contractLeftAux(d)(m) = d(m) \\cdot \\mathrm{fst} - v_{\\mathrm{mul}} \\circ \\mathrm{snd} $$$
Lean4
/-- Auxiliary construction for `CliffordAlgebra.contractLeft` -/
@[simps!]
def contractLeftAux (d : Module.Dual R M) : M →ₗ[R] CliffordAlgebra Q × CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q :=
haveI v_mul := (Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ ι Q
d.smulRight (LinearMap.fst _ (CliffordAlgebra Q) (CliffordAlgebra Q)) -
v_mul.compl₂ (LinearMap.snd _ (CliffordAlgebra Q) _)
