The universal property of the even subalgebra #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
clifford_algebra.even Q: The even subalgebra ofclifford_algebra Q.clifford_algebra.even_hom: The type of bilinear maps that satisfy the universal property of the even subalgebraclifford_algebra.even.lift: The universal property of the even subalgebra, which states that every bilinear mapfwithf v v = Q vandf u v * f v w = Q v • f u wis in unique correspondence with an algebra morphism fromclifford_algebra.even Q.
Implementation notes #
The approach here is outlined in "Computing with the universal properties of the Clifford algebra and the even subalgebra" (to appear).
The broad summary is that we have two tricks available to us for implementing complex recursors on
top of clifford_algebra.lift: the first is to use morphisms as the output type, such as
A = module.End R N which is how we obtained clifford_algebra.foldr; and the second is to use
N = (N', S) where N' is the value we wish to compute, and S is some auxiliary state passed
between one recursor invocation and the next.
For the universal property of the even subalgebra, we apply a variant of the first trick again by
choosing S to itself be a submodule of morphisms.
def
clifford_algebra.even
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
subalgebra R (clifford_algebra Q)
The even submodule clifford_algebra.even_odd Q 0 is also a subalgebra.
Equations
- clifford_algebra.even Q = (clifford_algebra.even_odd Q 0).to_subalgebra _ _
@[simp]
theorem
clifford_algebra.even_to_submodule
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
@[ext]
structure
clifford_algebra.even_hom
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(A : Type u_3)
[ring A]
[algebra R A] :
Type (max u_2 u_3)
- bilin : M →ₗ[R] M →ₗ[R] A
- contract : ∀ (m : M), ⇑(⇑(self.bilin) m) m = ⇑(algebra_map R A) (⇑Q m)
- contract_mid : ∀ (m₁ m₂ m₃ : M), ⇑(⇑(self.bilin) m₁) m₂ * ⇑(⇑(self.bilin) m₂) m₃ = ⇑Q m₂ • ⇑(⇑(self.bilin) m₁) m₃
The type of bilinear maps which are accepted by clifford_algebra.even.lift.
Instances for clifford_algebra.even_hom
- clifford_algebra.even_hom.has_sizeof_inst
- clifford_algebra.even_hom.inhabited
theorem
clifford_algebra.even_hom.ext_iff
{R : Type u_1}
{M : Type u_2}
{_inst_1 : comm_ring R}
{_inst_2 : add_comm_group M}
{_inst_3 : module R M}
{Q : quadratic_form R M}
{A : Type u_3}
{_inst_4 : ring A}
{_inst_6 : algebra R A}
(x y : clifford_algebra.even_hom Q A) :
theorem
clifford_algebra.even_hom.ext
{R : Type u_1}
{M : Type u_2}
{_inst_1 : comm_ring R}
{_inst_2 : add_comm_group M}
{_inst_3 : module R M}
{Q : quadratic_form R M}
{A : Type u_3}
{_inst_4 : ring A}
{_inst_6 : algebra R A}
(x y : clifford_algebra.even_hom Q A)
(h : x.bilin = y.bilin) :
x = y
def
clifford_algebra.even_hom.compr₂
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
{A : Type u_3}
{B : Type u_4}
[ring A]
[ring B]
[algebra R A]
[algebra R B]
(g : clifford_algebra.even_hom Q A)
(f : A →ₐ[R] B) :
Compose an even_hom with an alg_hom on the output.
Equations
- g.compr₂ f = {bilin := g.bilin.compr₂ f.to_linear_map, contract := _, contract_mid := _}
@[simp]
theorem
clifford_algebra.even_hom.compr₂_bilin
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
{A : Type u_3}
{B : Type u_4}
[ring A]
[ring B]
[algebra R A]
[algebra R B]
(g : clifford_algebra.even_hom Q A)
(f : A →ₐ[R] B) :
@[simp]
theorem
clifford_algebra.even.ι_bilin_apply_apply_coe
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
(m m₂ : M) :
↑(⇑(⇑((clifford_algebra.even.ι Q).bilin) m) m₂) = ⇑(clifford_algebra.ι Q) m * ⇑(clifford_algebra.ι Q) m₂
def
clifford_algebra.even.ι
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
The embedding of pairs of vectors into the even subalgebra, as a bilinear map.
Equations
- clifford_algebra.even.ι Q = {bilin := linear_map.mk₂ R (λ (m₁ m₂ : M), ⟨⇑(clifford_algebra.ι Q) m₁ * ⇑(clifford_algebra.ι Q) m₂, _⟩) _ _ _ _, contract := _, contract_mid := _}
@[protected, instance]
def
clifford_algebra.even_hom.inhabited
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M) :
Equations
@[ext]
theorem
clifford_algebra.even.alg_hom_ext
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
{A : Type u_3}
[ring A]
[algebra R A]
⦃f g : ↥(clifford_algebra.even Q) →ₐ[R] A⦄
(h : (clifford_algebra.even.ι Q).compr₂ f = (clifford_algebra.even.ι Q).compr₂ g) :
f = g
Two algebra morphisms from the even subalgebra are equal if they agree on pairs of generators.
def
clifford_algebra.even.lift.aux
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
{A : Type u_3}
[ring A]
[algebra R A]
(f : clifford_algebra.even_hom Q A) :
↥(clifford_algebra.even Q) →ₗ[R] A
The final auxiliary construction for clifford_algebra.even.lift. This map is the forwards
direction of that equivalence, but not in the fully-bundled form.
Equations
- clifford_algebra.even.lift.aux f = ((linear_map.fst R A ↥(S f)).comp (⇑(clifford_algebra.foldr Q (f_fold f) _) (1, 0))).comp (clifford_algebra.even Q).val.to_linear_map
theorem
clifford_algebra.even.lift.aux_apply
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
{A : Type u_3}
[ring A]
[algebra R A]
(f : clifford_algebra.even_hom Q A)
(ᾰ : ↥(clifford_algebra.even Q)) :
⇑(clifford_algebra.even.lift.aux f) ᾰ = (⇑(⇑(clifford_algebra.foldr Q (f_fold f) _) (1, 0)) ↑ᾰ).fst
@[simp]
theorem
clifford_algebra.even.lift.aux_one
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
{A : Type u_3}
[ring A]
[algebra R A]
(f : clifford_algebra.even_hom Q A) :
⇑(clifford_algebra.even.lift.aux f) 1 = 1
@[simp]
theorem
clifford_algebra.even.lift.aux_ι
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
{A : Type u_3}
[ring A]
[algebra R A]
(f : clifford_algebra.even_hom Q A)
(m₁ m₂ : M) :
⇑(clifford_algebra.even.lift.aux f) (⇑(⇑((clifford_algebra.even.ι Q).bilin) m₁) m₂) = ⇑(⇑(f.bilin) m₁) m₂
@[simp]
theorem
clifford_algebra.even.lift.aux_algebra_map
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
{A : Type u_3}
[ring A]
[algebra R A]
(f : clifford_algebra.even_hom Q A)
(r : R)
(hr : ⇑(algebra_map R (clifford_algebra Q)) r ∈ clifford_algebra.even Q) :
⇑(clifford_algebra.even.lift.aux f) ⟨⇑(algebra_map R (clifford_algebra Q)) r, hr⟩ = ⇑(algebra_map R A) r
@[simp]
theorem
clifford_algebra.even.lift.aux_mul
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
{A : Type u_3}
[ring A]
[algebra R A]
(f : clifford_algebra.even_hom Q A)
(x y : ↥(clifford_algebra.even Q)) :
⇑(clifford_algebra.even.lift.aux f) (x * y) = ⇑(clifford_algebra.even.lift.aux f) x * ⇑(clifford_algebra.even.lift.aux f) y
@[simp]
theorem
clifford_algebra.even.lift_symm_apply_bilin
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
{A : Type u_3}
[ring A]
[algebra R A]
(F : ↥(clifford_algebra.even Q) →ₐ[R] A) :
(⇑((clifford_algebra.even.lift Q).symm) F).bilin = (clifford_algebra.even.ι Q).bilin.compr₂ F.to_linear_map
def
clifford_algebra.even.lift
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
{A : Type u_3}
[ring A]
[algebra R A] :
clifford_algebra.even_hom Q A ≃ (↥(clifford_algebra.even Q) →ₐ[R] A)
Every algebra morphism from the even subalgebra is in one-to-one correspondence with a bilinear map that sends duplicate arguments to the quadratic form, and contracts across multiplication.
Equations
- clifford_algebra.even.lift Q = {to_fun := λ (f : clifford_algebra.even_hom Q A), alg_hom.of_linear_map (clifford_algebra.even.lift.aux f) _ _, inv_fun := λ (F : ↥(clifford_algebra.even Q) →ₐ[R] A), (clifford_algebra.even.ι Q).compr₂ F, left_inv := _, right_inv := _}
@[simp]
theorem
clifford_algebra.even.lift_ι
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
(Q : quadratic_form R M)
{A : Type u_3}
[ring A]
[algebra R A]
(f : clifford_algebra.even_hom Q A)
(m₁ m₂ : M) :