English
In the enlarged Clifford algebra, the image of (m,r) under ι decomposes as v(m) + r·e0.
Русский
Образ (m,r) через ι в расширенной клиффордовой алгебре разлагается как v(m) + r·e0.
LaTeX
$$$\iota(Q' Q)(m,r) = v(Q)m + r \cdot e_0(Q)$$$
Lean4
/-- The embedding from the smaller algebra into the new larger one. -/
def toEven : CliffordAlgebra Q →ₐ[R] CliffordAlgebra.even (Q' Q) :=
by
refine CliffordAlgebra.lift Q ⟨?_, fun m => ?_⟩
· refine LinearMap.codRestrict _ ?_ fun m => Submodule.mem_iSup_of_mem ⟨2, rfl⟩ ?_
· exact (LinearMap.mulLeft R <| e0 Q).comp (v Q)
rw [Subtype.coe_mk, pow_two]
exact Submodule.mul_mem_mul (LinearMap.mem_range_self _ _) (LinearMap.mem_range_self _ _)
· ext1
rw [Subalgebra.coe_mul] -- Porting note: was part of the `dsimp only` below
erw [LinearMap.codRestrict_apply] -- Porting note: was part of the `dsimp only` below
dsimp only [LinearMap.comp_apply, LinearMap.mulLeft_apply, Subalgebra.coe_algebraMap]
rw [← mul_assoc, e0_mul_v_mul_e0, v_sq_scalar]
