From 98a41b9307b860e1cf81f71b16abe3ad468e8f78 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 28 Jul 2020 18:52:29 +0100 Subject: [PATCH 1/3] Alternate proof formulation, maybe more readable? --- src/geometric_algebra/nursery/talk.lean | 69 +++++++++++++++---------- 1 file changed, 41 insertions(+), 28 deletions(-) diff --git a/src/geometric_algebra/nursery/talk.lean b/src/geometric_algebra/nursery/talk.lean index 4a7c987ae..5daeb01e2 100644 --- a/src/geometric_algebra/nursery/talk.lean +++ b/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 From 145364c602057270617309941b2f29e4c01914e1 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 29 Jul 2020 15:23:23 +0100 Subject: [PATCH 2/3] tensor_algebra from upstream mathlib --- .../nursery/tensor_algebra.lean | 387 ++++++++++++++++++ 1 file changed, 387 insertions(+) create mode 100644 src/geometric_algebra/nursery/tensor_algebra.lean diff --git a/src/geometric_algebra/nursery/tensor_algebra.lean b/src/geometric_algebra/nursery/tensor_algebra.lean new file mode 100644 index 000000000..8aa73430c --- /dev/null +++ b/src/geometric_algebra/nursery/tensor_algebra.lean @@ -0,0 +1,387 @@ +/- +Copyright (c) 2020 Adam Topaz. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Adam Topaz. +-/ + +import ring_theory.algebra +import linear_algebra + +/-! +# Tensor Algebras + +Given a commutative semiring R, and an R-module M, we construct the tensor algebra of M. +This is the free R-algebra generated by the module M. + +## Notation + +1. `tensor_algebra R M` is the tensor algebra itself. + It is endowed with an R-algebra structure. +2. `univ R M` is the R-linear map `M → tensor_algebra R M`. +3. Given a linear map `f : M → A` to an R-algebra A, + `lift R M f` is the lift of `f` to an R-algebra morphism + `tensor_algebra R M → A`. + +## Theorems + +1. `univ_comp_lift` states that the composition + `(lift R M f) ∘ (univ R M)` is identical to `f`. +2. `lift_unique` states that whenever an R-algebra morphism + `g : tensor_algebra R M → A` is given whose composision with `univ R M` is `f`, + then one has `g = lift R M f`. +-/ + +universes u1 u2 u3 u4 + +variables (R : Type u1) [comm_semiring R] +variables (M : Type u2) [add_comm_group M] [semimodule R M] + +namespace tensor_algebra + +/-- +This inductive type is used to express representatives +of the tensor algebra. +-/ +inductive pre +| of : M → pre +| of_scalar : R → pre +| add : pre → pre → pre +| mul : pre → pre → pre + +namespace pre + +instance : inhabited (pre R M) := ⟨of_scalar 0⟩ + +-- Note: These instances are only used to simplify the notation. +/-- Coercion from `M` to `pre R M`. Note: Used for notation only. -/ +def has_coe_module : has_coe M (pre R M) := ⟨of⟩ +/-- Coercion from `R` to `pre R M`. Note: Used for notation only. -/ +def has_coe_semiring : has_coe R (pre R M) := ⟨of_scalar⟩ +/-- Multiplication in `pre R M` defined as `pre.mul`. Note: Used for notation only. -/ +def has_mul : has_mul (pre R M) := ⟨mul⟩ +/-- Addition in `pre R M` defined as `pre.add`. Note: Used for notation only. -/ +def has_add : has_add (pre R M) := ⟨add⟩ +/-- Zero in `pre R M` defined as the image of `0` from `R`. Note: Used for notation only. -/ +def has_zero : has_zero (pre R M) := ⟨of_scalar 0⟩ +/-- One in `pre R M` defined as the image of `1` from `R`. Note: Used for notation only. -/ +def has_one : has_one (pre R M) := ⟨of_scalar 1⟩ +/-- +Scalar multiplication defined as multiplication by the image +of elements from `R`. +Note: Used for notation only. +-/ +def has_scalar : has_scalar R (pre R M) := ⟨λ r m, mul (of_scalar r) m⟩ + +end pre + +local attribute [instance] + pre.has_coe_module pre.has_coe_semiring pre.has_mul pre.has_add pre.has_zero + pre.has_one pre.has_scalar + +/-- +Given a linear map from `M` to an `R`-algebra `A`, `lift_fun` provides +a lift of `f` to a function from `pre R M` to `A`. +This is mainly used in the construction of `tensor_algebra.lift` below. +-/ +def lift_fun {A : Type u3} [semiring A] [algebra R A] (f : M →ₗ[R] A) : pre R M → A +| (pre.of m) := f m +| (pre.of_scalar r) := (algebra_map _ _) r +| (pre.add a b) := lift_fun a + lift_fun b +| (pre.mul a b) := lift_fun a * lift_fun b + -- λ t, pre.rec_on t f (algebra_map _ _) (λ _ _, (+)) (λ _ _, (*)) + +/-- +An inductively defined relation on `pre R M` +used to force the initial algebra structure on the associated quotient. +-/ +inductive rel : (pre R M) → (pre R M) → Prop +-- force `of` to be linear +| add_lin {a b : M} : rel ↑(a+b) (↑a + ↑b) +| smul_lin {r : R} {a : M} : rel ↑(r • a) (↑r * ↑a) +-- force `of_scalar` to be a central semiring morphism +| add_scalar {r s : R} : rel ↑(r + s) (↑r + ↑s) +| mul_scalar {r s : R} : rel ↑(r * s) (↑r * ↑s) +| central_scalar {r : R} {a : pre R M} : rel (r * a) (a * r) +-- commutative additive semigroup +| add_assoc {a b c : pre R M} : rel (a + b + c) (a + (b + c)) +| add_comm {a b : pre R M} : rel (a + b) (b + a) +| zero_add {a : pre R M} : rel (0 + a) a +-- multiplicative monoid +| mul_assoc {a b c : pre R M} : rel (a * b * c) (a * (b * c)) +| one_mul {a : pre R M} : rel (1 * a) a +| mul_one {a : pre R M} : rel (a * 1) a +-- distributivity +| left_distrib {a b c : pre R M} : rel (a * (b + c)) (a * b + a * c) +| right_distrib {a b c : pre R M} : rel ((a + b) * c) (a * c + b * c) +-- other relations needed for semiring +| zero_mul {a : pre R M} : rel (0 * a) 0 +| mul_zero {a : pre R M} : rel (a * 0) 0 +-- compatibility +| add_compat_left {a b c : pre R M} : rel a b → rel (a + c) (b + c) +| add_compat_right {a b c : pre R M} : rel a b → rel (c + a) (c + b) +| mul_compat_left {a b c : pre R M} : rel a b → rel (a * c) (b * c) +| mul_compat_right {a b c : pre R M} : rel a b → rel (c * a) (c * b) + +end tensor_algebra + +/-- +The tensor algebra of the module `M` over the commutative semiring `R`. +-/ +def tensor_algebra := quot (tensor_algebra.rel R M) + + +class tensor_algebra_class + (T : Type u3) [semiring T] extends algebra R T := +(to_fun' : M →ₗ[R] T) +(lifted : ℕ) +(lift : Π {A : Type u4} [semiring A] [algebra R A], (M →ₗ[R] A) → (T →ₐ[R] A)) + +#check tensor_algebra_class + +namespace tensor_algebra + +local attribute [instance] + pre.has_coe_module pre.has_coe_semiring pre.has_mul pre.has_add pre.has_zero + pre.has_one pre.has_scalar + +instance : semiring (tensor_algebra R M) := +{ add := λ a b, quot.lift_on a (λ x, quot.lift_on b (λ y, quot.mk (rel R M) (x + y)) + begin + intros a b h, + dsimp only [], + apply quot.sound, + apply rel.add_compat_right h, + end) + begin + intros a b h, + dsimp only [], + congr, + ext, + apply quot.sound, + apply rel.add_compat_left h, + end, + add_assoc := λ a b c, + begin + rcases quot.exists_rep a with ⟨a,rfl⟩, + rcases quot.exists_rep b with ⟨b,rfl⟩, + rcases quot.exists_rep c with ⟨c,rfl⟩, + apply quot.sound, + apply rel.add_assoc, + end, + zero := quot.mk _ 0, + zero_add := λ a, + begin + rcases quot.exists_rep a with ⟨a,rfl⟩, + apply quot.sound, + apply rel.zero_add, + end, + add_zero := λ a, + begin + rcases quot.exists_rep a with ⟨a,rfl⟩, + change quot.mk _ _ = _, + rw quot.sound rel.add_comm, + apply quot.sound, + apply rel.zero_add, + end, + add_comm := λ a b, + begin + rcases quot.exists_rep a with ⟨a,rfl⟩, + rcases quot.exists_rep b with ⟨b,rfl⟩, + apply quot.sound, + apply rel.add_comm, + end, + mul := λ a b, quot.lift_on a (λ x, quot.lift_on b (λ y, quot.mk _ (x * y)) + begin + intros a b h, + dsimp only [], + apply quot.sound, + apply rel.mul_compat_right h, + end) + begin + intros a b h, + dsimp only [], + congr, + ext, + apply quot.sound, + apply rel.mul_compat_left h, + end, + mul_assoc := λ a b c, + begin + rcases quot.exists_rep a with ⟨a,rfl⟩, + rcases quot.exists_rep b with ⟨b,rfl⟩, + rcases quot.exists_rep c with ⟨c,rfl⟩, + apply quot.sound, + apply rel.mul_assoc, + end, + one := quot.mk _ 1, + one_mul := λ a, + begin + rcases quot.exists_rep a with ⟨a,rfl⟩, + apply quot.sound, + apply rel.one_mul, + end, + mul_one := λ a, + begin + rcases quot.exists_rep a with ⟨a,rfl⟩, + apply quot.sound, + apply rel.mul_one, + end, + left_distrib := λ a b c, + begin + rcases quot.exists_rep a with ⟨a,rfl⟩, + rcases quot.exists_rep b with ⟨b,rfl⟩, + rcases quot.exists_rep c with ⟨c,rfl⟩, + apply quot.sound, + apply rel.left_distrib, + end, + right_distrib := λ a b c, + begin + rcases quot.exists_rep a with ⟨a,rfl⟩, + rcases quot.exists_rep b with ⟨b,rfl⟩, + rcases quot.exists_rep c with ⟨c,rfl⟩, + apply quot.sound, + apply rel.right_distrib, + end, + zero_mul := λ a, + begin + rcases quot.exists_rep a with ⟨a,rfl⟩, + apply quot.sound, + apply rel.zero_mul, + end, + mul_zero := λ a, + begin + rcases quot.exists_rep a with ⟨a,rfl⟩, + apply quot.sound, + apply rel.mul_zero, + end } + +instance : inhabited (tensor_algebra R M) := ⟨0⟩ + +instance : has_scalar R (tensor_algebra R M) := +{ smul := λ r a, quot.lift_on a (λ x, quot.mk _ $ ↑r * x) +begin + intros a b h, + dsimp only [], + apply quot.sound, + apply rel.mul_compat_right h, +end } + +instance : algebra R (tensor_algebra R M) := +{ to_fun := λ r, quot.mk _ ↑r, + map_one' := rfl, + map_mul' := λ a b, by apply quot.sound; apply rel.mul_scalar, + map_zero' := rfl, + map_add' := λ a b, by apply quot.sound; apply rel.add_scalar, + commutes' := λ r x, + begin + dsimp only [], + rcases quot.exists_rep x with ⟨x,rfl⟩, + apply quot.sound, + apply rel.central_scalar, + end, + smul_def' := λ r x, by refl } + +/-- +The universal linear map `M →ₗ[R] tensor_algebra R M`. +-/ +def univ : M →ₗ[R] (tensor_algebra R M) := +{ to_fun := λ m, quot.mk _ m, + map_add' := λ x y, by apply quot.sound; apply rel.add_lin, + map_smul' := λ r x, by apply quot.sound; apply rel.smul_lin } + +#print alg_hom + +/-- +Given a linear map `f : M → A` where `A` is an `R`-algebra, +`lift R M f` is the unique lift of `f` to a morphism of `R`-algebras +`tensor_algebra R M → A`. +-/ +def lift {A : Type u3} [semiring A] [algebra R A] (f : M →ₗ[R] A) : tensor_algebra R M →ₐ[R] A := +{ to_fun := λ a, quot.lift_on a (lift_fun _ _ f) $ λ a b h, + begin + induction h, + { change f _ = f _ + f _, simp, }, + { change f _ = (algebra_map _ _ _) * f _, rw linear_map.map_smul, + exact algebra.smul_def h_r (f h_a) }, + { change algebra_map _ _ _ = algebra_map _ _ _ + algebra_map _ _ _, + exact (algebra_map R A).map_add h_r h_s }, + { change algebra_map _ _ _ = algebra_map _ _ _ * algebra_map _ _ _, + exact (algebra_map R A).map_mul h_r h_s }, + { let G := lift_fun R M f, + change (algebra_map _ _ _) * G _ = G _, + exact algebra.commutes h_r (G h_a) }, + { change _ + _ + _ = _ + (_ + _), rw add_assoc }, + { change _ + _ = _ + _, rw add_comm, }, + { let G := lift_fun R M f, + change (algebra_map _ _ _) + G _ = G _, simp, }, + { change _ * _ * _ = _ * (_ * _), rw mul_assoc }, + { let G := lift_fun R M f, + change (algebra_map _ _ _) * G _ = G _, simp, }, + { let G := lift_fun R M f, + change G _ * (algebra_map _ _ _)= G _, simp, }, + { change _ * (_ + _) = _ * _ + _ * _, rw left_distrib, }, + { change (_ + _) * _ = _ * _ + _ * _, rw right_distrib, }, + repeat { set G := lift_fun R M f, + change G _ + G _ = G _ + G _, rw h_ih, }, + repeat { set G := lift_fun R M f, + change G _ * G _ = G _ * G _, rw h_ih, }, + { change (algebra_map _ _ _) * _ = algebra_map _ _ _, simp }, + { change _ * (algebra_map _ _ _) = algebra_map _ _ _, simp }, + end, + map_one' := by change algebra_map _ _ _ = _; simp, + map_mul' := + begin + intros x y, + rcases quot.exists_rep x with ⟨x,rfl⟩, + rcases quot.exists_rep y with ⟨y,rfl⟩, + refl, + end, + map_zero' := by change algebra_map _ _ _ = _; simp, + map_add' := + begin + intros x y, + rcases quot.exists_rep x with ⟨x,rfl⟩, + rcases quot.exists_rep y with ⟨y,rfl⟩, + refl, + end, + commutes' := by tauto } + +variables {R M} + +theorem univ_comp_lift {A : Type u3} [semiring A] [algebra R A] (f : M →ₗ[R] A) : + (lift R M f).to_linear_map.comp (univ R M) = f := by {ext, refl} + +theorem lift_unique {A : Type u3} [semiring A] [algebra R A] (f : M →ₗ[R] A) + (g : tensor_algebra R M →ₐ[R] A) : g.to_linear_map.comp (univ R M) = f → g = lift R M f := +begin + intro hyp, + ext, + rcases quot.exists_rep x with ⟨x,rfl⟩, + let G := lift_fun R M f, + induction x, + { change (g.to_linear_map.comp (univ R M)) _ = _, + rw hyp, refl }, + { change g (algebra_map R _ _) = algebra_map _ _ _, + exact alg_hom.commutes g x }, + { change g (quot.mk _ x_a + quot.mk _ x_a_1) = _, + rw alg_hom.map_add, + rw x_ih_a, rw x_ih_a_1, + refl }, + { change g (quot.mk _ x_a * quot.mk _ x_a_1) = _, + rw alg_hom.map_mul, + rw x_ih_a, rw x_ih_a_1, + refl }, +end + +theorem hom_ext {A : Type u3} [semiring A] [algebra R A] {f g : tensor_algebra R M →ₐ[R] A} : + f.to_linear_map.comp (univ R M) = g.to_linear_map.comp (univ R M) → f = g := +begin + intro hyp, + let h := f.to_linear_map.comp (univ R M), + have : f = lift R M h, by apply lift_unique; refl, + rw this, clear this, + symmetry, apply lift_unique, + rw ←hyp, +end + +end tensor_algebra \ No newline at end of file From ca288b1b7b81cea309b94121e30517618a062200 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 29 Jul 2020 18:59:21 +0100 Subject: [PATCH 3/3] Add an attempt at a clifford algebra via a quotient --- .../nursery/quotient_of_tensor.lean | 202 ++++++++++++++++++ .../nursery/tensor_algebra.lean | 12 +- .../nursery/tensor_algebra_ring.lean | 22 ++ 3 files changed, 230 insertions(+), 6 deletions(-) create mode 100644 src/geometric_algebra/nursery/quotient_of_tensor.lean create mode 100644 src/geometric_algebra/nursery/tensor_algebra_ring.lean diff --git a/src/geometric_algebra/nursery/quotient_of_tensor.lean b/src/geometric_algebra/nursery/quotient_of_tensor.lean new file mode 100644 index 000000000..d0f90d1a9 --- /dev/null +++ b/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 diff --git a/src/geometric_algebra/nursery/tensor_algebra.lean b/src/geometric_algebra/nursery/tensor_algebra.lean index 8aa73430c..2379f9872 100644 --- a/src/geometric_algebra/nursery/tensor_algebra.lean +++ b/src/geometric_algebra/nursery/tensor_algebra.lean @@ -130,13 +130,13 @@ The tensor algebra of the module `M` over the commutative semiring `R`. def tensor_algebra := quot (tensor_algebra.rel R M) -class tensor_algebra_class - (T : Type u3) [semiring T] extends algebra R T := -(to_fun' : M →ₗ[R] T) -(lifted : ℕ) -(lift : Π {A : Type u4} [semiring A] [algebra R A], (M →ₗ[R] A) → (T →ₐ[R] A)) +-- class tensor_algebra_class +-- (T : Type u3) [semiring T] extends algebra R T := +-- (to_fun' : M →ₗ[R] T) +-- (lifted : ℕ) +-- (lift : Π {A : Type u4} [semiring A] [algebra R A], (M →ₗ[R] A) → (T →ₐ[R] A)) -#check tensor_algebra_class +-- #check tensor_algebra_class namespace tensor_algebra diff --git a/src/geometric_algebra/nursery/tensor_algebra_ring.lean b/src/geometric_algebra/nursery/tensor_algebra_ring.lean new file mode 100644 index 000000000..dc32691a8 --- /dev/null +++ b/src/geometric_algebra/nursery/tensor_algebra_ring.lean @@ -0,0 +1,22 @@ +import geometric_algebra.nursery.tensor_algebra + +namespace tensor_algebra + +universes u v +variables (R : Type u) [comm_ring R] +variables (M : Type v) [add_comm_group M] [module R M] + +-- from https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/semiring.2Balgebra.20.3D.3E.20ring/near/204968473 +instance : ring (tensor_algebra R M) := +{ neg := λ a, (algebra_map R _ $ -1) * a, + add_left_neg := λ a, + begin + have : (algebra_map R _ 1) * a = a, by simp, + conv_lhs { congr, skip, rw ←this}, clear this, + change (algebra_map R _ (-1)) * a + _ = _, + rw [←right_distrib,← (algebra_map R _).map_add (-1) 1], + simp, + end, + ..show semiring _, by apply_instance } + +end tensor_algebra \ No newline at end of file