English
Given a quadratic form Q on a, and an R-algebra A with an invertible 2, there exists an auxiliary R-algebra homomorphism from the Clifford algebra of Q to the Clifford algebra of the base-changed form Q.baseChange(A). This homomorphism sends the generator ι_Q(v) to ι_{Q.baseChange A}(1 ⊗ v) and encodes the base-change at the level of generators.
Русский
При заданной квадратичной форме Q и базовом изменении через алгебру A, существует вспомогательное идело-отображение из CliffordAlgebra(Q) в CliffordAlgebra(Q.baseChange A), которое переводит генератор ι_Q(v) в ι_{Q.baseChange A}(1 ⊗ v).
LaTeX
$$$\exists φ : CliffordAlgebra(Q) \to_{R} CliffordAlgebra(Q.baseChange A) \,\text{ such that } φ(ι_Q(v)) = ι_{Q.baseChange A}(1 \otimes v)$$$
Lean4
/-- Auxiliary construction: note this is really just a heterobasic `CliffordAlgebra.map`. -/
def ofBaseChangeAux (Q : QuadraticForm R V) : CliffordAlgebra Q →ₐ[R] CliffordAlgebra (Q.baseChange A) :=
CliffordAlgebra.lift Q <|
by
refine ⟨(ι (Q.baseChange A)).restrictScalars R ∘ₗ TensorProduct.mk R A V 1, fun v => ?_⟩
refine (CliffordAlgebra.ι_sq_scalar (Q.baseChange A) (1 ⊗ₜ v)).trans ?_
rw [QuadraticForm.baseChange_tmul, one_mul, ← Algebra.algebraMap_eq_smul_one, ← IsScalarTower.algebraMap_apply]
