An attempt at a quotient definition

src/geometric_algebra/nursery/quotient_of_tensor.lean

@@ -0,0 +1,202 @@
+import geometric_algebra.nursery.tensor_algebra
+import geometric_algebra.nursery.tensor_algebra_ring
+import ring_theory.ideals
+import linear_algebra.quadratic_form
+
+open tensor_algebra
+
+universes u
+
+-- produce the setoid corresponding to the ideal of a subalgebra
+def setoid_ideal_of_subalgebra
+  {R : Type u} {A : Type u} [comm_ring R] [ring A] [algebra R A]
+  (s : subalgebra R A) : setoid A
+:= {
+  r := λ a b, a - b ∈ s,
+  iseqv := ⟨
+    λ a, by {rw sub_self, exact subalgebra.zero_mem _},
+    λ a b h, by {rw ←neg_sub, exact subalgebra.neg_mem _ h},
+    λ a b c hab hbc, by {
+      have hac := subalgebra.add_mem _ hab hbc,
+      rw [add_sub, sub_add, sub_self, sub_zero] at hac,
+      exact hac,
+    }⟩}
+
+namespace clifford_algebra
+
+variables {R : Type u} [comm_ring R]
+variables {M : Type u} [add_comm_group M] [module R M]
+variables (Q : quadratic_form R M)
+
+-- tensor parametrized by the quadratic form, just so we have a unique type
+include Q
+def pre := tensor_algebra R M
+omit Q
+namespace pre
+  instance : ring (pre Q) := tensor_algebra.ring R M
+  instance : algebra R (pre Q) := tensor_algebra.algebra R M
+end pre
+
+-- produce the setoid corresponding to the ideal of a subalgebra
+def setoid_ideal_of_subalgebra
+  {R : Type u} {A : Type u} [comm_ring R] [ring A] [algebra R A]
+  (s : subalgebra R A) : setoid A
+:= {
+  r := λ a b, a - b ∈ s,
+  iseqv := ⟨
+    λ a, by {rw sub_self, exact subalgebra.zero_mem _},
+    λ a b h, by {rw ←neg_sub, exact subalgebra.neg_mem _ h},
+    λ a b c hab hbc, by {
+      have hac := subalgebra.add_mem _ hab hbc,
+      rw [add_sub, sub_add, sub_self, sub_zero] at hac,
+      exact hac,
+    }⟩}
+
+-- we can't use the builtin idea, as that requires commutativity
+def ga_ideal : subalgebra R (pre Q) := algebra.adjoin R {
+  i | ∃ v, univ R M v * univ R M v - algebra_map R (pre Q) (Q v) = i
+}
+
+-- declare e
+instance : setoid (pre Q) := setoid_ideal_of_subalgebra (ga_ideal Q)
+
+end clifford_algebra
+
+#check ideal
+
+@[reducible]
+def clifford_algebra
+  {R : Type u} [comm_ring R]
+  {M : Type u} [add_comm_group M] [module R M]
+  (Q : quadratic_form R M) :=
+quotient (clifford_algebra.setoid Q)
+
+namespace clifford_algebra
+variables {R : Type u} [comm_ring R]
+variables {M : Type u} [add_comm_group M] [module R M]
+variables {Q : quadratic_form R M}
+
+instance : has_scalar R (clifford_algebra Q) := {
+  smul := λ k v, quotient.lift_on v
+    (λ v, ⟦has_scalar.smul k v⟧)
+    $ λ _ _ H, quotient.sound
+    $ begin
+      change _ ∈ _,
+      rw ← smul_sub,
+      refine subalgebra.smul_mem _ H _,
+    end}
+
+-- exercises left to reader...
+instance : ring (clifford_algebra Q) := {
+  zero := ⟦0⟧,
+  add := quotient.map₂ (+) (λ a a' ha b b' hb, begin
+    change _ ∈ _,
+    convert subalgebra.add_mem _ ha hb using 1,
+    abel,
+  end),
+  neg := quotient.map (has_neg.neg) (λ a a' ha, begin
+    change _ ∈ _,
+    convert subalgebra.neg_mem _ ha,
+    abel,
+  end),
+  -- these are very tedious
+  add_assoc := by {
+    rintros ⟨⟩ ⟨⟩ ⟨⟩,
+    change quotient.mk _ = quotient.mk _,
+    apply quotient.sound,
+    change _ ∈ _,
+    simp only [add_assoc, sub_self],
+    exact subalgebra.zero_mem _,
+  },
+  zero_add := by {
+    rintros ⟨⟩,
+    change quotient.mk _ = quotient.mk _,
+    apply quotient.sound,
+    change _ ∈ _,
+    simp only [zero_add, sub_self],
+    exact subalgebra.zero_mem _,
+  },
+  add_zero := by {
+    rintros ⟨⟩,
+    change quotient.mk _ = quotient.mk _,
+    apply quotient.sound,
+    change _ ∈ _,
+    simp only [add_zero, sub_self],
+    exact subalgebra.zero_mem _,
+  },
+  add_left_neg := by {
+    rintros ⟨⟩,
+    change quotient.mk _ = quotient.mk _,
+    apply quotient.sound,
+    change _ ∈ _,
+    simp only [add_left_neg, sub_self],
+    exact subalgebra.zero_mem _,
+  },
+  add_comm := by {
+    rintros ⟨⟩ ⟨⟩,
+    change quotient.mk _ = quotient.mk _,
+    apply quotient.sound,
+    change _ ∈ _,
+    simp only [add_comm, sub_self],
+    exact subalgebra.zero_mem _,
+  },
+
+  -- this stuff doesn't seem possible yet
+  one := ⟦1⟧,
+  mul := quotient.map₂ (*) (λ a a' ha b b' hb, begin
+    change _ ∈ _,
+    change _ ∈ _ at ha,
+    change _ ∈ _ at hb,
+    have h := subalgebra.mul_mem _ ha hb,
+    simp only [mul_sub, sub_mul] at h,
+    sorry,
+    -- this looks unprovable
+  end),
+  mul_assoc := by {
+    rintros ⟨⟩ ⟨⟩ ⟨⟩,
+    change quotient.mk _ = quotient.mk _,
+    apply quotient.sound,
+    change _ ∈ _,
+    sorry
+  },
+  one_mul := by {
+    rintros ⟨⟩,
+    change quotient.mk _ = quotient.mk _,
+    apply quotient.sound,
+    change _ ∈ _,
+    sorry
+  },
+  mul_one := by {
+    rintros ⟨⟩,
+    change quotient.mk _ = quotient.mk _,
+    apply quotient.sound,
+    change _ ∈ _,
+    sorry
+  },
+  left_distrib := by {
+    rintros ⟨⟩ ⟨⟩ ⟨⟩,
+    change quotient.mk _ = quotient.mk _,
+    apply quotient.sound,
+    change _ ∈ _,
+    sorry
+  },
+  right_distrib := by {
+    rintros ⟨⟩ ⟨⟩ ⟨⟩,
+    change quotient.mk _ = quotient.mk _,
+    apply quotient.sound,
+    change _ ∈ _,
+    sorry
+  }}
+
+instance : algebra R (clifford_algebra Q) := {
+  to_fun := λ r, ⟦algebra_map R (pre Q) r⟧,
+  map_one' := sorry,
+  map_mul' := sorry,
+  map_zero' := sorry,
+  map_add' := sorry,
+  commutes' := sorry,
+  smul_def' := sorry }
+
+-- lemma vector_square_scalar
+
+end clifford_algebra

src/geometric_algebra/nursery/talk.lean

@@ -7,6 +7,9 @@ universe u
 
 variables (α : Type u)
 
+/--
+Groups defined three ways
+-/
 namespace Group
 
 namespace extends_has
@@ -51,6 +54,9 @@ end in_real_lean
 
 end Group
 
+/--
+An example of a proof
+-/
 namespace proof_demo
 open int
 
@@ -78,6 +84,8 @@ show a = b, from
 end
 end proof_demo
 
+
+/-- An example of geometric algebra -/
 namespace GA
 
 namespace first
@@ -86,49 +94,54 @@ variables (K : Type u) [field K]
 
 variables (V : Type u) [add_comm_group V] [vector_space K V]
 
-structure GA
-(G : Type u)
-[ring G] extends algebra K G :=
+#print linear_map
+
+def sqr {α : Type u} [has_mul α] (x : α) := x*x
+local postfix `²`:80 := sqr
+
+structure GA (G : Type u) [ring G] [algebra K G] :=
 (fₛ : K →+* G)
-(fᵥ : V →+ G)
+(fᵥ : V →ₗ[K] G)
 -- (infix ` ❍ `:70 := has_mul.mul)
-(postfix `²`:80 := λ x, x * x)
 (contraction : ∀ v : V, ∃ k : K, (fᵥ v)² = fₛ k)
 
 -- local infix ` ❍ `:70 := has_mul.mul
-local postfix `²`:80 := λ x, x * x
 
 /-
   Symmetrised product of two vectors must be a scalar
 -/
 example
-(G : Type u) [ring G] [ga : GA K V G] :
+(G : Type u) [ring G] [algebra K G] [ga : GA K V G] :
 ∀ aᵥ bᵥ : V, ∃ kₛ : K,
-let a := ga.fᵥ aᵥ, b := ga.fᵥ bᵥ, k := ga.fₛ kₛ in
-a * b + b * a = k :=
+  let a := ga.fᵥ aᵥ, b := ga.fᵥ bᵥ, k := ga.fₛ kₛ in
+    a * b + b * a = k :=
 begin
   assume aᵥ bᵥ,
-  let a := ga.fᵥ aᵥ, 
-  let b := ga.fᵥ bᵥ,
-  have h1 : (a + b)² = a * b + b * a + a² + b², from begin
-    dsimp,
-    rw left_distrib,
-    repeat {rw right_distrib},
-    abel,
-  end,
-  obtain ⟨kabₛ, hab⟩ := GA.contraction ga (aᵥ + bᵥ),
-  obtain ⟨kaₛ, ha⟩ := GA.contraction ga (aᵥ),
-  obtain ⟨kbₛ, hb⟩ := GA.contraction ga (bᵥ),
-  have h2 : ga.fₛ (kabₛ - kaₛ - kbₛ) = a * b + b * a, by {
-    repeat {rw ring_hom.map_sub},
-    apply_fun (λ x, x - b * b - a * a) at h1,
-    simp [] at h1 ha hb hab,
-    simp [←h1, ha, hb, hab],
+  -- some tricks to unfold the `let`s and make things look tidy
+  delta,
+  set a := ga.fᵥ aᵥ,
+  set b := ga.fᵥ bᵥ,
+
+  -- collect square terms
+  rw (show a * b + b * a = (a + b)² - a² - b², from begin
+    unfold sqr,
+    simp only [left_distrib, right_distrib],
     abel,
-  },
+  end),
+
+  -- replace them with a scalar using the ga axiom
+  obtain ⟨kabₛ, hab⟩ := ga.contraction (aᵥ + bᵥ),
+  obtain ⟨kaₛ, ha⟩ := ga.contraction (aᵥ),
+  obtain ⟨kbₛ, hb⟩ := ga.contraction (bᵥ),
+  rw [
+    show (a + b)² = ga.fₛ kabₛ, by rw [← hab, linear_map.map_add],
+    show a² = ga.fₛ kaₛ, by rw ha,
+    show b² = ga.fₛ kbₛ, by rw hb
+  ],
+
+  -- rearrange, solve by inspection
+  simp only [← ring_hom.map_sub],
   use kabₛ - kaₛ - kbₛ,
-  rw h2,
-  abel,
 end
 
 end first