English
There is an equivalence between the space of EvenHom Q A and the algebra homs from the even subalgebra to A, given by lifting via aux, aux_one, and aux_mul.
Русский
Существует эквивалентность между множеством EvenHom Q A и алгебра-гомоморфизмами от чётной подалгебры к A, задаваемая через aux, aux_one и aux_mul.
LaTeX
$$Equiv (EvenHom Q A) (CliffordAlgebra.even Q →ₐ[R] A)$$
Lean4
/-- The embedding of pairs of vectors into the even subalgebra, as a bilinear map. -/
nonrec def ι : EvenHom Q (even Q)
where
bilin :=
LinearMap.mk₂ R (fun m₁ m₂ => ⟨ι Q m₁ * ι Q m₂, ι_mul_ι_mem_evenOdd_zero Q _ _⟩)
(fun _ _ _ => by simp only [LinearMap.map_add, add_mul]; rfl)
(fun _ _ _ => by simp only [LinearMap.map_smul, smul_mul_assoc]; rfl)
(fun _ _ _ => by simp only [LinearMap.map_add, mul_add]; rfl) fun _ _ _ => by
simp only [LinearMap.map_smul, mul_smul_comm]; rfl
contract m := Subtype.ext <| ι_sq_scalar Q m
contract_mid m₁ m₂
m₃ :=
Subtype.ext <|
calc
ι Q m₁ * ι Q m₂ * (ι Q m₂ * ι Q m₃) = ι Q m₁ * (ι Q m₂ * ι Q m₂ * ι Q m₃) := by simp only [mul_assoc]
_ = Q m₂ • (ι Q m₁ * ι Q m₃) := by rw [Algebra.smul_def, ι_sq_scalar, Algebra.left_comm]
