[WIP] New Design #8
+923
−17
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,3 +1,4 @@ | ||
| *.olean | ||
| /_target | ||
| /leanpkg.path | ||
| src/geometric_algebra/experiment/ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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. | ||
|
|
||
|
There was a problem hiding this comment. TODO: Add structure v.s. class here |
||
| ## 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 : α → α → α) | ||
|
There was a problem hiding this comment.
|
||
| ``` | ||
|
|
||
| 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.: | ||
|
There was a problem hiding this comment. It turns out that There was a problem hiding this comment. Can't we have There was a problem hiding this comment. old structure is flat, so no matter where smul comes from, as long as it's in our inheritance hierarchy, it conflicts. Better avoid it anyway. |
||
|
|
||
| ```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 | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,8 +1,8 @@ | ||
| [package] | ||
| name = "lean-ga" | ||
| version = "0.1" | ||
| lean_version = "leanprover-community/lean:3.17.1" | ||
| path = "src" | ||
|
|
||
| [dependencies] | ||
| mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "0322d8927d4cdc401a33743ab84e497e85916886"} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 | ||
|
There was a problem hiding this comment.
|
||
|
|
||
| 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 ) | ||
|
There was a problem hiding this comment. Is this weak form useful? Is there a way we can have lean infer it from the strong form? There was a problem hiding this comment. Yes, this can be proven by the strong form. I'm leaving the weak layer here because I want to be explicit about three layers that: purely just an ordinary algebra, having something about the linear map (the weak form demonstrate the usefulness of the linear maps but it could also be not there), and bundling a quadratic form. The real issue between choosing the weak form or the strong form, is whether we assume a metric at the beginning. There are literatures assumes no metric or assume a non-symmetric bilinear form, and this layer can be useful to them. There was a problem hiding this comment. It's more of a POC and I don't if we need them after some software engineering thinking. So far it can stay there and be in the way of nothing. |
||
|
|
||
| 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 | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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. | ||
|
There was a problem hiding this comment. The goal here is a quick "jump to definition"? There was a problem hiding this comment. Yes, only that. Since this is a branch so I'm a little casual about file organization and leave it by the side of the files I'm working on. There was a problem hiding this comment. I like this idea, just would like a comment in this file pointing out it it can be used this way :) |
||
| -/ | ||
| 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 | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,155 @@ | ||
| import ring_theory.algebra | ||
|
There was a problem hiding this comment. Mind adding a link to the zulip thread here? |
||
|
|
||
| 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 | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change | ||||||||||||||||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| @@ -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) | ||||||||||||||||||||||||||||||||||||||||
|
Comment on lines
+27
to
+28
There was a problem hiding this comment. What's the idea behind these? There was a problem hiding this comment. This exports a There was a problem hiding this comment. Ah, so I should read this as the python There was a problem hiding this comment. Not sure about the full extent of this, I saw this in code, check out what it seems to mean and commented it out because I thought it's not useful for our purpose. |
||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||
| local infix ⬝ := has_dot.dot | ||||||||||||||||||||||||||||||||||||||||
| local infix ∧ := has_wedge.wedge | ||||||||||||||||||||||||||||||||||||||||
|
There was a problem hiding this comment. A serious problem is that wedge is globally reserved to There was a problem hiding this comment. Can you elaborate on why right-associativity is an issue with an example? There was a problem hiding this comment. Also it conflicts with logical AND |
||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||
| -- 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 | ||||||||||||||||||||||||||||||||||||||||
|
Comment on lines
+35
to
+46
There was a problem hiding this comment. Shorter and equivalent as:
Suggested change
There was a problem hiding this comment. (unless you know a difference that I don't) |
||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||
| end geometric_algebra | ||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||
| #lint | ||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What if I have a
pointXYstructure, and I want to apply the theorems aboutPointto it?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This paragraph discusses how to do abstract reasoning without ever coming back to the concrete world. There was supposed to be a paragraph about what if we need to link back to the concrete world then that's where type classes come in. And I should also discuss using class v.s. structure (1:1 v.s. 1:n) as pointed out by Kevin Buzzard.