Grade selection with Mathlib

GeometricGrades.lean

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