English
Let f1 and f2 be isometries from quadratic forms Q1 and Q2 into Qn, and assume that for all x in M1 and y in M2 the images f1(x) and f2(y) are orthogonal in Qn. If m1 and m2 lie in the odd part (degree 1) of their respective Clifford algebras, then the images map f1(m1) and map f2(m2) anticommute in the target Clifford algebra; i.e., map f1(m1) map f2(m2) = - map f2(m2) map f1(m1).
Русский
Пусть f1, f2 — изометрии квадратичных форм Q1, Q2 в Qn, и полагаем hf: ∀x∈M1, ∀y∈M2, Qn.IsOrho (f1 x) (f2 y). Для m1, m2 из соответствующих Clifford-алгебр в подпространствах нечетной степени (1), произведения их образов в целевой Clifford-алгебре антикоммутируют:
LaTeX
$$$$\\forall R \\ M_1 \\ M_2 \\ N \\ [\\text{CommRing } R] \\, [\\text{AddCommGroup } M_1] [\\text{AddCommGroup } M_2] [\\text{AddCommGroup } N] \\\\ [\\text{Module } R M_1] [\\text{Module } R M_2] [\\text{Module } R N] \\\\ {Q_1 : QuadraticForm R M_1} {Q_2 : QuadraticForm R M_2} {Q_n : QuadraticForm R N} \\\\ (f_1 : Q_1 \\to q_i Q_n) (f_2 : Q_2 \\to q_i Q_n) (hf : \\forall x y, Q_n.IsOrtho (f_1 x) (f_2 y)) \\\\ (m_1 : CliffordAlgebra Q_1) (m_2 : CliffordAlgebra Q_2) \\left(n_1 : m_1 \\in evenOdd Q_1 1\\right) \\left(n_2 : m_2 \\in evenOdd Q_2 1\\right) \\\\ =>\\ map f_1 m_1 \\cdot map f_2 m_2 = - map f_2 m_2 \\cdot map f_1 m_1 $$$$
Lean4
theorem map_mul_map_eq_neg_of_isOrtho_of_mem_evenOdd_one (hm₁ : m₁ ∈ evenOdd Q₁ 1) (hm₂ : m₂ ∈ evenOdd Q₂ 1) :
map f₁ m₁ * map f₂ m₂ = -map f₂ m₂ * map f₁ m₁ := by simp [map_mul_map_of_isOrtho_of_mem_evenOdd _ _ hf _ _ hm₁ hm₂]
