English
A consequence of contractLeftAux_contractLeftAux is the core identity relating left contraction on a triple (v, x, fx) to Q(v) times fx.
Русский
Следствием contractLeftAux_contractLeftAux является основное тождество, связывающее левое свёртывание на тройке (v, x, fx) с произведением \(Q(v)\) на fx.
LaTeX
$$$ contractLeftAux\\_contractLeftAux(Q, d)(v, x, f_x) = Q(v) \\cdot f_x $$$
Lean4
/-- Contract an element of the clifford algebra with an element `d : Module.Dual R M` from the left.
Note that $v ⌋ x$ is spelt `contractLeft (Q.associated v) x`.
This includes [grinberg_clifford_2016][] Theorem 10.75 -/
def contractLeft : Module.Dual R M →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q
where
toFun d := foldr' Q (contractLeftAux Q d) (contractLeftAux_contractLeftAux Q d) 0
map_add' d₁
d₂ :=
LinearMap.ext fun x => by
rw [LinearMap.add_apply]
induction x using CliffordAlgebra.left_induction with
| algebraMap => simp_rw [foldr'_algebraMap, smul_zero, zero_add]
| add _ _ hx hy => rw [map_add, map_add, map_add, add_add_add_comm, hx, hy]
| ι_mul _ _ hx =>
rw [foldr'_ι_mul, foldr'_ι_mul, foldr'_ι_mul, hx]
dsimp only [contractLeftAux_apply_apply]
rw [sub_add_sub_comm, mul_add, LinearMap.add_apply, add_smul]
map_smul' c
d :=
LinearMap.ext fun x => by
rw [LinearMap.smul_apply, RingHom.id_apply]
induction x using CliffordAlgebra.left_induction with
| algebraMap => simp_rw [foldr'_algebraMap, smul_zero]
| add _ _ hx hy => rw [map_add, map_add, smul_add, hx, hy]
| ι_mul _ _ hx =>
rw [foldr'_ι_mul, foldr'_ι_mul, hx]
dsimp only [contractLeftAux_apply_apply]
rw [LinearMap.smul_apply, smul_assoc, mul_smul_comm, smul_sub]
