English
The reverse and involute maps preserve the even-to-Euclidean structure, ensuring compatibility of conjugations with the embedding.
Русский
Обратная и инволюционная карты сохраняют структуру вложения, обеспечивая совместимость конъюгирования с вложением.
LaTeX
$$Compatibility conditions for reverse and involute with the even embedding$$
Lean4
/-- The embedding from the even subalgebra with an extra dimension into the original algebra. -/
def ofEven : CliffordAlgebra.even (Q' Q) →ₐ[R] CliffordAlgebra Q := by
/-
Recall that we need:
* `f ⟨0,1⟩ ⟨x,0⟩ = ι x`
* `f ⟨x,0⟩ ⟨0,1⟩ = -ι x`
* `f ⟨x,0⟩ ⟨y,0⟩ = ι x * ι y`
* `f ⟨0,1⟩ ⟨0,1⟩ = -1`
-/
let f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
((Algebra.lmul R (CliffordAlgebra Q)).toLinearMap.comp <|
(ι Q).comp (LinearMap.fst _ _ _) + (Algebra.linearMap R _).comp (LinearMap.snd _ _ _)).compl₂
((ι Q).comp (LinearMap.fst _ _ _) - (Algebra.linearMap R _).comp (LinearMap.snd _ _ _))
haveI f_apply : ∀ x y, f x y = (ι Q x.1 + algebraMap R _ x.2) * (ι Q y.1 - algebraMap R _ y.2) := fun x y => by rfl
haveI hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute (algebraMap _ _ r) x := Algebra.commutes
haveI hm : ∀ m : M × R, ι Q m.1 * ι Q m.1 - algebraMap R _ m.2 * algebraMap R _ m.2 = algebraMap R _ (Q' Q m) :=
by
intro m
rw [ι_sq_scalar, ← RingHom.map_mul, ← RingHom.map_sub, sub_eq_add_neg, Q'_apply, sub_eq_add_neg]
refine even.lift (Q' Q) ⟨f, ?_, ?_⟩ <;> simp_rw [f_apply]
· intro m
rw [← (hc _ _).symm.mul_self_sub_mul_self_eq, hm]
· intro m₁ m₂ m₃
rw [← mul_smul_comm, ← mul_assoc, mul_assoc (_ + _), ← (hc _ _).symm.mul_self_sub_mul_self_eq', Algebra.smul_def, ←
mul_assoc, hm]
