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/ diff --git a/docs/misc/new_design.md b/docs/misc/new_design.md new file mode 100644 index 000000000..d430fb5d6 --- /dev/null +++ b/docs/misc/new_design.md @@ -0,0 +1,168 @@ +# 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.: + +```lean +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 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` 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 := +(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 diff --git a/docs/misc/related.md b/docs/misc/related.md index c4c1e1b5a..f56b8af73 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,46 @@ 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) + +> 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) + +- [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 ------------------ @@ -182,4 +211,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/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"} 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 diff --git a/src/geometric_algebra/generic/defs.lean b/src/geometric_algebra/generic/defs.lean new file mode 100644 index 000000000..290d31d39 --- /dev/null +++ b/src/geometric_algebra/generic/defs.lean @@ -0,0 +1,95 @@ +/- +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 +-- set_option old_structure_cmd true + +/-- +-/ +class semi_geometric_algebra +(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 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 := 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 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) +(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 (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 + +-- 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 + +#lint \ No newline at end of file diff --git a/src/geometric_algebra/generic/inspirations.lean b/src/geometric_algebra/generic/inspirations.lean new file mode 100644 index 000000000..ba1583802 --- /dev/null +++ b/src/geometric_algebra/generic/inspirations.lean @@ -0,0 +1,66 @@ +/- +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 init.function + +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.equiv.basic +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 +import analysis.normed_space.basic +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 diff --git a/src/geometric_algebra/generic/mwe.lean b/src/geometric_algebra/generic/mwe.lean new file mode 100644 index 000000000..833a4cdfb --- /dev/null +++ b/src/geometric_algebra/generic/mwe.lean @@ -0,0 +1,155 @@ +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) + +-- 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 + +#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 + +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 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 + diff --git a/src/geometric_algebra/nursery/talk.lean b/src/geometric_algebra/nursery/talk.lean new file mode 100644 index 000000000..8f8ddc92d --- /dev/null +++ b/src/geometric_algebra/nursery/talk.lean @@ -0,0 +1,242 @@ +import algebra.group +import tactic +import ring_theory.algebra +import linear_algebra.quadratic_form + +universe u + +variables (α : Type u) + +/- +Groups defined three ways +-/ +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 + +/- +An example of a proof +-/ +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 + + +/- An example of geometric algebra -/ +namespace GA + +namespace unbundled_weak + +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 →+* G) +(fᵥ : V →ₗ[K] G) +(vec_contraction : ∀ v : V, ∃ k : K, (fᵥ v)² = fₛ k) + +/- + 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ᵥ : V, ∃ kₛ : K, + 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ᵥ, + + -- multivectors a b + set a := ga.fᵥ aᵥ, + set b := ga.fᵥ bᵥ, + + -- rewrite the goal to square terms + rw (show a * b + b * a = (a + b)² - a² - b², from begin + 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 + -- 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 [ + 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] + ], + + -- collect scalars + simp only [← ring_hom.map_sub], + + -- use the scalars as the witness of the existence + use kabₛ - kaₛ - kbₛ, +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 + 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, + 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] + +-- 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