exterior_model.lean

import linear_algebra.exterior_algebra
import linear_algebra.basis
import linear_algebra.free_module.basic
import data.list.defs
import algebra.big_operators

namespace exterior_algebra

open_locale big_operators
open_locale classical
noncomputable theory

abbreviation model_basis (R : Type*) [field R] (n : ℕ) := finset (fin n)

variables (R : Type*) [field R] (n : ℕ)

def model := model_basis R n → R

variables {R} {n}

instance : add_comm_monoid (model R n) :=
by { dunfold model, apply_instance }

instance : module R (model R n) :=
by { dunfold model, apply_instance }

def inversions : list (fin n) → ℕ
| [] := 0
| (x :: xs) := (xs.filter (λ y, y < x)).length + inversions xs

/-- in `{-1, 0, 1}` -/
def sign (s t : finset (fin n)) : ℤ :=
let xs : list (fin n) := s.sort (≤),
    ys : list (fin n) := t.sort (≤)
in if s ∩ t = ∅ then (-1) ^ inversions (xs ++ ys) else 0

lemma eq_nil_iff {α : Type*} (s : list α) : s = [] ↔ ∀ x, ¬ x ∈ s :=
by exact list.eq_nil_iff_forall_not_mem

lemma inversions_sorted (s : list (fin n)) (h : s.sorted (<)) : inversions s = 0 :=
begin
  induction s,
  refl,
  simp!,
  simp at h,
  simp [s_ih h.2, list.length_eq_zero, list.eq_nil_iff_forall_not_mem],
  intros a ha,
  apply le_of_lt,
  exact h.1 a ha,
end

@[simp] lemma inversions_sort (s : finset (fin n)) : inversions (s.sort (≤)) = 0 :=
begin
  apply inversions_sorted,
  exact finset.sort_sorted_lt s,
end

@[simp] lemma sort_empty : finset.sort (≤) (∅ : finset (fin n)) = [] :=
begin
  simp [list.eq_nil_iff_forall_not_mem],
end

@[simp] lemma sign_snd_empty (s : finset (fin n)) : sign s ∅ = 1 :=
begin
  simp [sign],
end

@[simp] lemma sign_fst_empty (s : finset (fin n)) : sign ∅ s = 1 :=
begin
  simp [sign],
end

lemma sign_assoc (s t u : finset (fin n)) :
  sign s t * sign (s ∪ t) u = sign s (t ∪ u) * sign t u :=
begin
  sorry,
end

def partitions (b : model_basis R n) : finset (model_basis R n × model_basis R n) :=
finset.univ.filter (λ p, disjoint p.1 p.2 ∧ b = p.1 ∪ p.2)

lemma partitions_prop (p1 p2 b : model_basis R n) :
  (p1, p2) ∈ partitions b ↔ disjoint p1 p2 ∧ b = p1 ∪ p2 :=
begin
  simp [partitions],
end

lemma partitions_swap (p1 p2 b : model_basis R n) :
  (p1, p2) ∈ partitions b ↔ (p2, p1) ∈ partitions b :=
begin
  simp only [partitions_prop],
  simp [disjoint.comm, finset.union_comm],
end

lemma partitions_swap' (b : model_basis R n) :
  (partitions b).image prod.swap = partitions b :=
begin
  ext a,
  cases a with p1 p2,
  simp,
  split,
  rintro ⟨b1,b2,h,rfl,rfl⟩,
  rwa partitions_swap,
  intro h,
  rw partitions_swap at h,
  exact ⟨p2, p1, h, rfl, rfl⟩,
end

lemma partitions_filter_snd_empty (b : model_basis R n) :
  (partitions b).filter (λ p, p.snd = ∅) = {(b, ∅)} :=
begin
  ext p,
  cases p with p1 p2,
  simp [partitions_prop, eq_comm] {contextual := tt},
end

lemma partitions_filter_fst_empty (b : model_basis R n) :
  (partitions b).filter (λ p, p.fst = ∅) = {(∅, b)} :=
begin
  change (partitions b).filter ((λ p, prod.snd p = ∅) ∘ prod.swap) = _,
  rw ←partitions_swap',
  rw finset.image_filter,
  change finset.image prod.swap ((partitions b).filter (λ p, p.snd = ∅)) = _,
  rw partitions_filter_snd_empty,
  ext, simp,
end

/-- convolution using the partitions and the sign function -/
def mul (x y : model R n) : model R n := λ b,
∑ p in partitions b, sign p.1 p.2 * x p.1 * y p.2

variables {R} {n}

instance : semiring (model R n) :=
{ add := λ x y, x + y,
  add_comm := add_comm,
  add_assoc := add_assoc,
  zero := 0,
  zero_add := zero_add,
  add_zero := add_zero,
  mul := mul,
  one := λ b, if b = ∅ then 1 else 0,
  mul_one := λ x, begin
    ext b,
    simp [mul, finset.sum_ite, partitions_filter_snd_empty],
  end,
  one_mul := λ x, begin
    ext b,
    simp [mul, finset.sum_ite, partitions_filter_fst_empty],
  end,
  zero_mul := λ x, begin
    ext b,
    simp [mul],
  end,
  mul_zero := λ x, begin
    ext b,
    simp [mul],
  end,
  mul_assoc := λ x y z, begin
    ext b,
    simp [mul],
    convert_to ∑ p in partitions b, ∑ p' in partitions p.fst, (sign p.fst p.snd * sign p'.fst p'.snd : R) * x p'.fst * y p'.snd * z p.snd =
      ∑ p in partitions b, ∑ p' in partitions p.snd, (sign p.fst p.snd * sign p'.fst p'.snd : R) * x p.fst * y p'.fst * y p'.snd,
    sorry
  end,
}

end exterior_algebra