Documentation

TauCeti.LinearAlgebra.CliffordAlgebra.PBW

PBW equivalence for a Clifford filtration #

This file identifies the associated graded algebra of the Clifford degree filtration with the exterior algebra when 2 is invertible. It combines the equivalences on the successive quotients with their compatibility with homogeneous multiplication.

This completes the associated-graded-algebra part of Layer 0 in the spin representations roadmap.

Main definition #

Main result #

References #

source
theorem CliffordAlgebra.prod_map_ι_ofFn_ne_zero {M : Type v} [AddCommGroup M] {K : Type u} [Field K] [Module K M] (Q : QuadraticForm K M) {n : ℕ} (v : Fin n → M) (hv : LinearIndependent K v) :
(List.ofFn (⇑(ι Q) ∘ v)).prod ≠ 0

An ordered product of Clifford generators from a linearly independent finite family is nonzero, in every characteristic. This is the multiplicative PBW independence statement.

source
noncomputable def CliffordAlgebra.gradedPieceEquivExteriorPower {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (n : ℕ) :
TauCeti.Algebra.wordFiltration.GradedPiece (ι Q) n ≃ₗ[R] ↥(⋀[R]^n M)

The canonical equivalence from each graded filtration piece to the corresponding exterior power.

Equations
Instances For
    source
    @[simp]
    theorem CliffordAlgebra.gradedPieceEquivExteriorPower_apply_algebraMap₀ {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (r : R) :
    (gradedPieceEquivExteriorPower Q 0) ((TauCeti.Algebra.wordFiltration.gradedAlgebraMap₀ (ι Q)) r) = (exteriorPower.zeroEquiv R M).symm r

    The degree-zero piece equivalence sends a scalar class to the corresponding exterior scalar.

    source
    @[simp]
    theorem CliffordAlgebra.gradedPieceEquivExteriorPower_symm_apply_zeroEquiv_symm {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (r : R) :
    (gradedPieceEquivExteriorPower Q 0).symm ((exteriorPower.zeroEquiv R M).symm r) = (TauCeti.Algebra.wordFiltration.gradedAlgebraMap₀ (ι Q)) r

    The inverse degree-zero piece equivalence sends an exterior scalar to its scalar class.

    source
    noncomputable def CliffordAlgebra.associatedGradedEquivExterior {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] :
    TauCeti.Algebra.wordFiltration.AssociatedGraded (ι Q) ≃ₐ[R] ExteriorAlgebra R M

    The associated graded of the Clifford filtration is the exterior algebra.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CliffordAlgebra.associatedGradedEquivExterior_apply_of {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (n : ℕ) (x : TauCeti.Algebra.wordFiltration.GradedPiece (ι Q) n) :
      (associatedGradedEquivExterior Q) ((DirectSum.of (TauCeti.Algebra.wordFiltration.GradedPiece (ι Q)) n) x) = ↑((gradedPieceEquivExteriorPower Q n) x)

      The associated-graded equivalence on an arbitrary homogeneous piece.

      source
      @[simp]
      theorem CliffordAlgebra.associatedGradedEquivExterior_symm_apply_coe {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (n : ℕ) (x : ↥(⋀[R]^n M)) :
      (associatedGradedEquivExterior Q).symm ↑x = (DirectSum.of (TauCeti.Algebra.wordFiltration.GradedPiece (ι Q)) n) ((gradedPieceEquivExteriorPower Q n).symm x)

      The inverse associated-graded equivalence on an arbitrary exterior power.

      source
      @[simp]
      theorem CliffordAlgebra.associatedGradedEquivExterior_apply_of_succ {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (n : ℕ) (x : TauCeti.Algebra.wordFiltration.GradedPiece (ι Q) (n + 1)) :
      (associatedGradedEquivExterior Q) ((DirectSum.of (TauCeti.Algebra.wordFiltration.GradedPiece (ι Q)) (n + 1)) x) = ↑((filtrationGradedEquiv Q n) x)

      On a positive-degree homogeneous piece, the total equivalence is filtrationGradedEquiv.

      source
      @[simp]
      theorem CliffordAlgebra.associatedGradedEquivExterior_symm_apply_coe_succ {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (n : ℕ) (x : ↥(⋀[R]^(n + 1) M)) :
      (associatedGradedEquivExterior Q).symm ↑x = (DirectSum.of (TauCeti.Algebra.wordFiltration.GradedPiece (ι Q)) (n + 1)) ((filtrationGradedEquiv Q n).symm x)

      The inverse on a positive-degree exterior power is the inverse graded equivalence.