English
There is an induction principle stating that any property C of Clifford(Q) that holds for the base algebra map, for all iota_Q x, is closed under addition and multiplication and thus holds for all elements of Clifford(Q).
Русский
Существует принцип индукции для Clifford(Q): если C верна для алгебра-отображения и для каждого iota_Q x, и C сохраняется при сложении и умножении, то C верна для всех элементов Clifford(Q).
LaTeX
$$@[elab_as_elim] induction principle for CliffordAlgebra: If algebraMap, ι, mul and add preserve C, then C holds for all a ∈ CliffordAlgebra Q.$$
Lean4
/-- If `C` holds for the `algebraMap` of `r : R` into `CliffordAlgebra Q`, the `ι` of `x : M`,
and is preserved under addition and multiplication, then it holds for all of `CliffordAlgebra Q`.
See also the stronger `CliffordAlgebra.left_induction` and `CliffordAlgebra.right_induction`.
-/
@[elab_as_elim]
theorem induction {C : CliffordAlgebra Q → Prop} (algebraMap : ∀ r, C (algebraMap R (CliffordAlgebra Q) r))
(ι : ∀ x, C (ι Q x)) (mul : ∀ a b, C a → C b → C (a * b)) (add : ∀ a b, C a → C b → C (a + b))
(a : CliffordAlgebra Q) : C a := by
-- the arguments are enough to construct a subalgebra, and a mapping into it from M
let s : Subalgebra R (CliffordAlgebra Q) :=
{ carrier := C
mul_mem' := @mul
add_mem' := @add
algebraMap_mem' := algebraMap }
let of : { f : M →ₗ[R] s // ∀ m, f m * f m = _root_.algebraMap _ _ (Q m) } :=
⟨(CliffordAlgebra.ι Q).codRestrict (Subalgebra.toSubmodule s) ι, fun m => Subtype.eq <| ι_sq_scalar Q m⟩
-- the mapping through the subalgebra is the identity
have of_id : s.val.comp (lift Q of) = AlgHom.id R (CliffordAlgebra Q) :=
by
ext x
simpa [of, -LinearMap.codRestrict_apply]
-- This `@[simp]` lemma applies to `coeSort s.subModule`, but the goal contains
-- a plain `coeSort s`. So we remove it from the `simp` arguments, and add it to
-- the term that `simpa` will simplify before applying.
using
LinearMap.codRestrict_apply s.toSubmodule (CliffordAlgebra.ι Q) x (h := ι)
-- finding a proof is finding an element of the subalgebra
rw [← AlgHom.id_apply (R := R) a, ← of_id]
exact (lift Q of a).prop
