CliffordAlgebra.ι_sq_scalar
theorem CliffordAlgebra.ι_sq_scalar :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(Q : QuadraticForm R M) (m : M),
(CliffordAlgebra.ι Q) m * (CliffordAlgebra.ι Q) m = (algebraMap R (CliffordAlgebra Q)) (Q m)
The theorem `CliffordAlgebra.ι_sq_scalar` states that for any commutative ring `R`, and any `R`-module `M` equipped with a quadratic form `Q`, and for any element `m` of `M`, the mapping `ι Q` (which is a linear map from `M` to the Clifford algebra of `Q`) has the property that the square of this mapping applied to `m` is equal to the algebra map from `R` to the Clifford algebra of `Q` applied to the value of the quadratic form `Q` at `m`. In other words, the square of the canonical linear map of `m` is equivalent to the algebra map of the quadratic form evaluated at `m`.
More concisely: For any commutative ring `R`, `R`-module `M` with quadratic form `Q`, and `m` in `M`, the square of the linear map `ιQ(m)` from `M` to the Clifford algebra of `Q` equals the algebra map of `Q` evaluated at `m`.
|
CliffordAlgebra.map_id
theorem CliffordAlgebra.map_id :
∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_4} [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁]
(Q₁ : QuadraticForm R M₁),
CliffordAlgebra.map (QuadraticForm.Isometry.id Q₁) = AlgHom.id R (CliffordAlgebra Q₁)
The theorem `CliffordAlgebra.map_id` states that for any commutative ring `R`, an additive commutative group `M₁`, and a module `M₁` over `R`, and given a quadratic form `Q₁` on `M₁`, the mapping of the identity isometry from the quadratic form `Q₁` to itself (via the `CliffordAlgebra.map` function) is identical to the identity map on the Clifford algebra of `Q₁` as an algebra homomorphism (represented by `AlgHom.id R (CliffordAlgebra Q₁)`). In other words, the identity isometry on a quadratic form is equivalent to the identity algebra homomorphism on the corresponding Clifford algebra.
More concisely: The identity isometry of a quadratic form over a commutative ring is equivalent to the identity algebra homomorphism on its corresponding Clifford algebra.
|
CliffordAlgebra.induction
theorem CliffordAlgebra.induction :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M} {C : CliffordAlgebra Q → Prop},
(∀ (r : R), C ((algebraMap R (CliffordAlgebra Q)) r)) →
(∀ (x : M), C ((CliffordAlgebra.ι Q) x)) →
(∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)) →
(∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)) → ∀ (a : CliffordAlgebra Q), C a
This theorem states that for any commutative ring `R`, any additive commutative group `M` that is also an `R`-module, and any quadratic form `Q` on `M`, if a property `C` holds for the algebraic mapping of an element `r` of `R` into the Clifford algebra `CliffordAlgebra Q`, and for the canonical linear map `ι` of an element `x` from `M` into `CliffordAlgebra Q`, moreover, if this property `C` is preserved under both the multiplication and addition of the elements of `CliffordAlgebra Q`, then it must hold for all elements of `CliffordAlgebra Q`.
This induction principle is quite powerful, as it allows us to prove properties about all elements of the Clifford algebra, provided we can prove them for elements coming from the base ring and module and show that they are preserved under the algebraic operations.
More concisely: Given a commutative ring `R`, an `R`-module `M` with a quadratic form `Q`, if a property `C` holds for all elements of `CliffordAlgebra Q` that map from `R` and `M`, and is closed under multiplication and addition in `CliffordAlgebra Q`, then `C` holds for all elements of `CliffordAlgebra Q`.
|
CliffordAlgebra.ι_mul_ι_mul_ι
theorem CliffordAlgebra.ι_mul_ι_mul_ι :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M} (a b : M),
(CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a =
(CliffordAlgebra.ι Q) (QuadraticForm.polar (⇑Q) a b • a - Q a • b)
This theorem states that, for any commutative ring `R`, additive commutative group `M`, and `M` as a module over `R`, together with a quadratic form `Q` from `M` to `R` and any two vectors `a` and `b` from `M`, the product of the canonical linear map on `a`, `b`, and `a` (in the Clifford Algebra of `Q`) is equivalent to the canonical linear map on the result of the polar of the quadratic form `Q` applied to `a` and `b`, scaled by `a` and subtracted by `b` scaled by the value of the quadratic form `Q` at `a`. This can be written in mathematical notation as for $a, b \in M$: $\iota(a)\iota(b)\iota(a) = \iota((Q^{polar}(a, b)a - Q(a)b))$.
More concisely: For any commutative ring `R`, additive commutative group `M`, quadratic form `Q` on `M`, and vectors `a, b` in `M`, the product of canonical linear maps of `a`, `b`, and `a` in the Clifford algebra equals the scaled and translated canonical linear map of `Q`'s polar form applied to `a` and `b`.
|
CliffordAlgebra.ι_mul_ι_add_swap
theorem CliffordAlgebra.ι_mul_ι_add_swap :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M} (a b : M),
(CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b + (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a =
(algebraMap R (CliffordAlgebra Q)) (QuadraticForm.polar (⇑Q) a b)
This theorem, titled `CliffordAlgebra.ι_mul_ι_add_swap`, states that for any commutative ring `R`, additive commutative group `M` which is also a module over `R`, and any quadratic form `Q` on `M`, the symmetric product of two vectors `a` and `b` under the canonical linear map from `M` to the Clifford Algebra of `Q`, when added together, equals the image of the polar of the quadratic form `Q` at `a` and `b` under the embedding from `R` to the Clifford Algebra of `Q`. In mathematical terms, it says that $(ι(a) * ι(b) + ι(b) * ι(a)) = η(Q_p(a, b))$ where `ι` is the canonical linear map, `η` is the algebra map, and `Q_p` is the polar of the quadratic form `Q`.
More concisely: For any commutative ring `R`, additive commutative group `M` being an `R`-module, and quadratic form `Q` on `M`, the symmetric product of two vectors `a` and `b` under the canonical linear map to the Clifford Algebra of `Q` equals the polar form value of `Q` at `a` and `b` under the algebra map. In symbols: $(ι(a) * ι(b) + ι(b) * ι(a)) = η(Q\_p(a, b))$.
|
CliffordAlgebra.forall_mul_self_eq_iff
theorem CliffordAlgebra.forall_mul_self_eq_iff :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M} {A : Type u_4} [inst_3 : Ring A] [inst_4 : Algebra R A],
IsUnit 2 →
∀ (f : M →ₗ[R] A),
(∀ (x : M), f x * f x = (algebraMap R A) (Q x)) ↔
(LinearMap.mul R A).compl₂ f ∘ₗ f + (LinearMap.mul R A).flip.compl₂ f ∘ₗ f =
LinearMap.compr₂ Q.polarBilin (Algebra.linearMap R A)
This theorem, `CliffordAlgebra.forall_mul_self_eq_iff`, provides an alternative way to prove that a function squares to a quadratic form when `2` is invertible. It states that for any commutative ring `R`, an additive commutative group `M`, a module `M` over `R`, a quadratic form `Q` on `M`, a ring `A`, and a R-algebra `A`, if `2` is a unit in `R`, then a linear map `f` from `M` to `A` satisfies the property `f(x) * f(x) = algebraMap R A (Q x)` for all `x` in `M` if and only if the sum of the composition of `f` with `LinearMap.mul R A` applied to `f` and the composition of `f` with the flipped version of this linear map equals the composition of `Q.polarBilin` with the canonical ring homomorphism `algebraMap R A`, packaged as an R-linear map. Simply put, it equates the squared function to the quadratic form via a sum of compositions with bilinear mappings.
More concisely: For a commutative ring `R`, an additive commutative group `M`, a module `M` over `R`, a quadratic form `Q` on `M`, a ring `A`, and a R-algebra `A`, if `2` is invertible in `R`, then a linear map `f` from `M` to `A` satisfies `f(x) * f(x) = algebraMap R A (Q x)` for all `x` in `M` if and only if `f` and the flipped version of `f` satisfy the condition `Q.polarBilin ∘ algebraMap R A = (f ∘ LinearMap.mul R A ∘ f) + (f ∘ LinearMap.mulRFlip R A ∘ f)`.
|
CliffordAlgebra.hom_ext
theorem CliffordAlgebra.hom_ext :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M} {A : Type u_4} [inst_3 : Semiring A] [inst_4 : Algebra R A]
{f g : CliffordAlgebra Q →ₐ[R] A},
f.toLinearMap ∘ₗ CliffordAlgebra.ι Q = g.toLinearMap ∘ₗ CliffordAlgebra.ι Q → f = g
This theorem, named `CliffordAlgebra.hom_ext`, states that for any commutative ring `R`, additive commutative group `M`, `R`-module `M`, quadratic form `Q` of `M` over `R`, semiring `A` and algebra `A` over `R`, if we have two algebra homomorphisms `f` and `g` from the Clifford Algebra of `Q` to `A`, such that the composition of `f` and `g` with the canonical linear map from `M` to the Clifford Algebra of `Q` are equal when considered as linear maps, then `f` and `g` themselves must be equal. This theorem captures an important property of homomorphisms in the context of algebraic structures, demonstrating that the equal compositions of the homomorphisms with a canonical linear map imply the equality of the homomorphisms themselves.
More concisely: Given commutative rings R, additive commutative groups M as an R-module, quadratic forms Q over R, semirings A, and algebra homomorphisms f and g from the Clifford Algebra of Q to A such that their compositions with the canonical linear map from M to the Clifford Algebra of Q are equal, then f and g are equal.
|
CliffordAlgebra.lift_ι_apply
theorem CliffordAlgebra.lift_ι_apply :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Semiring A] [inst_4 : Algebra R A] (f : M →ₗ[R] A)
(cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)) (x : M),
((CliffordAlgebra.lift Q) ⟨f, cond⟩) ((CliffordAlgebra.ι Q) x) = f x
This theorem states that for any commutative ring `R`, any additive commutative group `M` that is also a module over `R`, any quadratic form `Q` on `M` with values in `R`, any semiring `A` that is also an algebra over `R`, any linear map `f` from `M` to `A` satisfying the condition that for each `m` in `M`, the square of `f(m)` equals the image of `Q(m)` under the algebra map from `R` to `A`, and any `x` in `M`, applying the lift of `Q` to the pair consisting of `f` and this condition to the result of applying the canonical linear map from `M` to the Clifford algebra of `Q` to `x` gives the same result as applying `f` to `x`. In other words, the lift of the quadratic form respects the application of the canonical map and the linear map `f`.
More concisely: For any commutative ring `R`, additive commutative group `M` as an `R`-module, quadratic form `Q` on `M` with values in `R`, semiring `A` as an `R`-algebra, linear map `f : M → A` satisfying `f(m)² = Q(m)(map R A)`, and `x` in `M`, the lift of `Q` to the Clifford algebra of `Q` applied to the pair `(f, (m ↦ f(m)² = Q(m)(map R A)))` and the canonical map from `M` to the Clifford algebra of `Q` applied to `x` yields the same result as applying `f` to `x`.
|
CliffordAlgebra.map_comp_map
theorem CliffordAlgebra.map_comp_map :
∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [inst_1 : AddCommGroup M₁]
[inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
[inst_6 : Module R M₃] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃}
(f : Q₂.Isometry Q₃) (g : Q₁.Isometry Q₂),
(CliffordAlgebra.map f).comp (CliffordAlgebra.map g) = CliffordAlgebra.map (f.comp g)
The theorem `CliffordAlgebra.map_comp_map` states that for any three types `M₁`, `M₂`, and `M₃` that are equipped with the structure of an additive commutative group and a module over a commutative ring `R`, and any three quadratic forms `Q₁`, `Q₂`, and `Q₃` over these respective modules, if there exists an isometry `f` from `Q₂` to `Q₃` and an isometry `g` from `Q₁` to `Q₂`, then the composition of the algebra homomorphisms induced by `map` operation on `f` and `g` in the Clifford algebra is equal to the algebra homomorphism induced by the `map` operation on the composition of `f` and `g`. This theorem essentially establishes the compatibility of the `map` operation in the Clifford algebra with the composition of isometries.
More concisely: Given isometries \(f: Q₂ \to Q₃\) and \(g: Q₁ \to Q₂\) between quadratic forms over additive commutative groups \(M₁, M₂, M₃\) over a commutative ring \(R\), the induced homomorphisms in the Clifford algebra commute: \(Cl(g) \circ Cl(f) = Cl(f \circ g)\).
|