From 664502246ef2107833fa7af73562360c4c48cbbb Mon Sep 17 00:00:00 2001 From: utensil Date: Sun, 12 Jul 2020 18:49:25 +0800 Subject: [PATCH 01/22] Draft the doc for new design --- docs/misc/new_design.md | 169 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 169 insertions(+) create mode 100644 docs/misc/new_design.md diff --git a/docs/misc/new_design.md b/docs/misc/new_design.md new file mode 100644 index 000000000..aac8ca16b --- /dev/null +++ b/docs/misc/new_design.md @@ -0,0 +1,169 @@ +# Rethinking the Design of Mathematical Theory Development in Lean + +It turns out that we must have a design template in mind in order to carry on further designing of GA in Lean. This document will address this issue. + +## Key Insight from Euclidean Geometry + +Taking a step back, let's go back to geometry and look at https://github.com/vaibhavkarve/leanteach2020/blob/master/src/euclid.lean . + +What's a point? How do we tell this concept to the computer? Do we draw a point? Or do we went to analytic geometry and give it a coordinate? It turns out we don't need to do either, the former is infeasible and the latter is the worst idea in formalizing. + +```lean +constant Point : Type +``` + +How about a line? Same. + +```lean +constant Line : Type +``` + +How about the relations between points and lines? + +```lean +constant lies_on : Point → Line → Prop +constant between : Point → Point → Point → Prop -- (between a b c) means "b is in between a and c" +constant congruent {A : Type} : A → A → Prop +constant distance : Point → Point → ℝ +``` + +How about axioms? + +```lean +axiom distance_not_neg {p1 p2 : Point} : 0 ≤ distance p1 p2 +axiom distance_pos {p1 p2 : Point} : p1 ≠ p2 ↔ 0 < distance p1 p2 +``` + +And this keeps on and on. Then we have a lot of lemmas and theorems and we still don't need to know what exactly a point is, we don't even need to know how to compute a distance. + +That's it. We don't need concrete types or computibility to reason about them. The semantic can end with their names and we don't need to know more underneath. + +This is the key insight one must have before formalizing a piece of mathematics. + +## Compatibility with mathlib + +A geometric product "contains" an inner product and an exterior product (or wedge product). + +They're established mathematic. There's already inner product space in mathlib and there would definitely be Grassmann Algebra in mathlib one day. And obviously we can't escape the general Clifford Algebra too. + +We must maintain compatibility with them, at least don't conflict with their existence. + +It's not a duplication. The development of mathlib is driven by professional mathematitians, they struggle for math generity but we're working at an abstraction level close to applications. + +We want to stand on such shoulders but we want good capsulation so that we don't want to worry about more abstract concepts and some too general cases. This would definitely leak, it might not be obvious in definitions but it would be very clear when you're proving something. For example, you have to deal with lattice and finsupp when proving things about linear algebra, and that should not be. + +## Operators + +We start with has_* that have absolutely no axioms with them, they don't have any properties and any behaviors. It's almost just a name. And we associate notations with them. + +Just like in https://github.com/leanprover-community/lean/blob/master/library/init/core.lean#L321 + +```lean +class has_mul (α : Type u) := (mul : α → α → α) +``` + +we could just: + +```lean +class has_wedge (α : Type u) := (wedge : α → α → α) +class has_inner (α : Type u) := (inner : α → α → α) +``` + +The latter presumably is already in mathlib and has a lot of structures and properties associated with it. We'll deal with that later. + +As for geometric product, I'm thinking about the following short name instead of `geomprod`, `gp` etc.: + +``` +class has_gmul (α : Type u) := (gmul : α → α → α) +``` + +## Notations + +Now we assoc notations with them: + +```lean +-- \circ +infix ∘ := has_gmul.gmul +-- \wedge +infix ∧ := has_wedge.wedge +-- \cdot +infix ⋅ := has_inner.inner +``` + +We'll always use `local` notations waiting for to be `open_locale`ed. I expect conflicts with notations in mathlib and using this to avoid the conflicts as long as possible. + +> TODO: describe how to use them even when there's a confliction. + +## Defining without defining + +There're really millions of products defined in GA and they're based on geometric product. But the definition might not be the most effient one or the most intuitive one. + +So instead of using `def`, we should make these products just a product with a Prop assering that they're equal to the definition based on gp and let the implementation prove it when intantiate the instance. + +```lean +class has_ga_wedge (α : Type u) extends has_wedge := +(defeq : ∀ a b : α, a ∧ b = (a ∘ b - b ∘ a) / 2) +``` + +The above ignore the fact this only works on vectors instead of multivectors. + +So the true story is that we should define `has_sym_mul` and `has_asym_mul` first. + +## The complication with mul + +mul group diamond + +C wrong + +## ga extends has_gmul + +## ga vs mv + +## the standard template + +import universe open variables + +class with parameter + +bundle + +prio + +marker forgetful_to + +directory structure + +## defs and lemmas + +contains no lemma except for ... see groups/defs.lean + +recover the usual for demo but never use them + +## R V are not G0 G1 + +## G is vector space + +## linear map + +no `:G` or `coe` + +## vector_contractible + +non-metric + +quadratic form? + +functional? + +induced topology + +## attr + +## universal algebra + +## what to inherit and forget? + +## Clifford and Grassmann + +## graded comes later + From 27edad5997dd7cb82a0c00534ae57ba152b21acd Mon Sep 17 00:00:00 2001 From: utensil Date: Mon, 13 Jul 2020 01:25:41 +0800 Subject: [PATCH 02/22] Add inspirations.lean --- .../generic/inspirations.lean | 33 +++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 src/geometric_algebra/generic/inspirations.lean diff --git a/src/geometric_algebra/generic/inspirations.lean b/src/geometric_algebra/generic/inspirations.lean new file mode 100644 index 000000000..a7a6e6794 --- /dev/null +++ b/src/geometric_algebra/generic/inspirations.lean @@ -0,0 +1,33 @@ +/- +Copyright (c) 2020 lean-ga Team. All rights reserved. +Released under MIT license as described in the file LICENSE. +Authors: Utensil Song + +This file contains only imports which are just the lean files +that the authors draw inspirations from. +-/ +import init.core + +import algebra.group.defs +import algebra.group.hom +import algebra.module +import algebra.direct_limit +import ring_theory.algebra +import linear_algebra.quadratic_form + +import data.real.basic +import data.complex.basic +import data.complex.module +import data.matrix.basic + +import geometry.euclidean +import geometry.manifold.real_instances + +import analysis.convex.cone +import analysis.normed_space.basic +import analysis.normed_space.real_inner_product + +import tactic +import tactic.lint + +#lint \ No newline at end of file From f692a3e80a4b0c8677dd417ad7d6a2d2447c3e8b Mon Sep 17 00:00:00 2001 From: utensil Date: Mon, 13 Jul 2020 01:26:20 +0800 Subject: [PATCH 03/22] Add operatrors.lean --- src/geometric_algebra/generic/operators.lean | 51 ++++++++++++++++++++ 1 file changed, 51 insertions(+) create mode 100644 src/geometric_algebra/generic/operators.lean diff --git a/src/geometric_algebra/generic/operators.lean b/src/geometric_algebra/generic/operators.lean new file mode 100644 index 000000000..e8cfe6b91 --- /dev/null +++ b/src/geometric_algebra/generic/operators.lean @@ -0,0 +1,51 @@ +/- +Copyright (c) 2020 lean-ga Team. All rights reserved. +Released under MIT license as described in the file LICENSE. +Authors: Utensil Song + +This file defines operators with local notations and no axioms. +-/ +import tactic.lint + +universes u + +namespace geometric_algebra + +class has_dot (α : Type u) := (dot : α → α → α) +class has_wedge (α : Type u) := (wedge : α → α → α) + +-- class has_geom_prod (α : Type u) := (geom_prod : α → α → α) + +class has_scalar_prod (α : Type u) := (scalar_prod : α → α → α) + +class has_symm_prod (α : Type u) := (symm_prod : α → α → α) +class has_asymm_prod (α : Type u) := (asymm_prod : α → α → α) + +class has_left_contract (α : Type u) := (left_contract : α → α → α) +class has_right_contract (α : Type u) := (right_contract : α → α → α) + +-- export has_dot (dot) +-- export has_wedge (wedge) + +local infix ⬝ := has_dot.dot +local infix ∧ := has_wedge.wedge + +-- local infix ∘ := has_geom_prod.geom_prod + +reserve infix ` ⊛ `:70 +local infix ` ⊛ ` := has_scalar_prod.scalar_prod + +reserve infix ` ⊙ `:70 +reserve infix ` ⊠ `:70 +local infix ` ⊙ ` := has_symm_prod.symm_prod +local infix ` ⊠ ` := has_asymm_prod.asymm_prod + +reserve infix ` ⨼ `:70 +reserve infix ` ⨽ `:70 +local infix ⨼ := has_left_contract.left_contract +local infix ⨽ := has_right_contract.right_contract + +end geometric_algebra + +#lint + From 1ef4437e3075d0e3cf59c5b1a4458c8aa029eb9e Mon Sep 17 00:00:00 2001 From: utensil Date: Mon, 13 Jul 2020 01:26:33 +0800 Subject: [PATCH 04/22] Add defs.lean --- src/geometric_algebra/generic/defs.lean | 67 +++++++++++++++++++++++++ 1 file changed, 67 insertions(+) create mode 100644 src/geometric_algebra/generic/defs.lean diff --git a/src/geometric_algebra/generic/defs.lean b/src/geometric_algebra/generic/defs.lean new file mode 100644 index 000000000..16adc33d3 --- /dev/null +++ b/src/geometric_algebra/generic/defs.lean @@ -0,0 +1,67 @@ +/- +Copyright (c) 2020 lean-ga Team. All rights reserved. +Released under MIT license as described in the file LICENRE. +Authors: Utensil Rong +-/ +import ring_theory.algebra +import linear_algebra.quadratic_form +import tactic +import tactic.lint + +-- import geometric_algebra.generic.operators + +universes ur uv ug + +variables {R : Type ur} [field R] +variables {V : Type uv} [add_comm_group V] [vector_space R V] +variables {G : Type ug} [ring G] + +section prio +-- set_option default_priority 200 -- see Note [default priority] +set_option default_priority 100 +set_option old_structure_cmd true + +/-- +-/ +@[ancestor algebra] +class semi_geometric_algebra +(R : Type ur) [field R] +(V : Type uv) [add_comm_group V] [vector_space R V] +(G : Type ug) [ring G] +extends algebra R G + +class weak_geometric_algebra +(R : Type ur) [field R] +(V : Type uv) [add_comm_group V] [vector_space R V] +(G : Type ug) [ring G] +extends semi_geometric_algebra R V G +:= +(fᵣ : R →+* G) +-- this follows normed_algebra in analysis.normed_space.basic +(fᵣ_algebra_map_eq : fᵣ = algebra_map R G) +(fᵥ : V →+ G) +-- this is the weaker form of the contraction rule for vectors +(vector_contract' : ∀ v, ∃ r, fᵥ v * fᵥ v = fᵣ r ) + +class geometric_algebra +(R : Type ur) [field R] +(V : Type uv) [add_comm_group V] [vector_space R V] +(G : Type ug) [ring G] +extends weak_geometric_algebra R V G +:= +(q : quadratic_form R V) +(vector_contract : ∀ v, fᵥ v * fᵥ v = fᵣ (q v) ) + +end prio + +-- #print geometric_algebra + +namespace geometric_algebra + +variables [geometric_algebra R V G] + +-- instance : inhabited (geometric_algebra R V G) := ⟨0⟩ + +end geometric_algebra + +#lint \ No newline at end of file From 456a95ead58951ca076420dc492ddee3d829dc0d Mon Sep 17 00:00:00 2001 From: Utensil Song Date: Mon, 13 Jul 2020 09:52:56 +0800 Subject: [PATCH 05/22] Fix typos found in review Co-authored-by: Eric Wieser --- docs/misc/new_design.md | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/docs/misc/new_design.md b/docs/misc/new_design.md index aac8ca16b..d430fb5d6 100644 --- a/docs/misc/new_design.md +++ b/docs/misc/new_design.md @@ -73,7 +73,7 @@ The latter presumably is already in mathlib and has a lot of structures and prop As for geometric product, I'm thinking about the following short name instead of `geomprod`, `gp` etc.: -``` +```lean class has_gmul (α : Type u) := (gmul : α → α → α) ``` @@ -96,9 +96,9 @@ We'll always use `local` notations waiting for to be `open_locale`ed. I expect c ## Defining without defining -There're really millions of products defined in GA and they're based on geometric product. But the definition might not be the most effient one or the most intuitive one. +There're really millions of products defined in GA and they're based on the geometric product. But the definition might not be the most efficient one or the most intuitive one. -So instead of using `def`, we should make these products just a product with a Prop assering that they're equal to the definition based on gp and let the implementation prove it when intantiate the instance. +So instead of using `def`, we should make these products just a product with a `Prop` asserting that they're equal to the definition based on gp and let the implementation prove it when intantiate the instance. ```lean class has_ga_wedge (α : Type u) extends has_wedge := @@ -166,4 +166,3 @@ induced topology ## Clifford and Grassmann ## graded comes later - From a9c56f722ec38edf01b8c90b1dfa5e35c6ffc4da Mon Sep 17 00:00:00 2001 From: utensil Date: Mon, 13 Jul 2020 16:19:08 +0800 Subject: [PATCH 06/22] Change universe symbols --- src/geometric_algebra/generic/defs.lean | 26 ++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/geometric_algebra/generic/defs.lean b/src/geometric_algebra/generic/defs.lean index 16adc33d3..f1ba5cd16 100644 --- a/src/geometric_algebra/generic/defs.lean +++ b/src/geometric_algebra/generic/defs.lean @@ -10,11 +10,11 @@ import tactic.lint -- import geometric_algebra.generic.operators -universes ur uv ug +universes u₀ u₁ u₂ -variables {R : Type ur} [field R] -variables {V : Type uv} [add_comm_group V] [vector_space R V] -variables {G : Type ug} [ring G] +variables {R : Type u₀} [field R] +variables {V : Type u₁} [add_comm_group V] [vector_space R V] +variables {G : Type u₂} [ring G] section prio -- set_option default_priority 200 -- see Note [default priority] @@ -25,15 +25,15 @@ set_option old_structure_cmd true -/ @[ancestor algebra] class semi_geometric_algebra -(R : Type ur) [field R] -(V : Type uv) [add_comm_group V] [vector_space R V] -(G : Type ug) [ring G] +(R : Type u₀) [field R] +(V : Type u₁) [add_comm_group V] [vector_space R V] +(G : Type u₂) [ring G] extends algebra R G class weak_geometric_algebra -(R : Type ur) [field R] -(V : Type uv) [add_comm_group V] [vector_space R V] -(G : Type ug) [ring G] +(R : Type u₀) [field R] +(V : Type u₁) [add_comm_group V] [vector_space R V] +(G : Type u₂) [ring G] extends semi_geometric_algebra R V G := (fᵣ : R →+* G) @@ -44,9 +44,9 @@ extends semi_geometric_algebra R V G (vector_contract' : ∀ v, ∃ r, fᵥ v * fᵥ v = fᵣ r ) class geometric_algebra -(R : Type ur) [field R] -(V : Type uv) [add_comm_group V] [vector_space R V] -(G : Type ug) [ring G] +(R : Type u₀) [field R] +(V : Type u₁) [add_comm_group V] [vector_space R V] +(G : Type u₂) [ring G] extends weak_geometric_algebra R V G := (q : quadratic_form R V) From 62cbbeb3fd70911445ccbee5e6f3ce65f7d9238a Mon Sep 17 00:00:00 2001 From: utensil Date: Tue, 14 Jul 2020 12:17:39 +0800 Subject: [PATCH 07/22] Trying stop using old structure --- src/geometric_algebra/generic/defs.lean | 50 +++++++++++++++++++------ 1 file changed, 39 insertions(+), 11 deletions(-) diff --git a/src/geometric_algebra/generic/defs.lean b/src/geometric_algebra/generic/defs.lean index f1ba5cd16..290d31d39 100644 --- a/src/geometric_algebra/generic/defs.lean +++ b/src/geometric_algebra/generic/defs.lean @@ -12,18 +12,13 @@ import tactic.lint universes u₀ u₁ u₂ -variables {R : Type u₀} [field R] -variables {V : Type u₁} [add_comm_group V] [vector_space R V] -variables {G : Type u₂} [ring G] - section prio -- set_option default_priority 200 -- see Note [default priority] set_option default_priority 100 -set_option old_structure_cmd true +-- set_option old_structure_cmd true /-- -/ -@[ancestor algebra] class semi_geometric_algebra (R : Type u₀) [field R] (V : Type u₁) [add_comm_group V] [vector_space R V] @@ -36,9 +31,7 @@ class weak_geometric_algebra (G : Type u₂) [ring G] extends semi_geometric_algebra R V G := -(fᵣ : R →+* G) --- this follows normed_algebra in analysis.normed_space.basic -(fᵣ_algebra_map_eq : fᵣ = algebra_map R G) +(fᵣ : R →+* G := algebra_map R G) (fᵥ : V →+ G) -- this is the weaker form of the contraction rule for vectors (vector_contract' : ∀ v, ∃ r, fᵥ v * fᵥ v = fᵣ r ) @@ -58,9 +51,44 @@ end prio namespace geometric_algebra -variables [geometric_algebra R V G] +variables {R : Type u₀} [field R] +variables {V : Type u₁} [add_comm_group V] [vector_space R V] +variables {G : Type u₂} [ring G] +variables (GA : geometric_algebra R V G) + +/- +@[reducible] +def weak_geometric_algebra.vector_contract' : ∀ {R : Type u₀} [_inst_1 : field R] {V : Type u₁} [_inst_2 : add_comm_group V] [_inst_3 : vector_space R V] +{G : Type u₂} [_inst_4 : ring G] [c : weak_geometric_algebra R V G] (v : V), + ∃ (r : R), + ⇑(weak_geometric_algebra.fᵥ R) v * ⇑(weak_geometric_algebra.fᵥ R) v = ⇑(weak_geometric_algebra.fᵣ V) r := +λ (R : Type u₀) [_inst_1 : field R] (V : Type u₁) [_inst_2 : add_comm_group V] [_inst_3 : vector_space R V] +(G : Type u₂) [_inst_4 : ring G] [c : weak_geometric_algebra R V G], [weak_geometric_algebra.vector_contract' c] +-/ +#print weak_geometric_algebra.vector_contract' + +/- +@[reducible] +def geometric_algebra.vector_contract : ∀ {R : Type u₀} [_inst_1 : field R] {V : Type u₁} [_inst_2 : add_comm_group V] [_inst_3 : vector_space R V] +{G : Type u₂} [_inst_4 : ring G] [c : geometric_algebra R V G] (v : V), + ⇑(weak_geometric_algebra.fᵥ R) v * ⇑(weak_geometric_algebra.fᵥ R) v = + ⇑(weak_geometric_algebra.fᵣ V) (⇑(q G) v) := +λ (R : Type u₀) [_inst_1 : field R] (V : Type u₁) [_inst_2 : add_comm_group V] [_inst_3 : vector_space R V] +(G : Type u₂) [_inst_4 : ring G] [c : geometric_algebra R V G], [geometric_algebra.vector_contract c] +-/ +#print geometric_algebra.vector_contract + +/- +theorem geometric_algebra.dummy : ∀ {R : Type u₀} [_inst_1 : field R] {V : Type u₁} [_inst_2 : add_comm_group V] [_inst_3 : vector_space R V] +(v : V), ∃ (r : R), r = r ∧ v = v := +λ {R : Type u₀} [_inst_1 : field R] {V : Type u₁} [_inst_2 : add_comm_group V] [_inst_3 : vector_space R V], sorry +-/ +lemma dummy : ∀ v : V, ∃ r : R, r = r ∧ v = v := sorry + +#print dummy --- instance : inhabited (geometric_algebra R V G) := ⟨0⟩ +-- example : ∀ v : V, ∃ r : R, +-- ⇑(weak_geometric_algebra.fᵥ R) v * ⇑(weak_geometric_algebra.fᵥ R) v = ⇑(weak_geometric_algebra.fᵣ V) r end geometric_algebra From 604ef0f2538993aef925825b5957e4f1e0740fe1 Mon Sep 17 00:00:00 2001 From: utensil Date: Tue, 14 Jul 2020 12:18:53 +0800 Subject: [PATCH 08/22] Experiment with bundled definitions --- .../generic/bundled_defs.lean | 97 +++++++++++++++++++ 1 file changed, 97 insertions(+) create mode 100644 src/geometric_algebra/generic/bundled_defs.lean diff --git a/src/geometric_algebra/generic/bundled_defs.lean b/src/geometric_algebra/generic/bundled_defs.lean new file mode 100644 index 000000000..964b7934b --- /dev/null +++ b/src/geometric_algebra/generic/bundled_defs.lean @@ -0,0 +1,97 @@ +/- +Copyright (c) 2020 lean-ga Team. All rights reserved. +Released under MIT license as described in the file LICENRE. +Authors: Utensil Rong +-/ +import ring_theory.algebra +import linear_algebra.quadratic_form +import tactic +import tactic.lint + +-- import geometric_algebra.generic.operators + +universes u₀ u₁ u₂ + +section prio +-- set_option default_priority 200 -- see Note [default priority] +set_option default_priority 100 + +/-- +-/ +@[ancestor algebra] +class semi_geometric_algebra +(R : Type u₀) [field R] +(G : Type u₂) [ring G] +extends algebra R G +:= +(V : Type u₁) +[V_acg : add_comm_group V] +[V_vs : vector_space R V] + +/-- +-/ +class weak_geometric_algebra +(R : Type u₀) [field R] +(G : Type u₂) [ring G] +extends semi_geometric_algebra R G +:= +(fᵣ : R →+* G := algebra_map R G) +(fᵥ : V →ₗ[R] G) +-- this is the weaker form of the contraction rule for vectors +(vector_contract' : ∀ v, ∃ r, fᵥ v * fᵥ v = fᵣ r ) + +/-- +-/ +class geometric_algebra +(R : Type u₀) [field R] +(G : Type u₂) [ring G] +extends weak_geometric_algebra R G +:= +(q : quadratic_form R V) +(vector_contract : ∀ v, fᵥ v * fᵥ v = fᵣ (q v) ) + +end prio + +-- #print geometric_algebra + +namespace geometric_algebra + +variables {R : Type u₀} [field R] +-- variables {V : Type u₁} [add_comm_group V] [vector_space R V] +variables {G : Type u₂} [ring G] +variables [geometric_algebra R G] +variables (g : geometric_algebra R G) + +namespace trivial + +lemma assoc : ∀ A B C : G, (A * B) * C = A * (B * C) := mul_assoc + +lemma left_distrib : ∀ A B C : G, A * (B + C) = (A * B) + (A * C) := mul_add + +lemma right_distrib : ∀ A B C : G, (A + B) * C = (A * C) + (B * C) := add_mul + +end trivial + +-- def half : G := fᵣ V (2⁻¹ : R) + +-- local notation ` ½[` T `]` := geometric_algebra.fᵣ (2⁻¹ : T) + +-- def symm_prod (A B : G) : G := ½[R] * (A * B + B * A) + +-- #check symm_prod + +-- instance : inhabited (geometric_algebra R V G) := ⟨0⟩ + +-- @[simp] lemma to_fun_eq_coe : fᵥ.to_fun = ⇑fᵥ := rfl + +-- #check ∀ v : g.V, fᵥ v + +-- /- +-- Symmetrised product of two vectors must be a scalar +-- -/ +-- lemma vec_symm_prod_is_scalar: +-- ∀ (u v : V), ∃ k : R, (fᵥ u) * (fᵥ u) = fᵣ k := + +end geometric_algebra + +#lint \ No newline at end of file From 5f8d3ebabb86bd604bcb10a013b38d5e9f505af8 Mon Sep 17 00:00:00 2001 From: utensil Date: Wed, 15 Jul 2020 17:11:58 +0800 Subject: [PATCH 09/22] Breakthrough: worked out stating theorems under variables for unbundled, V_bundled and namespace VR_bundled. There's no way to bundle R only. --- src/geometric_algebra/generic/mwe.lean | 135 +++++++++++++++++++++++++ 1 file changed, 135 insertions(+) create mode 100644 src/geometric_algebra/generic/mwe.lean diff --git a/src/geometric_algebra/generic/mwe.lean b/src/geometric_algebra/generic/mwe.lean new file mode 100644 index 000000000..8c108a88c --- /dev/null +++ b/src/geometric_algebra/generic/mwe.lean @@ -0,0 +1,135 @@ +import ring_theory.algebra + +universes u₀ u₁ u₂ + +namespace unbundled + +class mwc +(R : Type u₀) [field R] +(V : Type u₁) [add_comm_group V] [vector_space R V] +(G : Type u₂) [ring G] +extends algebra R G +:= +(fᵣ : R →+* G := algebra_map R G) +(fᵥ : V →+ G) + +section lemmas + +variables (R : Type u₀) [field R] +variables (V : Type u₁) [add_comm_group V] [vector_space R V] +variables (G : Type u₂) [ring G] + +variables (r₀ : R) +variables (v₀ : V) + +#check mwc.fᵣ + +#check mwc.fᵣ V + +#check mwc.fᵣ V r₀ + +#check mwc.fᵥ + +#check mwc.fᵥ R v₀ + +example (v : V) [mwc R V G] : ∃ r : R, + ((mwc.fᵥ R v) * (mwc.fᵥ R v)) = ((mwc.fᵥ R v) * (mwc.fᵥ R v) : G) +:= sorry + +example (v : V) [mwc R V G] : ∃ r : R, + ((mwc.fᵥ R v) * (mwc.fᵥ R v)) = (mwc.fᵣ V r : G) +:= sorry + +example [mwc R V G] : ∀ v : V, ∃ r : R, + ((mwc.fᵥ R v) * (mwc.fᵥ R v)) = ((mwc.fᵥ R v) * (mwc.fᵥ R v) : G) +:= sorry + +example [mwc R V G] : ∀ v : V, ∃ r : R, + ((mwc.fᵥ R v) * (mwc.fᵥ R v)) = (mwc.fᵣ V r : G) +:= sorry + +end lemmas + +end unbundled + +namespace V_bundled + +class mwc +(R : Type u₀) [field R] +(G : Type u₂) [ring G] +extends algebra R G +:= +(V : Type u₁) +[V_acg : add_comm_group V] +[V_vs : vector_space R V] +(fᵣ : R →+* G := algebra_map R G) +(fᵥ : V →+ G) + +section lemmas + +variables (R : Type u₀) [field R] +variables (G : Type u₂) [ring G] [mwc R G] + +variables (r₀ : R) +variables (v₀ : mwc.V R G) + +#check mwc.fᵣ + +#check mwc.fᵣ r₀ + +#check mwc.fᵥ + +#check mwc.V + +#check mwc.V R G + +#check mwc.fᵥ v₀ + +example : ∀ v : mwc.V R G, ∃ r : R, + (mwc.fᵥ v) * (mwc.fᵥ v) = mwc.fᵣ r +:= sorry + +end lemmas + +end V_bundled + +namespace VR_bundled + +class mwc +(G : Type u₂) [ring G] +:= +(R : Type u₀) +[R_f : field R] +(V : Type u₁) +[V_acg : add_comm_group V] +[V_vs : vector_space R V] +(to_algebra : algebra R G) +(fᵣ : R →+* G := algebra_map R G) +(fᵥ : V →+ G) + +section lemmas + +variables (G : Type u₂) [ring G] [mwc G] + +variables (r₀ : mwc.R G) +variables (v₀ : mwc.V G) + +#check mwc.fᵣ + +#check mwc.fᵣ r₀ + +#check mwc.fᵥ + +#check mwc.V + +#check mwc.V G + +#check mwc.fᵥ v₀ + +example : ∀ v : mwc.V G, ∃ r : mwc.R G, + (mwc.fᵥ v) * (mwc.fᵥ v) = mwc.fᵣ r +:= sorry + +end lemmas + +end VR_bundled \ No newline at end of file From a727f31601802ee7b4c84bdde16ae8935a795ec4 Mon Sep 17 00:00:00 2001 From: utensil Date: Sat, 18 Jul 2020 18:32:14 +0800 Subject: [PATCH 10/22] Update related inspirations.lean --- docs/misc/related.md | 39 ++++++++++++------- .../generic/inspirations.lean | 31 +++++++++++++++ 2 files changed, 55 insertions(+), 15 deletions(-) diff --git a/docs/misc/related.md b/docs/misc/related.md index c4c1e1b5a..8dafc29b0 100644 --- a/docs/misc/related.md +++ b/docs/misc/related.md @@ -4,23 +4,9 @@ Related References GA & Lean related -------------------- -### Lean/Mathlib Src - -- [init/core](https://github.com/leanprover/lean/blob/master/library/init/core.lean) -- [data/complex/basic](https://github.com/leanprover-community/mathlib/blob/master/src/data/complex/basic.lean) -- [data/matrix/basic](https://github.com/leanprover-community/mathlib/blob/master/src/data/matrix/basic.lean) -- [geometry/euclidean](https://github.com/leanprover-community/mathlib/blob/master/src/geometry/euclidean.lean) - - https://github.com/jsm28/bmo2-2020-lean/ -- [geometry/manifold/real_instances](https://github.com/leanprover-community/mathlib/blob/master/src/geometry/manifold/real_instances.lean) -- [analysis/convex/cone](https://github.com/leanprover-community/mathlib/blob/master/src/analysis/convex/cone.lean) -- [analysis/normed_space/real_inner_product](https://github.com/leanprover-community/mathlib/blob/master/src/analysis/normed_space/real_inner_product.lean) - - [doc](https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/real_inner_product.html#inner_product_space) - ### Lean/Mathlib PRs - [`feat(data/quaternion): define quaternions and prove some basic properties #2339`](https://github.com/leanprover-community/mathlib/pull/2339/) -- [refactor(algebra/module): change module into an abbreviation for semimodule #2848](https://github.com/leanprover-community/mathlib/pull/2848) -- [feat(algebra/add_torsor): torsors of additive group actions #2720](https://github.com/leanprover-community/mathlib/pull/2720/files) ### Inspiring Lean Code @@ -28,6 +14,8 @@ GA & Lean related - [commutative differential graded algebras](https://gist.github.com/kbuzzard/f5ee35457c5d257ceec58c66d7da0c38) - [free module](https://gist.github.com/sflicht/53bdcdb1e3536e668736f7b4eb63cd79) - [Huber_pair](https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/Huber_pair.lean#L72) +- https://github.com/jsm28/bmo2-2020-lean/ +- https://github.com/GeoCoq/GeoCoq/tree/master/Highschool (in Coq) ### Lean/Mathlib Doc @@ -63,6 +51,7 @@ GA & Lean related - https://github.com/leanprover/vscode-lean/blob/master/translations.json - https://en.wikipedia.org/wiki/Unicode_subscripts_and_superscripts - https://en.wikipedia.org/wiki/List_of_mathematical_symbols_by_subject + - [Unicode characters and corresponding LaTeX math mode commands](http://milde.users.sourceforge.net/LUCR/Math/unimathsymbols.pdf) ### Tactics @@ -114,6 +103,24 @@ with Clifford Algebras](https://macau.uni-kiel.de/servlets/MCRFileNodeServlet/di - [Chris Doran's Geometric Algebra Haskell Package](https://github.com/ga/haskell) - http://geometry.mrao.cam.ac.uk/2016/10/geometric-algebra-2016/ - http://math.uga.edu/~pete/quadraticforms.pdf +- [Comparing Complex Numbers to Clifford Algebra](https://www.av8n.com/physics/complex-clifford.pdf) +- [Euclidean Geometry and Geometric Algebra](http://geometry.mrao.cam.ac.uk/2020/06/euclidean-geometry-and-geometric-algebra/) + +Related Math Concepts +------------------------ + +- [Free module](https://en.wikipedia.org/wiki/Free_module) +- [Free algebra](https://en.wikipedia.org/wiki/Free_algebra) +- [Universal algebra](https://en.wikipedia.org/wiki/Universal_algebra) +- [Sedenion](https://en.wikipedia.org/wiki/Sedenion) +- [Alternative algebra](https://en.wikipedia.org/wiki/Alternative_algebra) +- [Metric signature](https://en.wikipedia.org/wiki/Metric_signature) +- [Complete lattice](https://en.wikipedia.org/wiki/Complete_lattice) +- [Filters](https://en.wikipedia.org/wiki/Filter_(mathematics)) + - [Topology in mathlib](https://www.imo.universite-paris-saclay.fr/~pmassot/topology.pdf) +- [examples of fields](https://planetmath.org/examplesoffields) +- [differential forms on simplices](https://ncatlab.org/nlab/show/differential+forms+on+simplices) + - [Differential graded algebras](https://stacks.math.columbia.edu/tag/061U) Lean related ------------------ @@ -182,4 +189,6 @@ Theorem Prover/Type theory related - [Comparison of Two Theorem Provers: Isabelle/HOL and Coq](https://arxiv.org/abs/1808.09701) - [A Survey of Languages for Formalizing Mathematics](https://arxiv.org/abs/2005.12876) - [Category theory for scientists](https://arxiv.org/abs/1302.6946) -- [Rethinking set theory](https://arxiv.org/abs/1212.6543) \ No newline at end of file +- [Rethinking set theory](https://arxiv.org/abs/1212.6543) +- [Lean versus Coq: The cultural chasm](https://artagnon.com/articles/leancoq) +- [Equality of mathematical structures](https://www.cs.bham.ac.uk/~mhe/.talks/xii-pcc.pdf) \ No newline at end of file diff --git a/src/geometric_algebra/generic/inspirations.lean b/src/geometric_algebra/generic/inspirations.lean index a7a6e6794..184e0fdd6 100644 --- a/src/geometric_algebra/generic/inspirations.lean +++ b/src/geometric_algebra/generic/inspirations.lean @@ -10,17 +10,40 @@ import init.core import algebra.group.defs import algebra.group.hom +-- [refactor(algebra/module): change module into an abbreviation for semimodule #2848](https://github.com/leanprover-community/mathlib/pull/2848) import algebra.module +-- [feat(algebra/add_torsor): torsors of additive group actions #2720](https://github.com/leanprover-community/mathlib/pull/2720/files) +import algebra.add_torsor import algebra.direct_limit +-- def closure +import group_theory.subgroup import ring_theory.algebra +-- structure bilin_form +-- def is_sym +import linear_algebra.bilinear_form +-- def polar +-- structure quadratic_form import linear_algebra.quadratic_form +-- def module_equiv_finsupp +import linear_algebra.basis +-- @[derive [add_comm_group, module R]] def dual +-- def eval_equiv +-- def dual_basis +import linear_algebra.dual +-- def tensor_product +import linear_algebra.tensor_product +-- @[reducible] def finite_dimensional +import linear_algebra.finite_dimensional +import linear_algebra.affine_space import data.real.basic import data.complex.basic import data.complex.module import data.matrix.basic +-- def angle import geometry.euclidean +-- class inner_product_space import geometry.manifold.real_instances import analysis.convex.cone @@ -30,4 +53,12 @@ import analysis.normed_space.real_inner_product import tactic import tactic.lint +/- +### Lean/Mathlib PRs + +- [`feat(data/quaternion): define quaternions and prove some basic properties #2339`](https://github.com/leanprover-community/mathlib/pull/2339/) +- [refactor(algebra/module): change module into an abbreviation for semimodule #2848](https://github.com/leanprover-community/mathlib/pull/2848) +- [feat(algebra/add_torsor): torsors of additive group actions #2720](https://github.com/leanprover-community/mathlib/pull/2720/files) +-/ + #lint \ No newline at end of file From f7f09d651a639ff1dbd201f9e440d507ce818628 Mon Sep 17 00:00:00 2001 From: utensil Date: Sat, 18 Jul 2020 18:33:15 +0800 Subject: [PATCH 11/22] Ignore local experiments --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 1cb9f3cfa..0eb7b3c89 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ *.olean /_target /leanpkg.path +src/geometric_algebra/experiment/ From 8371f5d2dc02abef78da0e2b37a2fe668892e586 Mon Sep 17 00:00:00 2001 From: utensil Date: Sat, 18 Jul 2020 18:34:03 +0800 Subject: [PATCH 12/22] Further explore unbundled v.s. (semi-)bundled --- src/geometric_algebra/generic/mwe.lean | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/geometric_algebra/generic/mwe.lean b/src/geometric_algebra/generic/mwe.lean index 8c108a88c..833a4cdfb 100644 --- a/src/geometric_algebra/generic/mwe.lean +++ b/src/geometric_algebra/generic/mwe.lean @@ -73,12 +73,24 @@ variables (G : Type u₂) [ring G] [mwc R G] variables (r₀ : R) variables (v₀ : mwc.V R G) +-- variables {GA : mwc R G} + +/- +V_bundled.mwc.fᵣ : Π {R : Type u₀} [_inst_1 : field R] {G : Type u₂} [_inst_2 : ring G] [c : mwc R G], R →+* G +-/ #check mwc.fᵣ #check mwc.fᵣ r₀ +/- +V_bundled.mwc.fᵥ : Π {R : Type u₀} [_inst_1 : field R] {G : Type u₂} [_inst_2 : ring G] [c : mwc R G], mwc.V R G →+ G + +-/ #check mwc.fᵥ +/- +mwc.V : Π (R : Type u_2) [_inst_1 : field R] (G : Type u_4) [_inst_2 : ring G] [c : mwc R G], Type u_3 +-/ #check mwc.V #check mwc.V R G @@ -86,6 +98,14 @@ variables (v₀ : mwc.V R G) #check mwc.fᵥ v₀ example : ∀ v : mwc.V R G, ∃ r : R, + mwc.fᵣ r = (mwc.fᵣ r : G) +:= sorry + +example : ∀ v : mwc.V R G, ∃ r : R, + (mwc.fᵥ v) * (mwc.fᵥ v) = mwc.fᵣ r +:= sorry + +example {GA : mwc R G} : ∀ v : GA.V, ∃ r : R, (mwc.fᵥ v) * (mwc.fᵥ v) = mwc.fᵣ r := sorry From f465714f8ffd279fcd109406f3788b2261a9b5ba Mon Sep 17 00:00:00 2001 From: utensil Date: Sat, 18 Jul 2020 22:59:29 +0800 Subject: [PATCH 13/22] Add equiv to inspirations --- src/geometric_algebra/generic/inspirations.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/geometric_algebra/generic/inspirations.lean b/src/geometric_algebra/generic/inspirations.lean index 184e0fdd6..ba1583802 100644 --- a/src/geometric_algebra/generic/inspirations.lean +++ b/src/geometric_algebra/generic/inspirations.lean @@ -7,6 +7,7 @@ This file contains only imports which are just the lean files that the authors draw inspirations from. -/ import init.core +import init.function import algebra.group.defs import algebra.group.hom @@ -36,6 +37,7 @@ import linear_algebra.tensor_product import linear_algebra.finite_dimensional import linear_algebra.affine_space +import data.equiv.basic import data.real.basic import data.complex.basic import data.complex.module From 487738a7dd97d2a302126d6f2f18370e38cfa5fa Mon Sep 17 00:00:00 2001 From: utensil Date: Sat, 18 Jul 2020 22:59:44 +0800 Subject: [PATCH 14/22] Cl(V,Q) is a N-filtered algebra --- docs/misc/related.md | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/docs/misc/related.md b/docs/misc/related.md index 8dafc29b0..c2fbbc058 100644 --- a/docs/misc/related.md +++ b/docs/misc/related.md @@ -122,6 +122,24 @@ Related Math Concepts - [differential forms on simplices](https://ncatlab.org/nlab/show/differential+forms+on+simplices) - [Differential graded algebras](https://stacks.math.columbia.edu/tag/061U) +> A [Clifford algebra](https://en.wikipedia.org/wiki/Clifford_algebra) is an algebra generated by a vector space with a quadratic form, and is a unital associative algebra(a K-algebra(K is called the base field of Clifford algebra)), and satisfy a [universal property](https://en.wikipedia.org/wiki/Universal_property). +> Let Q:V→k denote a quadratic form on a vector space V over a field k. The Clifford algebra Cl(V,Q) is defined as T(V)/I_Q where T(V) is the tensor algebra of V and I_Q is the two-sided ideal generated by all elements of the form v⊗v−Q(v) for all v∈V. +> Cl(V,Q) is the exterior algebra ∧V when Q=0. +> Clifford algebra is also a quantization of the exterior algebra. +> To create a Clifford algebra, all one needs to do is specify a quadratic form. +> Cl(V,Q) is a N-[filtered algebra](https://en.wikipedia.org/wiki/Filtered_algebra), Z/2Z-[graded algebra](https://en.wikipedia.org/wiki/Graded_ring#Graded_algebra), the associated graded algebra to the filtration is the exterior algebra +> quantization map q: ∧(V)→Cl(V) +> Clifford algebras may be thought of as quantizations (cf. quantum group) of the exterior algebra, in the same way that the [Weyl algebra](https://en.wikipedia.org/wiki/Weyl_algebra) is a quantization of the symmetric algebra. +> Weyl algebras and Clifford algebras admit a further structure of a [*-algebra](https://en.wikipedia.org/wiki/*-algebra), and can be unified as even and odd terms of a superalgebra, as discussed in CCR and CAR algebras. + +- [Clifford Algebras in Sage manual](https://doc.sagemath.org/html/en/reference/algebras/sage/algebras/clifford_algebra.html) +- [Clifford Algebras as Filtered Algebras](http://www-math.mit.edu/~dav/cliffordfilt.pdf) +- [MATH 651: Lie Algebras - Lecture 8 - Universal Enveloping Algebras and Related Concepts, II](https://www.math.upenn.edu/~brweber/Courses/2013/Math651/Notes/L8_UEnvAlgII.pdf) +- [PG course on Spin Geometry - Lecture 1: Clifford algebras: basic notions](https://empg.maths.ed.ac.uk/Activities/Spin/Lecture1.pdf) +- [MAT 1120HF Lie groups and Clifford algebras - CHAPTER 2 Clifford algebras](http://www.math.toronto.edu/mein/teaching/LieClifford/cl2.pdf) +- [Topics in Representation Theory: Clifford Algebras](http://www.math.columbia.edu/~woit/notes17.pdf) +- [Clifford algebras and Lie theory](https://link.springer.com/chapter/10.1007%2F978-3-642-36216-3_2) + Lean related ------------------ From 699cd14ef599426b1dcdacbc3f48b450e9851b34 Mon Sep 17 00:00:00 2001 From: utensil Date: Tue, 21 Jul 2020 10:44:00 +0800 Subject: [PATCH 15/22] Relation with Grassmann-Cayley Algebra --- docs/misc/related.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/docs/misc/related.md b/docs/misc/related.md index c2fbbc058..f56b8af73 100644 --- a/docs/misc/related.md +++ b/docs/misc/related.md @@ -140,6 +140,10 @@ Related Math Concepts - [Topics in Representation Theory: Clifford Algebras](http://www.math.columbia.edu/~woit/notes17.pdf) - [Clifford algebras and Lie theory](https://link.springer.com/chapter/10.1007%2F978-3-642-36216-3_2) +- [Geometric Algebra FAQ](https://staff.science.uva.nl/l.dorst/clifford/faq.html) + - Q11. HOW IS IT DIFFERENT FROM CLIFFORD ALGEBRA? + - Q12. HOW IS IT DIFFERENT FROM GRASSMANN-CAYLEY ALGEBRA? + Lean related ------------------ From d3774507d92dc90c0658ac18dc31308d0949304b Mon Sep 17 00:00:00 2001 From: utensil Date: Tue, 21 Jul 2020 17:34:23 +0800 Subject: [PATCH 16/22] leanproject up --- leanpkg.toml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/leanpkg.toml b/leanpkg.toml index db0088588..807a376d3 100644 --- a/leanpkg.toml +++ b/leanpkg.toml @@ -1,8 +1,8 @@ [package] name = "lean-ga" version = "0.1" -lean_version = "leanprover-community/lean:3.16.5" +lean_version = "leanprover-community/lean:3.17.1" path = "src" [dependencies] -mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "e803c851d221764eb3ec8bf010e4ed300a32b113"} +mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "0322d8927d4cdc401a33743ab84e497e85916886"} From a388fbd22f3188b0f5a07cd35fee541e7f6d2e3a Mon Sep 17 00:00:00 2001 From: utensil Date: Wed, 29 Jul 2020 00:18:26 +0800 Subject: [PATCH 17/22] group, proof_demo, and unbundled GA for the talk --- src/geometric_algebra/nursery/talk.lean | 136 ++++++++++++++++++++++++ 1 file changed, 136 insertions(+) create mode 100644 src/geometric_algebra/nursery/talk.lean diff --git a/src/geometric_algebra/nursery/talk.lean b/src/geometric_algebra/nursery/talk.lean new file mode 100644 index 000000000..4a7c987ae --- /dev/null +++ b/src/geometric_algebra/nursery/talk.lean @@ -0,0 +1,136 @@ +import algebra.group +import tactic +import ring_theory.algebra +import linear_algebra.quadratic_form + +universe u + +variables (α : Type u) + +namespace Group + +namespace extends_has + +structure group extends has_mul α, has_one α, has_inv α := +(mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)) +(one_mul : ∀ (a : α), 1 * a = a) +(mul_one : ∀ (a : α), a * 1 = a) +(mul_left_inv : ∀ (a : α), a⁻¹ * a = 1) + +end extends_has + +namespace explicit + +structure group := +(mul : α → α → α) +(infix `*` := mul) +(mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)) + +(one : α) +(notation `𝟙` := one) +(one_mul : ∀ (a : α), 𝟙 * a = a) +(mul_one : ∀ (a : α), a * 𝟙 = a) + +(inv : α → α) +(postfix `⁻¹` := inv) +(mul_left_inv : ∀ (a : α), a⁻¹ * a = 𝟙) + +end explicit + +namespace in_real_lean + +class group (α : Type u) extends monoid α, has_inv α := +(mul_left_inv : ∀ a : α, a⁻¹ * a = 1) + +class add_group (α : Type u) extends add_monoid α, has_neg α := +(add_left_neg : ∀ a : α, -a + a = 0) + +attribute [to_additive add_group] group + +end in_real_lean + +end Group + +namespace proof_demo +open int + +theorem le.antisymm : ∀ {a b : ℤ}, a ≤ b → b ≤ a → a = b := +begin +assume a b : ℤ, assume (H₁ : a ≤ b) (H₂ : b ≤ a), +obtain ⟨n, Hn⟩ := int.le.dest H₁, +obtain ⟨m, Hm⟩ := int.le.dest H₂, +have H₃ : a + of_nat (n + m) = a + 0, from + calc + a + of_nat (n + m) = a + (of_nat n + m) : rfl + ... = a + (n + m) : by rw of_nat_eq_coe + ... = a + n + m : by rw add_assoc + ... = b + m : by rw Hn + ... = a : Hm + ... = a + 0 : by rw add_zero, +have H₄ : of_nat (n + m) = of_nat 0, from add_left_cancel H₃, +have H₅ : n + m = 0, from of_nat.inj H₄, +have h₆ : n = 0, from nat.eq_zero_of_add_eq_zero_right H₅, +show a = b, from + calc + a = a + 0 : by simp_rw [add_zero] + ... = a + n : by simp_rw [h₆, int.coe_nat_zero] + ... = b : Hn +end +end proof_demo + +namespace GA + +namespace first + +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 := +(fₛ : K →+* G) +(fᵥ : V →+ 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] : +∀ aᵥ bᵥ : V, ∃ kₛ : 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], + abel, + }, + use kabₛ - kaₛ - kbₛ, + rw h2, + abel, +end + +end first + +end GA \ No newline at end of file From 724220b87db5a7e329effebb29e0591d5081c978 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 29 Jul 2020 03:45:10 +0100 Subject: [PATCH 18/22] Alternate proof formulation, maybe more readable? (#10) --- 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 8538cfca3d95923e9db104f492cdaf80f0930893 Mon Sep 17 00:00:00 2001 From: utensil Date: Wed, 29 Jul 2020 14:06:11 +0800 Subject: [PATCH 19/22] General clean up and improve the proof doc --- src/geometric_algebra/nursery/talk.lean | 36 ++++++++++++++----------- 1 file changed, 20 insertions(+), 16 deletions(-) diff --git a/src/geometric_algebra/nursery/talk.lean b/src/geometric_algebra/nursery/talk.lean index 5daeb01e2..8a3134176 100644 --- a/src/geometric_algebra/nursery/talk.lean +++ b/src/geometric_algebra/nursery/talk.lean @@ -7,7 +7,7 @@ universe u variables (α : Type u) -/-- +/- Groups defined three ways -/ namespace Group @@ -54,7 +54,7 @@ end in_real_lean end Group -/-- +/- An example of a proof -/ namespace proof_demo @@ -85,7 +85,7 @@ end end proof_demo -/-- An example of geometric algebra -/ +/- An example of geometric algebra -/ namespace GA namespace first @@ -94,19 +94,14 @@ variables (K : Type u) [field K] variables (V : Type u) [add_comm_group V] [vector_space K V] -#print linear_map - -def sqr {α : Type u} [has_mul α] (x : α) := x*x +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 →ₗ[K] G) --- (infix ` ❍ `:70 := has_mul.mul) (contraction : ∀ v : V, ∃ k : K, (fᵥ v)² = fₛ k) --- local infix ` ❍ `:70 := has_mul.mul - /- Symmetrised product of two vectors must be a scalar -/ @@ -116,31 +111,40 @@ example let a := ga.fᵥ aᵥ, b := ga.fᵥ bᵥ, k := ga.fₛ kₛ in a * b + b * a = k := begin + -- vectors aᵥ bᵥ assume aᵥ bᵥ, - -- some tricks to unfold the `let`s and make things look tidy - delta, + + -- multivectors a b set a := ga.fᵥ aᵥ, set b := ga.fᵥ bᵥ, - -- collect square terms + -- simplify the goal by definition, i.e. remove let etc. + delta, + + -- rewrite the goal to 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 + -- rewrite square terms of vectors + -- to scalars using the contraction axiom obtain ⟨kabₛ, hab⟩ := ga.contraction (aᵥ + bᵥ), obtain ⟨kaₛ, ha⟩ := ga.contraction (aᵥ), obtain ⟨kbₛ, hb⟩ := ga.contraction (bᵥ), + + -- map the above to multivectors 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 + show a² = ga.fₛ kaₛ, by rw [← ha], + show b² = ga.fₛ kbₛ, by rw [← hb] ], - -- rearrange, solve by inspection + -- collect scalars simp only [← ring_hom.map_sub], + + -- use the scalars as the witness of the existence use kabₛ - kaₛ - kbₛ, end From 948c9b4c82776918b14f6b0835d6fc2838a5039a Mon Sep 17 00:00:00 2001 From: utensil Date: Wed, 29 Jul 2020 15:37:25 +0800 Subject: [PATCH 20/22] Add bundled quadratic_form --- src/geometric_algebra/nursery/talk.lean | 66 +++++++++++++++++++++---- 1 file changed, 56 insertions(+), 10 deletions(-) diff --git a/src/geometric_algebra/nursery/talk.lean b/src/geometric_algebra/nursery/talk.lean index 8a3134176..b02346140 100644 --- a/src/geometric_algebra/nursery/talk.lean +++ b/src/geometric_algebra/nursery/talk.lean @@ -88,7 +88,7 @@ end proof_demo /- An example of geometric algebra -/ namespace GA -namespace first +namespace unbundled_weak variables (K : Type u) [field K] @@ -100,7 +100,7 @@ local postfix `²`:80 := sqr structure GA (G : Type u) [ring G] [algebra K G] := (fₛ : K →+* G) (fᵥ : V →ₗ[K] G) -(contraction : ∀ v : V, ∃ k : K, (fᵥ v)² = fₛ k) +(vec_contraction : ∀ v : V, ∃ k : K, (fᵥ v)² = fₛ k) /- Symmetrised product of two vectors must be a scalar @@ -111,6 +111,9 @@ example let a := ga.fᵥ aᵥ, b := ga.fᵥ bᵥ, k := ga.fₛ kₛ in a * b + b * a = k := begin + -- simplify the goal by definition, i.e. remove let etc. + delta, + -- vectors aᵥ bᵥ assume aᵥ bᵥ, @@ -118,9 +121,6 @@ begin set a := ga.fᵥ aᵥ, set b := ga.fᵥ bᵥ, - -- simplify the goal by definition, i.e. remove let etc. - delta, - -- rewrite the goal to square terms rw (show a * b + b * a = (a + b)² - a² - b², from begin unfold sqr, @@ -129,10 +129,10 @@ begin end), -- rewrite square terms of vectors - -- to scalars using the contraction axiom - obtain ⟨kabₛ, hab⟩ := ga.contraction (aᵥ + bᵥ), - obtain ⟨kaₛ, ha⟩ := ga.contraction (aᵥ), - obtain ⟨kbₛ, hb⟩ := ga.contraction (bᵥ), + -- to scalars using the vector contraction axiom + obtain ⟨kabₛ, hab⟩ := ga.vec_contraction (aᵥ + bᵥ), + obtain ⟨kaₛ, ha⟩ := ga.vec_contraction (aᵥ), + obtain ⟨kbₛ, hb⟩ := ga.vec_contraction (bᵥ), -- map the above to multivectors rw [ @@ -148,6 +148,52 @@ begin use kabₛ - kaₛ - kbₛ, end -end first +end unbundled_weak + +namespace bundled_quad + +variables (K : Type u) [field K] + +-- variables (V : Type u) [add_comm_group V] [vector_space K V] + +def sqr {α : Type u} [has_mul α] (x : α) := x * x +local postfix `²`:80 := sqr + +structure GA (G : Type u) [ring G] [algebra K G] := +(V : Type u) [vec_is_acg : add_comm_group V] [vec_is_vs : vector_space K V] +(fₛ : K →+* G) +(fᵥ : V →ₗ[K] G) +(q : quadratic_form K V) +(vec_contraction : ∀ v : V, (fᵥ v)² = fₛ (q v)) + +attribute [instance] GA.vec_is_acg +attribute [instance] GA.vec_is_vs + +/- + Symmetrised product of two vectors must be a scalar +-/ +example (G : Type u) [ring G] [algebra K G] [ga : GA K G] : +∀ aᵥ bᵥ : ga.V, let a := ga.fᵥ aᵥ, b := ga.fᵥ bᵥ in + a * b + b * a = ga.fₛ (quadratic_form.polar ga.q aᵥ bᵥ) := +begin + -- simplify the goal by definition, i.e. remove let etc. + delta, + + -- vectors aᵥ bᵥ + assume aᵥ bᵥ, + + -- multivectors a b + set a := ga.fᵥ aᵥ with ha, + set b := ga.fᵥ bᵥ with hb, + + rw [ha, hb], + unfold quadratic_form.polar, + simp only [ring_hom.map_add, ring_hom.map_sub, ←GA.vec_contraction], + unfold sqr, + simp only [linear_map.map_add, linear_map.map_sub], + noncomm_ring, +end + +end bundled_quad end GA \ No newline at end of file From 2a2c83a6046c70f1741fd07903dcfe2382f1565b Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 29 Jul 2020 18:02:13 +0800 Subject: [PATCH 21/22] Add unbundled_range --- src/geometric_algebra/nursery/talk.lean | 39 +++++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/src/geometric_algebra/nursery/talk.lean b/src/geometric_algebra/nursery/talk.lean index b02346140..4886a41df 100644 --- a/src/geometric_algebra/nursery/talk.lean +++ b/src/geometric_algebra/nursery/talk.lean @@ -150,6 +150,45 @@ end end unbundled_weak +namespace unbundled_range + +variables (K : Type u) [field K] + +variables (V : Type u) [add_comm_group V] [vector_space K V] + +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 →ₐ[K] G) +(fᵥ : V →ₗ[K] G) +(contraction : ∀ v ∈ fᵥ.range, v² ∈ fₛ.range ) +/- + Symmetrised product of two vectors must be a scalar +-/ +example +(G : Type u) [ring G] [algebra K G] [ga : GA K V G] : +∀ a b ∈ ga.fᵥ.range, a * b + b * a ∈ ga.fₛ.range := +begin + assume a 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), + -- obtain proofs that each term is a scalar + assume ha hb, + have ha2 := ga.contraction a ha, + have hb2 := ga.contraction b hb, + have hab2 := ga.contraction (a + b) (submodule.add_mem _ ha hb), + apply subalgebra.sub_mem, + apply subalgebra.sub_mem, + repeat {assumption}, +end + +end unbundled_range + namespace bundled_quad variables (K : Type u) [field K] From 2f2dff18885d6a1ce0000885ef8ca54ebbfbbb45 Mon Sep 17 00:00:00 2001 From: utensil Date: Wed, 29 Jul 2020 18:18:38 +0800 Subject: [PATCH 22/22] Rewrite to calc --- src/geometric_algebra/nursery/talk.lean | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/src/geometric_algebra/nursery/talk.lean b/src/geometric_algebra/nursery/talk.lean index 4886a41df..8f8ddc92d 100644 --- a/src/geometric_algebra/nursery/talk.lean +++ b/src/geometric_algebra/nursery/talk.lean @@ -123,9 +123,11 @@ begin -- rewrite the goal to square terms rw (show a * b + b * a = (a + b)² - a² - b², from begin - unfold sqr, - simp only [left_distrib, right_distrib], - abel, + calc a * b + b * a + = a * b + b * a + a * a - a * a + b * b - b * b : by simp only [add_sub_cancel] + ... = a * a + a * b + (b * a + b * b) - a * a - b * b : by abel + ... = (a + b) * (a + b) - a * a - b * b : by simp only [left_distrib, right_distrib] + ... = (a + b)² - a² - b² : by refl end), -- rewrite square terms of vectors @@ -173,9 +175,11 @@ begin assume a 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, + calc a * b + b * a + = a * b + b * a + a * a - a * a + b * b - b * b : by simp only [add_sub_cancel] + ... = a * a + a * b + (b * a + b * b) - a * a - b * b : by abel + ... = (a + b) * (a + b) - a * a - b * b : by simp only [left_distrib, right_distrib] + ... = (a + b)² - a² - b² : by refl end), -- obtain proofs that each term is a scalar assume ha hb,