Skip to content

Instantly share code, notes, and snippets.

@eric-wieser
Created November 21, 2023 13:28
Show Gist options
  • Save eric-wieser/05b3947863d502c86fd5e0592831761b to your computer and use it in GitHub Desktop.
Save eric-wieser/05b3947863d502c86fd5e0592831761b to your computer and use it in GitHub Desktop.
Grade selection with Mathlib
import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
set_option pp.proofs.withType false
variable {R M} [CommRing R] [Invertible (2 : R)] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M)
abbrev ExteriorAlgebra.rMultivector (r : ℕ) : Submodule R (ExteriorAlgebra R M) :=
(LinearMap.range (ExteriorAlgebra.ι R : M →ₗ[R] _) ^ r)
namespace CliffordAlgebra
abbrev rMultivector (r : ℕ) : Submodule R (CliffordAlgebra Q) :=
(ExteriorAlgebra.rMultivector r).comap (CliffordAlgebra.equivExterior Q)
abbrev ofGrade {r : ℕ} (mv : rMultivector Q r) : CliffordAlgebra Q := mv
def gradeSelect (x : CliffordAlgebra Q) (r : ℕ) : rMultivector Q r :=
⟨(equivExterior Q).symm <|
DirectSum.decompose ExteriorAlgebra.rMultivector (equivExterior Q x) r, by
simp only [rMultivector, LinearEquiv.apply_symm_apply, Submodule.mem_comap]
exact Subtype.prop _⟩
variable {Q} in
def wedge (a b : CliffordAlgebra Q) : CliffordAlgebra Q :=
(equivExterior Q).symm (equivExterior Q a * equivExterior Q b)
infix:65 " ⋏ " => wedge
theorem wedge_mv_mem {ra rb} (a : rMultivector Q ra) (b : rMultivector Q rb) :
a ⋏ b ∈ rMultivector Q (ra + rb) := by
obtain ⟨a, ha⟩ := a
obtain ⟨b, hb⟩ := b
simp only [wedge, rMultivector, Submodule.mem_comap, LinearEquiv.apply_symm_apply] at *
apply SetLike.mul_mem_graded <;> assumption
end CliffordAlgebra
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment