English
The even subalgebras corresponding to Q and to −Q are canonically isomorphic as R-algebras. This isomorphism is constructed by mapping generators in the Q-case to their negated counterparts in the −Q-case.
Русский
Четные подполя, соответствующие Q и −Q, канонически изоморфны как R-алгебры. Этот изоморфизм строится сопоставлением порождающих в случае Q с их отрицательными аналогами в случае −Q.
LaTeX
$$$ \\mathrm{even}(Q) \\cong_R \\mathrm{even}(-Q) $$$
Lean4
theorem ofEven_comp_toEven : (ofEven Q).comp (toEven Q) = AlgHom.id R _ :=
CliffordAlgebra.hom_ext <|
LinearMap.ext fun m =>
calc
ofEven Q (toEven Q (ι Q m)) = ofEven Q ⟨_, (toEven Q (ι Q m)).prop⟩ := by rw [Subtype.coe_eta]
_ = (ι Q 0 + algebraMap R _ 1) * (ι Q m - algebraMap R _ 0) :=
by
simp_rw [toEven_ι]
exact ofEven_ι Q _ _
_ = ι Q m := by rw [map_one, map_zero, map_zero, sub_zero, zero_add, one_mul]
