CliffordAlgebra.evenOdd_induction
theorem CliffordAlgebra.evenOdd_induction :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(Q : QuadraticForm R M) (n : ZMod 2) {motive : (x : CliffordAlgebra Q) → x ∈ CliffordAlgebra.evenOdd Q n → Prop},
(∀ (v : CliffordAlgebra Q) (h : v ∈ LinearMap.range (CliffordAlgebra.ι Q) ^ n.val), motive v ⋯) →
(∀ (x y : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q n) (hy : y ∈ CliffordAlgebra.evenOdd Q n),
motive x hx → motive y hy → motive (x + y) ⋯) →
(∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q n),
motive x hx → motive ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) ⋯) →
∀ (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q n), motive x hx
This theorem, `CliffordAlgebra.evenOdd_induction`, is a principle of induction for properties of elements in the even or odd submodules of a Clifford algebra of an `R`-module `M` equipped with a quadratic form `Q`. It states that for a property to hold for all elements in these submodules, it suffices to show that it holds for all vectors (in the range of the canonical linear map from `M` to the Clifford algebra), that it's closed under the addition of elements from the same submodule, and that it's preserved under left multiplication by a pair of vectors. It says that if these conditions are met, then the property must hold for any element in the even or odd submodules of the Clifford algebra.
More concisely: If a property holds for all vectors in an `R`-module `M` equipped with a quadratic form `Q`, is closed under addition of vectors in the same submodule, and is preserved under left multiplication by pairs of vectors, then the property holds for all elements in the even or odd submodules of the Clifford algebra over `M` and `Q`.
|
CliffordAlgebra.even_induction
theorem CliffordAlgebra.even_induction :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(Q : QuadraticForm R M) {motive : (x : CliffordAlgebra Q) → x ∈ CliffordAlgebra.evenOdd Q 0 → Prop},
(∀ (r : R), motive ((algebraMap R (CliffordAlgebra Q)) r) ⋯) →
(∀ (x y : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 0) (hy : y ∈ CliffordAlgebra.evenOdd Q 0),
motive x hx → motive y hy → motive (x + y) ⋯) →
(∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 0),
motive x hx → motive ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) ⋯) →
∀ (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 0), motive x hx
This theorem states that in order to prove a property is true for every element in the even subpart of a Clifford Algebra constructed from a quadratic form `Q`, it suffices to prove three things:
1. The property holds for all scalars from the ring `R` when embedded into the Clifford Algebra.
2. The property is preserved under addition; that is, if the property is true for two elements in the even subpart, then it is also true for their sum.
3. The property is preserved under left multiplication by a pair of vectors from the module `M`; that is, if the property is true for an element in the even subpart, then it is also true for the element multiplied by a pair of vectors.
This is a form of structural induction over the even subpart of a Clifford Algebra.
More concisely: The property holds for every element in the even subpart of a Clifford Algebra constructed from a quadratic form if and only if it holds for scalars, is closed under addition, and is preserved under left multiplication by pairs of vectors from the module.
|
CliffordAlgebra.odd_induction
theorem CliffordAlgebra.odd_induction :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(Q : QuadraticForm R M) {P : (x : CliffordAlgebra Q) → x ∈ CliffordAlgebra.evenOdd Q 1 → Prop},
(∀ (v : M), P ((CliffordAlgebra.ι Q) v) ⋯) →
(∀ (x y : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 1) (hy : y ∈ CliffordAlgebra.evenOdd Q 1),
P x hx → P y hy → P (x + y) ⋯) →
(∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 1),
P x hx → P ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) ⋯) →
∀ (x : CliffordAlgebra Q) (hx : x ∈ CliffordAlgebra.evenOdd Q 1), P x hx
The theorem `CliffordAlgebra.odd_induction` states that to prove a property `P` is true for all elements `x` in the odd part of a Clifford Algebra (constructed from a quadratic form `Q` on an `R`-module `M`), it suffices to show three things: Firstly, the property `P` holds for all vectors `v` in `M` mapped to the Clifford Algebra using the canonical linear map `CliffordAlgebra.ι Q`. Secondly, the property `P` is closed under addition, i.e., if `P` holds for two elements `x` and `y` in the odd part of the Clifford Algebra, then `P` also holds for the sum `x + y`. Lastly, the property `P` is closed under left-multiplication by a pair of vectors, i.e., if `P` holds for an element `x` in the odd part of the Clifford Algebra, then `P` also holds for the result of multiplying `x` by two vectors `m₁` and `m₂` from `M` mapped to the Clifford Algebra.
More concisely: To prove a property holds for all odd elements in a Clifford algebra constructed from a quadratic form over an R-module, it suffices to verify it for elements mapped from module vectors, closure under addition, and closure under left-multiplication by two module vectors.
|
CliffordAlgebra.ι_mul_ι_mem_evenOdd_zero
theorem CliffordAlgebra.ι_mul_ι_mem_evenOdd_zero :
∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
(Q : QuadraticForm R M) (m₁ m₂ : M),
(CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ ∈ CliffordAlgebra.evenOdd Q 0
The theorem `CliffordAlgebra.ι_mul_ι_mem_evenOdd_zero` states that for any commutative ring `R`, any additive commutative group `M`, and any `R`-module `M`, given a quadratic form `Q` on `M` and any two elements `m₁` and `m₂` of `M`, the product of the canonical linear maps of `m₁` and `m₂` under the quadratic form `Q` is an element of the even submodule of the Clifford algebra of `Q`. The even submodule is defined as the supremum of the even powers of the range of the canonical linear map.
More concisely: For any commutative ring R, additive commutative group M, R-module structure on M, quadratic form Q on M, and elements m₁, m₂ in M, the product of the canonical linear maps of m₁ and m₂ under the quadratic form Q lies in the even submodule of the Clifford algebra of Q.
|