English
There is a canonical A-algebra isomorphism (an algebra equivalence) between the base-changed Clifford algebra and the Clifford algebra of the base-changed quadratic form: Cℓ_A(Q) ≃_A A ⊗_R Cℓ(Q).
Русский
Существует каноническое A-алгебро-эквивалентное отображение между CliffordAlgebra(Q.baseChange A) и A ⊗_R CliffordAlgebra(Q): Cℓ_A(Q) ≃_A A ⊗ Cℓ(Q).
LaTeX
$$$\mathrm{Cℓ}(Q.baseChange A) \cong_A A \otimes_R \mathrm{Cℓ}(Q)$$$
Lean4
/-- Convert from the clifford algebra over a base-changed module to the base-changed clifford
algebra. -/
def toBaseChange (Q : QuadraticForm R V) : CliffordAlgebra (Q.baseChange A) →ₐ[A] A ⊗[R] CliffordAlgebra Q :=
CliffordAlgebra.lift _ <|
by
refine ⟨TensorProduct.AlgebraTensorModule.map (LinearMap.id : A →ₗ[A] A) (ι Q), ?_⟩
letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm
letI : Invertible (2 : A ⊗[R] CliffordAlgebra Q) := (Invertible.map (algebraMap R _) 2).copy 2 (map_ofNat _ _).symm
suffices hpure_tensor :
∀ v w,
(1 * 1) ⊗ₜ[R] (ι Q v * ι Q w) + (1 * 1) ⊗ₜ[R] (ι Q w * ι Q v) =
QuadraticMap.polarBilin (Q.baseChange A) (1 ⊗ₜ[R] v) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1
by
-- the crux is that by converting to a statement about linear maps instead of quadratic forms,
-- we then have access to all the partially-applied `ext` lemmas.
rw [CliffordAlgebra.forall_mul_self_eq_iff (isUnit_of_invertible _)]
refine TensorProduct.AlgebraTensorModule.curry_injective ?_
ext v w
dsimp
exact hpure_tensor v w
intro v w
rw [← TensorProduct.tmul_add, CliffordAlgebra.ι_mul_ι_add_swap, QuadraticForm.polarBilin_baseChange,
LinearMap.BilinForm.baseChange_tmul, one_mul, TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one,
QuadraticMap.polarBilin_apply_apply]
