Built with Alectryon. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+πŸ–±οΈ to focus. On Mac, use ⌘ instead of Ctrl.
Hover-Settings: Show types: Show goals:
import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

set_option pp.proofs.withType false

variable {
R: Type ?u.4
R 
M: Type ?u.10
M} [
CommRing: Type ?u.4 β†’ Type ?u.4
CommRing 
R: Type u_1
R] [
Invertible: {Ξ± : Type ?u.4} β†’ [Mul Ξ±] β†’ [One Ξ±] β†’ Ξ± β†’ Type ?u.4
Invertible (
2: R
2 : 
R: Type ?u.4
R)] [
AddCommGroup: Type u_2 β†’ Type u_2
AddCommGroup 
M: Type u_2
M] [
Module: (R : Type ?u.4) β†’ (M : Type ?u.10) β†’ [Semiring R] β†’ [AddCommMonoid M] β†’ Type (max ?u.4 ?u.10)
Module 
R: Type u_1
R 
M: Type ?u.10
M] (
Q: QuadraticForm R M
Q : 
QuadraticForm: (R : Type u_1) β†’
  (M : Type u_2) β†’ [inst : CommSemiring R] β†’ [inst_1 : AddCommMonoid M] β†’ [Module R M] β†’ Type (max u_1 u_2)
QuadraticForm 
R: Type u_1
R 
M: Type ?u.10
M)

abbrev 
ExteriorAlgebra.rMultivector: {R : Type u_1} β†’
  {M : Type u_2} β†’
    [inst : CommRing R] β†’ [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ β„• β†’ Submodule R (ExteriorAlgebra R M)
ExteriorAlgebra.rMultivector (
r: β„•
r : 
β„•: Type
β„•) : 
Submodule: (R : Type u_1) β†’
  (M : Type (max u_2 u_1)) β†’ [inst : Semiring R] β†’ [inst_1 : AddCommMonoid M] β†’ [Module R M] β†’ Type (max u_2 u_1)
Submodule 
R: Type u_1
R (
ExteriorAlgebra: (R : Type u_1) β†’ [inst : CommRing R] β†’ (M : Type u_2) β†’ [inst_1 : AddCommGroup M] β†’ [Module R M] β†’ Type (max u_1 u_2)
ExteriorAlgebra 
R: Type u_1
R 
M: Type u_2
M) :=
  (
LinearMap.range: {R Rβ‚‚ : Type u_1} β†’
  {M : Type u_2} β†’
    {Mβ‚‚ : Type (max u_1 u_2)} β†’
      [inst : Semiring R] β†’
        [inst_1 : Semiring Rβ‚‚] β†’
          [inst_2 : AddCommMonoid M] β†’
            [inst_3 : AddCommMonoid Mβ‚‚] β†’
              [inst_4 : Module R M] β†’
                [inst_5 : Module Rβ‚‚ Mβ‚‚] β†’ {τ₁₂ : R β†’+* Rβ‚‚} β†’ [RingHomSurjective τ₁₂] β†’ (M β†’β‚›β‚—[τ₁₂] Mβ‚‚) β†’ Submodule Rβ‚‚ Mβ‚‚
LinearMap.range (
ExteriorAlgebra.ΞΉ: (R : Type u_1) β†’
  [inst : CommRing R] β†’ {M : Type u_2} β†’ [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ M β†’β‚—[R] ExteriorAlgebra R M
ExteriorAlgebra.ΞΉ 
R: Type u_1
R : 
M: Type u_2
M β†’β‚—[
R: Type u_1
R] 
_: Type (max u_1 u_2)
_) ^ 
r: β„•
r)

-- def ExteriorAlgebra.proj (mv : ExteriorAlgebra R M) (r : β„•) : ExteriorAlgebra R M :=
--   @GradedAlgebra.proj β„• R (ExteriorAlgebra R M) _ _ _ _ _ ExteriorAlgebra.rMultivector _ r mv

-- def ExteriorAlgebra.proj' (mv : ExteriorAlgebra R M) (r : β„•) : ExteriorAlgebra R M :=
--   GradedAlgebra.proj ExteriorAlgebra.rMultivector r mv

namespace CliffordAlgebra

abbrev 
rMultivector: {R : Type u_1} β†’
  {M : Type u_2} β†’
    [inst : CommRing R] β†’
      [Invertible 2] β†’
        [inst_2 : AddCommGroup M] β†’
          [inst_3 : Module R M] β†’ (Q : QuadraticForm R M) β†’ β„• β†’ Submodule R (CliffordAlgebra Q)
rMultivector (
r: β„•
r : 
β„•: Type
β„•) : 
Submodule: (R : Type u_1) β†’
  (M : Type (max u_2 u_1)) β†’ [inst : Semiring R] β†’ [inst_1 : AddCommMonoid M] β†’ [Module R M] β†’ Type (max u_2 u_1)
Submodule 
R: Type u_1
R (
CliffordAlgebra: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’ [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ QuadraticForm R M β†’ Type (max u_1 u_2)
CliffordAlgebra 
Q: QuadraticForm R M
Q) :=
  (
ExteriorAlgebra.rMultivector: {R : Type u_1} β†’
  {M : Type u_2} β†’
    [inst : CommRing R] β†’ [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ β„• β†’ Submodule R (ExteriorAlgebra R M)
ExteriorAlgebra.rMultivector 
r: β„•
r).
comap: {R Rβ‚‚ : Type u_1} β†’
  {M Mβ‚‚ : Type (max u_1 u_2)} β†’
    [inst : Semiring R] β†’
      [inst_1 : Semiring Rβ‚‚] β†’
        [inst_2 : AddCommMonoid M] β†’
          [inst_3 : AddCommMonoid Mβ‚‚] β†’
            [inst_4 : Module R M] β†’
              [inst_5 : Module Rβ‚‚ Mβ‚‚] β†’ {σ₁₂ : R β†’+* Rβ‚‚} β†’ (M β†’β‚›β‚—[σ₁₂] Mβ‚‚) β†’ Submodule Rβ‚‚ Mβ‚‚ β†’ Submodule R M
comap (
CliffordAlgebra.equivExterior: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’
      [inst_1 : AddCommGroup M] β†’
        [inst_2 : Module R M] β†’ (Q : QuadraticForm R M) β†’ [Invertible 2] β†’ CliffordAlgebra Q ≃ₗ[R] ExteriorAlgebra R M
CliffordAlgebra.equivExterior 
Q: QuadraticForm R M
Q).
toLinearMap: {R S : Type u_1} β†’
  [inst : Semiring R] β†’
    [inst_1 : Semiring S] β†’
      {Οƒ : R β†’+* S} β†’
        {Οƒ' : S β†’+* R} β†’
          [inst_2 : RingHomInvPair Οƒ Οƒ'] β†’
            [inst_3 : RingHomInvPair Οƒ' Οƒ] β†’
              {M Mβ‚‚ : Type (max u_1 u_2)} β†’
                [inst_4 : AddCommMonoid M] β†’
                  [inst_5 : AddCommMonoid Mβ‚‚] β†’
                    [inst_6 : Module R M] β†’ [inst_7 : Module S Mβ‚‚] β†’ (M ≃ₛₗ[Οƒ] Mβ‚‚) β†’ M β†’β‚›β‚—[Οƒ] Mβ‚‚
toLinearMap

abbrev 
ofGrade: {r : β„•} β†’ β†₯(rMultivector Q r) β†’ CliffordAlgebra Q
ofGrade {
r: β„•
r : 
β„•: Type
β„•} (
mv: β†₯(rMultivector Q r)
mv : 
rMultivector: {R : Type u_1} β†’
  {M : Type u_2} β†’
    [inst : CommRing R] β†’
      [Invertible 2] β†’
        [inst_2 : AddCommGroup M] β†’
          [inst_3 : Module R M] β†’ (Q : QuadraticForm R M) β†’ β„• β†’ Submodule R (CliffordAlgebra Q)
rMultivector 
Q: QuadraticForm R M
Q 
r: β„•
r) : 
CliffordAlgebra: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’ [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ QuadraticForm R M β†’ Type (max u_1 u_2)
CliffordAlgebra 
Q: QuadraticForm R M
Q := 
mv: β†₯(rMultivector Q r)
mv

variable {Q} in
def 
wedge: CliffordAlgebra Q β†’ CliffordAlgebra Q β†’ CliffordAlgebra Q
wedge (
a: CliffordAlgebra Q
a 
b: CliffordAlgebra Q
b : 
CliffordAlgebra: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’ [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ QuadraticForm R M β†’ Type (max u_1 u_2)
CliffordAlgebra 
Q: QuadraticForm R M
Q) : 
CliffordAlgebra: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’ [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ QuadraticForm R M β†’ Type (max u_1 u_2)
CliffordAlgebra 
Q: QuadraticForm R M
Q :=
  (
equivExterior: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’
      [inst_1 : AddCommGroup M] β†’
        [inst_2 : Module R M] β†’ (Q : QuadraticForm R M) β†’ [Invertible 2] β†’ CliffordAlgebra Q ≃ₗ[R] ExteriorAlgebra R M
equivExterior 
Q: QuadraticForm R M
Q).
symm: {R S : Type u_1} β†’
  {M Mβ‚‚ : Type (max u_1 u_2)} β†’
    [inst : Semiring R] β†’
      [inst_1 : Semiring S] β†’
        [inst_2 : AddCommMonoid M] β†’
          [inst_3 : AddCommMonoid Mβ‚‚] β†’
            {module_M : Module R M} β†’
              {module_S_Mβ‚‚ : Module S Mβ‚‚} β†’
                {Οƒ : R β†’+* S} β†’
                  {Οƒ' : S β†’+* R} β†’
                    {re₁ : RingHomInvPair Οƒ Οƒ'} β†’ {reβ‚‚ : RingHomInvPair Οƒ' Οƒ} β†’ (M ≃ₛₗ[Οƒ] Mβ‚‚) β†’ Mβ‚‚ ≃ₛₗ[Οƒ'] M
symm (
equivExterior: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’
      [inst_1 : AddCommGroup M] β†’
        [inst_2 : Module R M] β†’ (Q : QuadraticForm R M) β†’ [Invertible 2] β†’ CliffordAlgebra Q ≃ₗ[R] ExteriorAlgebra R M
equivExterior 
Q: QuadraticForm R M
Q 
a: CliffordAlgebra Q
a * 
equivExterior: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’
      [inst_1 : AddCommGroup M] β†’
        [inst_2 : Module R M] β†’ (Q : QuadraticForm R M) β†’ [Invertible 2] β†’ CliffordAlgebra Q ≃ₗ[R] ExteriorAlgebra R M
equivExterior 
Q: QuadraticForm R M
Q 
b: CliffordAlgebra Q
b)

infix:65 " ⋏ " => 
wedge: {R : Type u_1} β†’
  {M : Type u_2} β†’
    [inst : CommRing R] β†’
      [Invertible 2] β†’
        [inst_2 : AddCommGroup M] β†’
          [inst_3 : Module R M] β†’ {Q : QuadraticForm R M} β†’ CliffordAlgebra Q β†’ CliffordAlgebra Q β†’ CliffordAlgebra Q
wedge

variable (
r: β„•
r : 
β„•: Type
β„•) (
mv: CliffordAlgebra Q
mv : 
CliffordAlgebra: {R : Type ?u.4} β†’
  [inst : CommRing R] β†’
    {M : Type ?u.10} β†’ [inst_1 : AddCommGroup M] β†’ [inst_2 : Module R M] β†’ QuadraticForm R M β†’ Type (max ?u.4 ?u.10)
CliffordAlgebra 
Q: QuadraticForm R M
Q) in

(equivExterior Q) mv : ExteriorAlgebra R M
 
equivExterior: {R : Type u_1} β†’
  [inst : CommRing R] β†’
    {M : Type u_2} β†’
      [inst_1 : AddCommGroup M] β†’
        [inst_2 : Module R M] β†’ (Q : QuadraticForm R M) β†’ [Invertible 2] β†’ CliffordAlgebra Q ≃ₗ[R] ExteriorAlgebra R M
equivExterior 
Q: QuadraticForm R M
Q 
mv: CliffordAlgebra Q
mv

-- def proj (mv : CliffordAlgebra Q) (i : β„•) : CliffordAlgebra Q := (equivExterior Q).symm ((equivExterior Q mv).proj i)

-- #check proj

theorem 
wedge_mv_mem: βˆ€ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (Q : QuadraticForm R M) {ra rb : β„•} (a : β†₯(rMultivector Q ra)) (b : β†₯(rMultivector Q rb)),
  ↑a ⋏ ↑b ∈ rMultivector Q (ra + rb)
wedge_mv_mem {
ra: β„•
ra 
rb: β„•
rb} (
a: β†₯(rMultivector Q ra)
a : 
rMultivector: {R : Type u_1} β†’
  {M : Type u_2} β†’
    [inst : CommRing R] β†’
      [Invertible 2] β†’
        [inst_2 : AddCommGroup M] β†’
          [inst_3 : Module R M] β†’ (Q : QuadraticForm R M) β†’ β„• β†’ Submodule R (CliffordAlgebra Q)
rMultivector 
Q: QuadraticForm R M
Q 
ra: β„•
ra) (
b: β†₯(rMultivector Q rb)
b : 
rMultivector: {R : Type u_1} β†’
  {M : Type u_2} β†’
    [inst : CommRing R] β†’
      [Invertible 2] β†’
        [inst_2 : AddCommGroup M] β†’
          [inst_3 : Module R M] β†’ (Q : QuadraticForm R M) β†’ β„• β†’ Submodule R (CliffordAlgebra Q)
rMultivector 
Q: QuadraticForm R M
Q 
rb: β„•
rb) :
    
a: β†₯(rMultivector Q ra)
a ⋏ 
b: β†₯(rMultivector Q rb)
b ∈ 
rMultivector: {R : Type u_1} β†’
  {M : Type u_2} β†’
    [inst : CommRing R] β†’
      [Invertible 2] β†’
        [inst_2 : AddCommGroup M] β†’
          [inst_3 : Module R M] β†’ (Q : QuadraticForm R M) β†’ β„• β†’ Submodule R (CliffordAlgebra Q)
rMultivector 
Q: QuadraticForm R M
Q (
ra: β„•
ra + 
rb: β„•
rb) := 
Goals accomplished! πŸ™

  
R: Type u_1
M: Type u_2
inst✝³: CommRing R
inst✝²: Invertible 2
inst✝¹: AddCommGroup M
inst✝: Module R M
Q: QuadraticForm R M
ra, rb: β„•
b: β†₯(rMultivector Q rb)
a: CliffordAlgebra Q
ha: a ∈ rMultivector Q ra
β†‘βŸ¨a, ha⟩ ⋏ ↑b ∈ rMultivector Q (ra + rb)

  
R: Type u_1
M: Type u_2
inst✝³: CommRing R
inst✝²: Invertible 2
inst✝¹: AddCommGroup M
inst✝: Module R M
Q: QuadraticForm R M
ra, rb: β„•
a: CliffordAlgebra Q
ha: a ∈ rMultivector Q ra
b: CliffordAlgebra Q
hb: b ∈ rMultivector Q rb
β†‘βŸ¨a, ha⟩ ⋏ β†‘βŸ¨b, hb⟩ ∈ rMultivector Q (ra + rb)

  
R: Type u_1
M: Type u_2
inst✝³: CommRing R
inst✝²: Invertible 2
inst✝¹: AddCommGroup M
inst✝: Module R M
Q: QuadraticForm R M
ra, rb: β„•
a: CliffordAlgebra Q
ha: a ∈ rMultivector Q ra
b: CliffordAlgebra Q
hb: b ∈ rMultivector Q rb
↑(equivExterior Q) ((equivExterior Q).symm ((equivExterior Q) a * (equivExterior Q) b)) ∈
  ExteriorAlgebra.rMultivector (ra + rb)

  -- v4.32: the semilinear `LinearEquiv` coercion needs an explicit `change` before
  -- `apply_symm_apply` can fire
  
R: Type u_1
M: Type u_2
inst✝³: CommRing R
inst✝²: Invertible 2
inst✝¹: AddCommGroup M
inst✝: Module R M
Q: QuadraticForm R M
ra, rb: β„•
a: CliffordAlgebra Q
ha: a ∈ rMultivector Q ra
b: CliffordAlgebra Q
hb: b ∈ rMultivector Q rb
(equivExterior Q) ((equivExterior Q).symm ((equivExterior Q) a * (equivExterior Q) b)) ∈
  ExteriorAlgebra.rMultivector (ra + rb)

  
R: Type u_1
M: Type u_2
inst✝³: CommRing R
inst✝²: Invertible 2
inst✝¹: AddCommGroup M
inst✝: Module R M
Q: QuadraticForm R M
ra, rb: β„•
a: CliffordAlgebra Q
ha: a ∈ rMultivector Q ra
b: CliffordAlgebra Q
hb: b ∈ rMultivector Q rb
(equivExterior Q) ((equivExterior Q).symm ((equivExterior Q) a * (equivExterior Q) b)) ∈
  ExteriorAlgebra.rMultivector (ra + rb)
R: Type u_1
M: Type u_2
inst✝³: CommRing R
inst✝²: Invertible 2
inst✝¹: AddCommGroup M
inst✝: Module R M
Q: QuadraticForm R M
ra, rb: β„•
a: CliffordAlgebra Q
ha: a ∈ rMultivector Q ra
b: CliffordAlgebra Q
hb: b ∈ rMultivector Q rb
(equivExterior Q) a * (equivExterior Q) b ∈ ExteriorAlgebra.rMultivector (ra + rb)
R: Type u_1
M: Type u_2
inst✝³: CommRing R
inst✝²: Invertible 2
inst✝¹: AddCommGroup M
inst✝: Module R M
Q: QuadraticForm R M
ra, rb: β„•
a: CliffordAlgebra Q
ha: a ∈ rMultivector Q ra
b: CliffordAlgebra Q
hb: b ∈ rMultivector Q rb
(equivExterior Q) a * (equivExterior Q) b ∈ ExteriorAlgebra.rMultivector (ra + rb)

  
Goals accomplished! πŸ™


-- lemma outer_homo {i j} (u : rMultivector Q i) (v : rMultivector Q j) :
--   u ⋏ v = proj Q (u * v) (i + j) := sorry

end CliffordAlgebra