Physlib.Relativity.CliffordAlgebra

Physlib
Relativity
CliffordAlgebra

Imports

/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Mathlib.Analysis.Complex.Basic
public import Mathlib.Data.Matrix.Reflection
public import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
public import Physlib.Meta.TODO.Basic

The Clifford Algebra

This file defines the Gamma matrices and their relationship to the Clifford algebra.

Main Definitions

γ0, γ1, γ2, γ3: The four gamma matrices in the Dirac representation (4×4 complex matrices)

γSet: The set of gamma matrices

diracForm: The quadratic form with Minkowski signature (+,-,-,-) corresponding to the gamma matrices

diracAlgebra: The algebra generated by the gamma matrices over ℝ

ofCliffordAlgebra: The algebra homomorphism from the Clifford algebra to diracAlgebra

Main Results

ofCliffordAlgebra_surjective: The homomorphism ofCliffordAlgebra is surjective

TODO

Complete the isomorphism by proving injectivity of ofCliffordAlgebra (requires dimension theory)

Construct the AlgEquiv between CliffordAlgebra diracForm and diracAlgebra

@[expose] public sectionTODO "Prove injectivity of ofCliffordAlgebra and construct the full isomorphism."

The γ⁰ gamma matrix in the Dirac representation.

def γ0 : Matrix (Fin 4) (Fin 4) ℂ :=
  !![1, 0, 0, 0; 0, 1, 0, 0; 0, 0, -1, 0; 0, 0, 0, -1]

The γ¹ gamma matrix in the Dirac representation.

def γ1 : Matrix (Fin 4) (Fin 4) ℂ :=
  !![0, 0, 0, 1; 0, 0, 1, 0; 0, -1, 0, 0; -1, 0, 0, 0]

The γ² gamma matrix in the Dirac representation.

def γ2 : Matrix (Fin 4) (Fin 4) ℂ :=
  !![0, 0, 0, - I; 0, 0, I, 0; 0, I, 0, 0; -I, 0, 0, 0]

The γ³ gamma matrix in the Dirac representation.

def γ3 : Matrix (Fin 4) (Fin 4) ℂ :=
  !![0, 0, 1, 0; 0, 0, 0, -1; -1, 0, 0, 0; 0, 1, 0, 0]

              theorem _root_.Matrix.one_fin_four {α} [Zero α] [One α] :
    (1 : Matrix (Fin 4) (Fin 4) α) = !![1, 0, 0, 0; 0, 1, 0, 0; 0, 0, 1, 0; 0, 0, 0, 1] :=
  Matrix.etaExpand_eq _ |>.symm@[simp] lemma γ0_mul_γ0 : γ0 * γ0 = 1 := by⊢ γ0 * γ0 = 1 simp [γ0, Matrix.one_fin_four]All goals completed! 🐙@[simp] lemma γ1_mul_γ1 : γ1 * γ1 = -1 := by⊢ γ1 * γ1 = -1 simp [γ1, Matrix.one_fin_four]All goals completed! 🐙@[simp] lemma γ2_mul_γ2 : γ2 * γ2 = -1 := by⊢ γ2 * γ2 = -1 simp [γ2, Matrix.one_fin_four]All goals completed! 🐙@[simp] lemma γ3_mul_γ3 : γ3 * γ3 = -1 := by⊢ γ3 * γ3 = -1 simp [γ3, Matrix.one_fin_four]All goals completed! 🐙@[simp] lemma γ1_mul_γ0 : γ1 * γ0 = -(γ0 * γ1) := by⊢ γ1 * γ0 = -(γ0 * γ1) simp [γ0, γ1]All goals completed! 🐙@[simp] lemma γ2_mul_γ0 : γ2 * γ0 = -(γ0 * γ2) := by⊢ γ2 * γ0 = -(γ0 * γ2) simp [γ0, γ2]All goals completed! 🐙@[simp] lemma γ3_mul_γ0 : γ3 * γ0 = -(γ0 * γ3) := by⊢ γ3 * γ0 = -(γ0 * γ3) simp [γ0, γ3]All goals completed! 🐙@[simp] lemma γ2_mul_γ1 : γ2 * γ1 = -(γ1 * γ2) := by⊢ γ2 * γ1 = -(γ1 * γ2) simp [γ1, γ2]All goals completed! 🐙@[simp] lemma γ3_mul_γ1 : γ3 * γ1 = -(γ1 * γ3) := by⊢ γ3 * γ1 = -(γ1 * γ3) simp [γ1, γ3]All goals completed! 🐙@[simp] lemma γ3_mul_γ2 : γ3 * γ2 = -(γ2 * γ3) := by⊢ γ3 * γ2 = -(γ2 * γ3) simp [γ2, γ3]All goals completed! 🐙

The γ⁵ gamma matrix in the Dirac representation.

def γ5 : Matrix (Fin 4) (Fin 4) ℂ := I • (γ0 * γ1 * γ2 * γ3)

The γ gamma matrices in the Dirac representation.

@[simp]
def γ : Fin 4 → Matrix (Fin 4) (Fin 4) ℂ := ![γ0, γ1, γ2, γ3]

The subset of Matrix (Fin 4) (Fin 4) ℂ formed by the gamma matrices in the Dirac representation.

@[simp]
def γSet : Set (Matrix (Fin 4) (Fin 4) ℂ) := {γ i | i : Fin 4}

lemma γ_in_γSet (μ : Fin 4) : γ μ ∈ γSet := byμ:Fin 4⊢ γ μ ∈ γSet
  simp [γSet]All goals completed! 🐙

The algebra generated by the gamma matrices in the Dirac representation.

def diracAlgebra : Subalgebra ℝ (Matrix (Fin 4) (Fin 4) ℂ) :=
  Algebra.adjoin ℝ γSet

lemma γSet_subset_diracAlgebra : γSet ⊆ diracAlgebra :=
  Algebra.subset_adjoin

lemma γ_in_diracAlgebra (μ : Fin 4) : γ μ ∈ diracAlgebra :=
  γSet_subset_diracAlgebra (γ_in_γSet μ)

The quadratic form of the clifford algebra corresponding to the γ matrices.

@[simps!]
def diracForm : QuadraticForm ℝ (Fin 4 → ℝ) :=
  QuadraticMap.sq.comp (LinearMap.proj 0)
    - QuadraticMap.sq.comp (LinearMap.proj 1)
    - QuadraticMap.sq.comp (LinearMap.proj 2)
    - QuadraticMap.sq.comp (LinearMap.proj 3)

The injection from the clifford algebra over diracForm into the algebra generated by the γ matrices.

def ofCliffordAlgebra : CliffordAlgebra diracForm →ₐ[ℝ] diracAlgebra :=
  CliffordAlgebra.lift _
    ⟨∑ i, (LinearMap.proj i).smulRight ⟨γ i, γ_in_diracAlgebra _⟩, fun v => byμ:Fin 4ν:Fin 4v:Fin 4 → ℝ⊢ (∑ i, (LinearMap.proj i).smulRight ⟨γ i, ⋯⟩) v * (∑ i, (LinearMap.proj i).smulRight ⟨γ i, ⋯⟩) v =
  (algebraMap ℝ ↥diracAlgebra) (diracForm v)
      ext : 1μ:Fin 4ν:Fin 4v:Fin 4 → ℝ⊢ ↑((∑ i, (LinearMap.proj i).smulRight ⟨γ i, ⋯⟩) v * (∑ i, (LinearMap.proj i).smulRight ⟨γ i, ⋯⟩) v) =
  ↑((algebraMap ℝ ↥diracAlgebra) (diracForm v))
      simp only [γ, Fin.sum_univ_four, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one,
        Matrix.cons_val, LinearMap.add_apply, LinearMap.coe_smulRight, LinearMap.coe_proj,
        Function.eval, SetLike.mk_smul_mk, AddMemClass.mk_add_mk, MulMemClass.mk_mul_mk, mul_add,
        Algebra.mul_smul_comm, add_mul, Algebra.smul_mul_assoc, γ0_mul_γ0, γ1_mul_γ0, smul_neg,
        γ2_mul_γ0, γ3_mul_γ0, smul_add, γ1_mul_γ1, γ2_mul_γ1, γ3_mul_γ1, γ2_mul_γ2, γ3_mul_γ2,
        γ3_mul_γ3, diracForm_apply, Algebra.algebraMap_eq_smul_one, SetLike.val_smul,
        OneMemClass.coe_one]μ:Fin 4ν:Fin 4v:Fin 4 → ℝ⊢ v 0 • v 0 • 1 + -(v 0 • v 1 • (γ0 * γ1)) + -(v 0 • v 2 • (γ0 * γ2)) + -(v 0 • v 3 • (γ0 * γ3)) +
        (v 1 • v 0 • (γ0 * γ1) + -(v 1 • v 1 • 1) + -(v 1 • v 2 • (γ1 * γ2)) + -(v 1 • v 3 • (γ1 * γ3))) +
      (v 2 • v 0 • (γ0 * γ2) + v 2 • v 1 • (γ1 * γ2) + -(v 2 • v 2 • 1) + -(v 2 • v 3 • (γ2 * γ3))) +
    (v 3 • v 0 • (γ0 * γ3) + v 3 • v 1 • (γ1 * γ3) + v 3 • v 2 • (γ2 * γ3) + -(v 3 • v 3 • 1)) =
  (v 0 * v 0 - v 1 * v 1 - v 2 * v 2 - v 3 * v 3) • 1
      moduleAll goals completed! 🐙⟩

The generators of the clifford algebra correspond to the elements γ.


@[simp]
lemma ofCliffordAlgebra_ι_single (i : Fin 4) (r : ℝ) :
    ofCliffordAlgebra (CliffordAlgebra.ι _ (Pi.single i r)) = r • ⟨γ i, γ_in_diracAlgebra _⟩ :=
  CliffordAlgebra.lift_ι_apply _ _ _ |>.trans <| Subtype.ext <| byi:Fin 4r:ℝ⊢ ↑((∑ i, (LinearMap.proj i).smulRight ⟨γ i, ⋯⟩) (Pi.single i r)) = ↑(r • ⟨γ i, ⋯⟩)
    simp only [γ, LinearMap.coe_sum, LinearMap.coe_smulRight, LinearMap.coe_proj, Function.eval,
      SetLike.mk_smul_mk, Finset.sum_apply, AddSubmonoidClass.coe_finsetSum]i:Fin 4r:ℝ⊢ ∑ x, Pi.single i r x • ![γ0, γ1, γ2, γ3] x = r • ![γ0, γ1, γ2, γ3] i
    rw [Finset.sum_eq_single ii:Fin 4r:ℝ⊢ Pi.single i r i • ![γ0, γ1, γ2, γ3] i = r • ![γ0, γ1, γ2, γ3] ih₀i:Fin 4r:ℝ⊢ ∀ b ∈ Finset.univ, b ≠ i → Pi.single i r b • ![γ0, γ1, γ2, γ3] b = 0h₁i:Fin 4r:ℝ⊢ i ∉ Finset.univ → Pi.single i r i • ![γ0, γ1, γ2, γ3] i = 0i:Fin 4r:ℝ⊢ Pi.single i r i • ![γ0, γ1, γ2, γ3] i = r • ![γ0, γ1, γ2, γ3] ih₀i:Fin 4r:ℝ⊢ ∀ b ∈ Finset.univ, b ≠ i → Pi.single i r b • ![γ0, γ1, γ2, γ3] b = 0h₁i:Fin 4r:ℝ⊢ i ∉ Finset.univ → Pi.single i r i • ![γ0, γ1, γ2, γ3] i = 0]i:Fin 4r:ℝ⊢ Pi.single i r i • ![γ0, γ1, γ2, γ3] i = r • ![γ0, γ1, γ2, γ3] ih₀i:Fin 4r:ℝ⊢ ∀ b ∈ Finset.univ, b ≠ i → Pi.single i r b • ![γ0, γ1, γ2, γ3] b = 0h₁i:Fin 4r:ℝ⊢ i ∉ Finset.univ → Pi.single i r i • ![γ0, γ1, γ2, γ3] i = 0
    ·i:Fin 4r:ℝ⊢ Pi.single i r i • ![γ0, γ1, γ2, γ3] i = r • ![γ0, γ1, γ2, γ3] i simpAll goals completed! 🐙
    ·h₀i:Fin 4r:ℝ⊢ ∀ b ∈ Finset.univ, b ≠ i → Pi.single i r b • ![γ0, γ1, γ2, γ3] b = 0 intro b _ hbh₀i:Fin 4r:ℝb:Fin 4a✝:b ∈ Finset.univhb:b ≠ i⊢ Pi.single i r b • ![γ0, γ1, γ2, γ3] b = 0
      simp [Pi.single_eq_of_ne hb]All goals completed! 🐙
    ·h₁i:Fin 4r:ℝ⊢ i ∉ Finset.univ → Pi.single i r i • ![γ0, γ1, γ2, γ3] i = 0 simpAll goals completed! 🐙

Surjectivity of ofCliffordAlgebra

Each gamma matrix (as an element of diracAlgebra) is in the range of ofCliffordAlgebra.

lemma γ_subtype_in_range (i : Fin 4) :
    ⟨γ i, γ_in_diracAlgebra i⟩ ∈ ofCliffordAlgebra.range := byi:Fin 4⊢ ⟨γ i, ⋯⟩ ∈ ofCliffordAlgebra.range
  use CliffordAlgebra.ι diracForm (Pi.single i 1)hi:Fin 4⊢ ofCliffordAlgebra.toRingHom ((CliffordAlgebra.ι diracForm) (Pi.single i 1)) = ⟨γ i, ⋯⟩
  simp [ofCliffordAlgebra_ι_single]All goals completed! 🐙

Helper lemma: If a matrix is in Algebra.adjoin ℝ γSet, then its subtype is in the range.

private lemma mem_adjoin_imp_subtype_in_range (m : Matrix (Fin 4) (Fin 4) ℂ)
    (hm : m ∈ Algebra.adjoin ℝ γSet) : ⟨m, hm⟩ ∈ ofCliffordAlgebra.range := bym:Matrix (Fin 4) (Fin 4) ℂhm:m ∈ Algebra.adjoin ℝ γSet⊢ ⟨m, hm⟩ ∈ ofCliffordAlgebra.range
  induction hm using Algebra.adjoin_induction with
  | mem y hy =>memm:Matrix (Fin 4) (Fin 4) ℂy:Matrix (Fin 4) (Fin 4) ℂhy:y ∈ γSet⊢ ⟨y, ⋯⟩ ∈ ofCliffordAlgebra.range
    -- y ∈ γSet, so y = γ i for some i
    obtain ⟨i, rfl⟩ := hymemm:Matrix (Fin 4) (Fin 4) ℂi:Fin 4⊢ ⟨γ i, ⋯⟩ ∈ ofCliffordAlgebra.range
    exact γ_subtype_in_range iAll goals completed! 🐙
  | algebraMap r =>algebraMapm:Matrix (Fin 4) (Fin 4) ℂr:ℝ⊢ ⟨(algebraMap ℝ (Matrix (Fin 4) (Fin 4) ℂ)) r, ⋯⟩ ∈ ofCliffordAlgebra.range
    -- r from ℝ
    use algebraMap ℝ _ rhm:Matrix (Fin 4) (Fin 4) ℂr:ℝ⊢ ofCliffordAlgebra.toRingHom ((algebraMap ℝ (CliffordAlgebra diracForm)) r) =
  ⟨(algebraMap ℝ (Matrix (Fin 4) (Fin 4) ℂ)) r, ⋯⟩
    exthm:Matrix (Fin 4) (Fin 4) ℂr:ℝi✝:Fin 4j✝:Fin 4⊢ ↑(ofCliffordAlgebra.toRingHom ((algebraMap ℝ (CliffordAlgebra diracForm)) r)) i✝ j✝ =
  ↑⟨(algebraMap ℝ (Matrix (Fin 4) (Fin 4) ℂ)) r, ⋯⟩ i✝ j✝
    simp [Algebra.algebraMap_eq_smul_one]All goals completed! 🐙
  | add y z _ _ hy hz =>addm:Matrix (Fin 4) (Fin 4) ℂy:Matrix (Fin 4) (Fin 4) ℂz:Matrix (Fin 4) (Fin 4) ℂhx✝:y ∈ Algebra.adjoin ℝ γSethy✝:z ∈ Algebra.adjoin ℝ γSethy:⟨y, hx✝⟩ ∈ ofCliffordAlgebra.rangehz:⟨z, hy✝⟩ ∈ ofCliffordAlgebra.range⊢ ⟨y + z, ⋯⟩ ∈ ofCliffordAlgebra.range
    -- If y and z are in range, so is y + z
    obtain ⟨y', hy'⟩ := hyaddm:Matrix (Fin 4) (Fin 4) ℂy:Matrix (Fin 4) (Fin 4) ℂz:Matrix (Fin 4) (Fin 4) ℂhx✝:y ∈ Algebra.adjoin ℝ γSethy✝:z ∈ Algebra.adjoin ℝ γSethz:⟨z, hy✝⟩ ∈ ofCliffordAlgebra.rangey':CliffordAlgebra diracFormhy':ofCliffordAlgebra.toRingHom y' = ⟨y, hx✝⟩⊢ ⟨y + z, ⋯⟩ ∈ ofCliffordAlgebra.range
    obtain ⟨z', hz'⟩ := hzaddm:Matrix (Fin 4) (Fin 4) ℂy:Matrix (Fin 4) (Fin 4) ℂz:Matrix (Fin 4) (Fin 4) ℂhx✝:y ∈ Algebra.adjoin ℝ γSethy✝:z ∈ Algebra.adjoin ℝ γSety':CliffordAlgebra diracFormhy':ofCliffordAlgebra.toRingHom y' = ⟨y, hx✝⟩z':CliffordAlgebra diracFormhz':ofCliffordAlgebra.toRingHom z' = ⟨z, hy✝⟩⊢ ⟨y + z, ⋯⟩ ∈ ofCliffordAlgebra.range
    use y' + z'hm:Matrix (Fin 4) (Fin 4) ℂy:Matrix (Fin 4) (Fin 4) ℂz:Matrix (Fin 4) (Fin 4) ℂhx✝:y ∈ Algebra.adjoin ℝ γSethy✝:z ∈ Algebra.adjoin ℝ γSety':CliffordAlgebra diracFormhy':ofCliffordAlgebra.toRingHom y' = ⟨y, hx✝⟩z':CliffordAlgebra diracFormhz':ofCliffordAlgebra.toRingHom z' = ⟨z, hy✝⟩⊢ ofCliffordAlgebra.toRingHom (y' + z') = ⟨y + z, ⋯⟩
    ext : 1hm:Matrix (Fin 4) (Fin 4) ℂy:Matrix (Fin 4) (Fin 4) ℂz:Matrix (Fin 4) (Fin 4) ℂhx✝:y ∈ Algebra.adjoin ℝ γSethy✝:z ∈ Algebra.adjoin ℝ γSety':CliffordAlgebra diracFormhy':ofCliffordAlgebra.toRingHom y' = ⟨y, hx✝⟩z':CliffordAlgebra diracFormhz':ofCliffordAlgebra.toRingHom z' = ⟨z, hy✝⟩⊢ ↑(ofCliffordAlgebra.toRingHom (y' + z')) = ↑⟨y + z, ⋯⟩
    have hy'' : (ofCliffordAlgebra y' : Matrix (Fin 4) (Fin 4) ℂ) = y := congr_arg Subtype.val hy'hm:Matrix (Fin 4) (Fin 4) ℂy:Matrix (Fin 4) (Fin 4) ℂz:Matrix (Fin 4) (Fin 4) ℂhx✝:y ∈ Algebra.adjoin ℝ γSethy✝:z ∈ Algebra.adjoin ℝ γSety':CliffordAlgebra diracFormhy':ofCliffordAlgebra.toRingHom y' = ⟨y, hx✝⟩z':CliffordAlgebra diracFormhz':ofCliffordAlgebra.toRingHom z' = ⟨z, hy✝⟩hy'':↑(ofCliffordAlgebra y') = y⊢ ↑(ofCliffordAlgebra.toRingHom (y' + z')) = ↑⟨y + z, ⋯⟩
    have hz'' : (ofCliffordAlgebra z' : Matrix (Fin 4) (Fin 4) ℂ) = z := congr_arg Subtype.val hz'hm:Matrix (Fin 4) (Fin 4) ℂy:Matrix (Fin 4) (Fin 4) ℂz:Matrix (Fin 4) (Fin 4) ℂhx✝:y ∈ Algebra.adjoin ℝ γSethy✝:z ∈ Algebra.adjoin ℝ γSety':CliffordAlgebra diracFormhy':ofCliffordAlgebra.toRingHom y' = ⟨y, hx✝⟩z':CliffordAlgebra diracFormhz':ofCliffordAlgebra.toRingHom z' = ⟨z, hy✝⟩hy'':↑(ofCliffordAlgebra y') = yhz'':↑(ofCliffordAlgebra z') = z⊢ ↑(ofCliffordAlgebra.toRingHom (y' + z')) = ↑⟨y + z, ⋯⟩
    simp [hy'', hz'']All goals completed! 🐙
  | mul y z _ _ hy hz =>mulm:Matrix (Fin 4) (Fin 4) ℂy:Matrix (Fin 4) (Fin 4) ℂz:Matrix (Fin 4) (Fin 4) ℂhx✝:y ∈ Algebra.adjoin ℝ γSethy✝:z ∈ Algebra.adjoin ℝ γSethy:⟨y, hx✝⟩ ∈ ofCliffordAlgebra.rangehz:⟨z, hy✝⟩ ∈ ofCliffordAlgebra.range⊢ ⟨y * z, ⋯⟩ ∈ ofCliffordAlgebra.range
    -- If y and z are in range, so is y * z
    obtain ⟨y', hy'⟩ := hymulm:Matrix (Fin 4) (Fin 4) ℂy:Matrix (Fin 4) (Fin 4) ℂz:Matrix (Fin 4) (Fin 4) ℂhx✝:y ∈ Algebra.adjoin ℝ γSethy✝:z ∈ Algebra.adjoin ℝ γSethz:⟨z, hy✝⟩ ∈ ofCliffordAlgebra.rangey':CliffordAlgebra diracFormhy':ofCliffordAlgebra.toRingHom y' = ⟨y, hx✝⟩⊢ ⟨y * z, ⋯⟩ ∈ ofCliffordAlgebra.range
    obtain ⟨z', hz'⟩ := hzmulm:Matrix (Fin 4) (Fin 4) ℂy:Matrix (Fin 4) (Fin 4) ℂz:Matrix (Fin 4) (Fin 4) ℂhx✝:y ∈ Algebra.adjoin ℝ γSethy✝:z ∈ Algebra.adjoin ℝ γSety':CliffordAlgebra diracFormhy':ofCliffordAlgebra.toRingHom y' = ⟨y, hx✝⟩z':CliffordAlgebra diracFormhz':ofCliffordAlgebra.toRingHom z' = ⟨z, hy✝⟩⊢ ⟨y * z, ⋯⟩ ∈ ofCliffordAlgebra.range
    use y' * z'hm:Matrix (Fin 4) (Fin 4) ℂy:Matrix (Fin 4) (Fin 4) ℂz:Matrix (Fin 4) (Fin 4) ℂhx✝:y ∈ Algebra.adjoin ℝ γSethy✝:z ∈ Algebra.adjoin ℝ γSety':CliffordAlgebra diracFormhy':ofCliffordAlgebra.toRingHom y' = ⟨y, hx✝⟩z':CliffordAlgebra diracFormhz':ofCliffordAlgebra.toRingHom z' = ⟨z, hy✝⟩⊢ ofCliffordAlgebra.toRingHom (y' * z') = ⟨y * z, ⋯⟩
    ext : 1hm:Matrix (Fin 4) (Fin 4) ℂy:Matrix (Fin 4) (Fin 4) ℂz:Matrix (Fin 4) (Fin 4) ℂhx✝:y ∈ Algebra.adjoin ℝ γSethy✝:z ∈ Algebra.adjoin ℝ γSety':CliffordAlgebra diracFormhy':ofCliffordAlgebra.toRingHom y' = ⟨y, hx✝⟩z':CliffordAlgebra diracFormhz':ofCliffordAlgebra.toRingHom z' = ⟨z, hy✝⟩⊢ ↑(ofCliffordAlgebra.toRingHom (y' * z')) = ↑⟨y * z, ⋯⟩
    have hy'' : (ofCliffordAlgebra y' : Matrix (Fin 4) (Fin 4) ℂ) = y := congr_arg Subtype.val hy'hm:Matrix (Fin 4) (Fin 4) ℂy:Matrix (Fin 4) (Fin 4) ℂz:Matrix (Fin 4) (Fin 4) ℂhx✝:y ∈ Algebra.adjoin ℝ γSethy✝:z ∈ Algebra.adjoin ℝ γSety':CliffordAlgebra diracFormhy':ofCliffordAlgebra.toRingHom y' = ⟨y, hx✝⟩z':CliffordAlgebra diracFormhz':ofCliffordAlgebra.toRingHom z' = ⟨z, hy✝⟩hy'':↑(ofCliffordAlgebra y') = y⊢ ↑(ofCliffordAlgebra.toRingHom (y' * z')) = ↑⟨y * z, ⋯⟩
    have hz'' : (ofCliffordAlgebra z' : Matrix (Fin 4) (Fin 4) ℂ) = z := congr_arg Subtype.val hz'hm:Matrix (Fin 4) (Fin 4) ℂy:Matrix (Fin 4) (Fin 4) ℂz:Matrix (Fin 4) (Fin 4) ℂhx✝:y ∈ Algebra.adjoin ℝ γSethy✝:z ∈ Algebra.adjoin ℝ γSety':CliffordAlgebra diracFormhy':ofCliffordAlgebra.toRingHom y' = ⟨y, hx✝⟩z':CliffordAlgebra diracFormhz':ofCliffordAlgebra.toRingHom z' = ⟨z, hy✝⟩hy'':↑(ofCliffordAlgebra y') = yhz'':↑(ofCliffordAlgebra z') = z⊢ ↑(ofCliffordAlgebra.toRingHom (y' * z')) = ↑⟨y * z, ⋯⟩
    simp [hy'', hz'']All goals completed! 🐙

The range of ofCliffordAlgebra equals the top subalgebra (i.e., all of diracAlgebra).


lemma ofCliffordAlgebra_range_eq_top : ofCliffordAlgebra.range = ⊤ := by⊢ ofCliffordAlgebra.range = ⊤
  rw [eq_top_iff⊢ ⊤ ≤ ofCliffordAlgebra.range⊢ ⊤ ≤ ofCliffordAlgebra.range]⊢ ⊤ ≤ ofCliffordAlgebra.range
  intro x _x:↥diracAlgebraa✝:x ∈ ⊤⊢ x ∈ ofCliffordAlgebra.range
  exact mem_adjoin_imp_subtype_in_range x.val x.propertyAll goals completed! 🐙

The homomorphism ofCliffordAlgebra is surjective.


theorem ofCliffordAlgebra_surjective : Function.Surjective ofCliffordAlgebra := by⊢ Function.Surjective ⇑ofCliffordAlgebra
  rw [← AlgHom.range_eq_top⊢ ofCliffordAlgebra.range = ⊤⊢ ofCliffordAlgebra.range = ⊤]⊢ ofCliffordAlgebra.range = ⊤
  exact ofCliffordAlgebra_range_eq_topAll goals completed! 🐙