The universal property of the even subalgebra

Main definitions

• CliffordAlgebra.even Q: The even subalgebra of CliffordAlgebra Q.
• CliffordAlgebra.EvenHom: The type of bilinear maps that satisfy the universal property of the even subalgebra
• CliffordAlgebra.even.lift: The universal property of the even subalgebra, which states that every bilinear map f with f v v = Q v and f u v * f v w = Q v • f u w is in unique correspondence with an algebra morphism from CliffordAlgebra.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 CliffordAlgebra.lift: the first is to use morphisms as the output type, such as A = Module.End R N which is how we obtained CliffordAlgebra.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 CliffordAlgebra.even {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : Subalgebra R (CliffordAlgebra Q)

The even submodule CliffordAlgebra.evenOdd Q 0 is also a subalgebra.

Equations

• CliffordAlgebra.even Q = (CliffordAlgebra.evenOdd Q 0).toSubalgebra ⋯ ⋯

instance CliffordAlgebra.instAddCommMonoidSubtypeMemSubalgebraEven {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : AddCommMonoid ↥(CliffordAlgebra.even Q)

Equations

• CliffordAlgebra.instAddCommMonoidSubtypeMemSubalgebraEven Q = AddSubmonoidClass.toAddCommMonoid (CliffordAlgebra.even Q)

@[simp]

theorem CliffordAlgebra.even_toSubmodule {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : Subalgebra.toSubmodule (CliffordAlgebra.even Q) = CliffordAlgebra.evenOdd Q 0

structure CliffordAlgebra.EvenHom {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (A : Type uA) [Ring A] [Algebra R A] : Type (max uA uM)

The type of bilinear maps which are accepted by CliffordAlgebra.even.lift.

• bilin : M →ₗ[R] M →ₗ[R] A
• contract : ∀ (m : M), (self.bilin m) m = (algebraMap R A) (Q m)
• contract_mid : ∀ (m₁ m₂ m₃ : M), (self.bilin m₁) m₂ * (self.bilin m₂) m₃ = Q m₂ • (self.bilin m₁) m₃

theorem CliffordAlgebra.EvenHom.ext {R : Type uR} {M : Type uM} : ∀ {inst : CommRing R} {inst_1 : AddCommGroup M} {inst_2 : Module R M} {Q : QuadraticForm R M} {A : Type uA} {inst_3 : Ring A} {inst_4 : Algebra R A} {x y : CliffordAlgebra.EvenHom Q A}, x.bilin = y.bilin → x = y

theorem CliffordAlgebra.EvenHom.contract {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {A : Type uA} [Ring A] [Algebra R A] (self : CliffordAlgebra.EvenHom Q A) (m : M) : (self.bilin m) m = (algebraMap R A) (Q m)

theorem CliffordAlgebra.EvenHom.contract_mid {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {A : Type uA} [Ring A] [Algebra R A] (self : CliffordAlgebra.EvenHom Q A) (m₁ : M) (m₂ : M) (m₃ : M) : (self.bilin m₁) m₂ * (self.bilin m₂) m₃ = Q m₂ • (self.bilin m₁) m₃

def CliffordAlgebra.EvenHom.compr₂ {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {A : Type uA} {B : Type uB} [Ring A] [Ring B] [Algebra R A] [Algebra R B] (g : CliffordAlgebra.EvenHom Q A) (f : A →ₐ[R] B) : CliffordAlgebra.EvenHom Q B

Compose an EvenHom with an AlgHom on the output.

Equations

• g.compr₂ f = { bilin := g.bilin.compr₂ f.toLinearMap, contract := ⋯, contract_mid := ⋯ }

@[simp]

theorem CliffordAlgebra.EvenHom.compr₂_bilin {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {A : Type uA} {B : Type uB} [Ring A] [Ring B] [Algebra R A] [Algebra R B] (g : CliffordAlgebra.EvenHom Q A) (f : A →ₐ[R] B) : (g.compr₂ f).bilin = g.bilin.compr₂ f.toLinearMap

def CliffordAlgebra.even.ι {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : CliffordAlgebra.EvenHom Q ↥(CliffordAlgebra.even Q)

The embedding of pairs of vectors into the even subalgebra, as a bilinear map.

Equations

• CliffordAlgebra.even.ι Q = { bilin := LinearMap.mk₂ R (fun (m₁ m₂ : M) => ⟨(CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂, ⋯⟩) ⋯ ⋯ ⋯ ⋯, contract := ⋯, contract_mid := ⋯ }

instance CliffordAlgebra.instInhabitedEvenHomSubtypeMemSubalgebraEven {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : Inhabited (CliffordAlgebra.EvenHom Q ↥(CliffordAlgebra.even Q))

Equations

• CliffordAlgebra.instInhabitedEvenHomSubtypeMemSubalgebraEven Q = { default := CliffordAlgebra.even.ι Q }

theorem CliffordAlgebra.even.algHom_ext {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {A : Type uA} [Ring A] [Algebra R A] ⦃f : ↥(CliffordAlgebra.even Q) →ₐ[R] A⦄ ⦃g : ↥(CliffordAlgebra.even Q) →ₐ[R] A⦄ (h : (CliffordAlgebra.even.ι Q).compr₂ f = (CliffordAlgebra.even.ι Q).compr₂ g) : f = g

Two algebra morphisms from the even subalgebra are equal if they agree on pairs of generators.

See note [partially-applied ext lemmas].

def CliffordAlgebra.even.lift.aux {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {A : Type uA} [Ring A] [Algebra R A] (f : CliffordAlgebra.EvenHom Q A) : ↥(CliffordAlgebra.even Q) →ₗ[R] A

The final auxiliary construction for CliffordAlgebra.even.lift. This map is the forwards direction of that equivalence, but not in the fully-bundled form.

Equations

• One or more equations did not get rendered due to their size.

theorem CliffordAlgebra.even.lift.aux_apply {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {A : Type uA} [Ring A] [Algebra R A] (f : CliffordAlgebra.EvenHom Q A) : ∀ (a : ↥(CliffordAlgebra.even Q)), (CliffordAlgebra.even.lift.aux f) a = (((CliffordAlgebra.foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (1, 0)) ↑a).1

@[simp]

theorem CliffordAlgebra.even.lift.aux_one {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {A : Type uA} [Ring A] [Algebra R A] (f : CliffordAlgebra.EvenHom Q A) : (CliffordAlgebra.even.lift.aux f) 1 = 1

@[simp]

theorem CliffordAlgebra.even.lift.aux_ι {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {A : Type uA} [Ring A] [Algebra R A] (f : CliffordAlgebra.EvenHom Q A) (m₁ : M) (m₂ : M) : (CliffordAlgebra.even.lift.aux f) (((CliffordAlgebra.even.ι Q).bilin m₁) m₂) = (f.bilin m₁) m₂

@[simp]

theorem CliffordAlgebra.even.lift.aux_algebraMap {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {A : Type uA} [Ring A] [Algebra R A] (f : CliffordAlgebra.EvenHom Q A) (r : R) (hr : (algebraMap R (CliffordAlgebra Q)) r ∈ CliffordAlgebra.even Q) : (CliffordAlgebra.even.lift.aux f) ⟨(algebraMap R (CliffordAlgebra Q)) r, hr⟩ = (algebraMap R A) r

@[simp]

theorem CliffordAlgebra.even.lift.aux_mul {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {A : Type uA} [Ring A] [Algebra R A] (f : CliffordAlgebra.EvenHom Q A) (x : ↥(CliffordAlgebra.even Q)) (y : ↥(CliffordAlgebra.even Q)) : (CliffordAlgebra.even.lift.aux f) (x * y) = (CliffordAlgebra.even.lift.aux f) x * (CliffordAlgebra.even.lift.aux f) y

def CliffordAlgebra.even.lift {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {A : Type uA} [Ring A] [Algebra R A] : CliffordAlgebra.EvenHom Q A ≃ (↥(CliffordAlgebra.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

• One or more equations did not get rendered due to their size.

@[simp]

theorem CliffordAlgebra.even.lift_symm_apply_bilin {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {A : Type uA} [Ring A] [Algebra R A] (F : ↥(CliffordAlgebra.even Q) →ₐ[R] A) : ((CliffordAlgebra.even.lift Q).symm F).bilin = (CliffordAlgebra.even.ι Q).bilin.compr₂ F.toLinearMap

theorem CliffordAlgebra.even.lift_ι {R : Type uR} {M : Type uM} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {A : Type uA} [Ring A] [Algebra R A] (f : CliffordAlgebra.EvenHom Q A) (m₁ : M) (m₂ : M) : ((CliffordAlgebra.even.lift Q) f) (((CliffordAlgebra.even.ι Q).bilin m₁) m₂) = (f.bilin m₁) m₂