[WIP] New Design #8
Conversation
| 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 |
There was a problem hiding this comment.
What if I have a pointXY structure, and I want to apply the theorems about Point to it?
There was a problem hiding this comment.
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.
|
|
||
| /-- | ||
| -/ | ||
| @[ancestor algebra] |
There was a problem hiding this comment.
What does this do that isn't covered by extends?
There was a problem hiding this comment.
Still trying to figure out the exact effect, it shows up in group.defs in mathlib
There was a problem hiding this comment.
Yeah, I've seen it before too, was hoping you'd worked out its meaning since I haven't yet...
| 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 :)
| (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 ) |
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.
| 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
|
|
||
| ```lean | ||
| class has_wedge (α : Type u) := (wedge : α → α → α) | ||
| class has_inner (α : Type u) := (inner : α → α → α) |
There was a problem hiding this comment.
has_inner assumes the result is real. It could be a more concrete instance of the general has_dot we have.
|
|
||
| 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 gmul doesn't scale well, Scalar Product can't be smul because it's used by has_scalar which would be in our inheritance hierarchy.
There was a problem hiding this comment.
Can't we have geometric_algebra.has_scalar_product.smul to distinguish from has_scalar.smul? Or do namespaces not work well here?
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.
| -- export has_wedge (wedge) | ||
|
|
||
| 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 infixr which has right associativity and conflicts with our wedge. local only evaded the problem temporarily.
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
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
| ```lean | ||
| class has_ga_wedge (α : Type u) extends has_wedge := | ||
| (defeq : ∀ a b : α, a ∧ b = (a ∘ b - b ∘ a) / 2) | ||
| ``` |
| (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 |
There was a problem hiding this comment.
has_geom_prod will return here. Haven't figure out how to and how it surves the purpose yet.
| 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] |
There was a problem hiding this comment.
It seems that I can't leave them to variables because that would cause failure to use either semi_geometric_algebra G or semi_geometric_algebra R V G. They still stick here.
for unbundled, V_bundled and namespace VR_bundled. There's no way to bundle R only.
| 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 |
There was a problem hiding this comment.
Shorter and equivalent as:
| 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 | |
| local infix ` ⊛ `:70 := has_scalar_prod.scalar_prod | |
| local infix ` ⊙ `:70 := has_symm_prod.symm_prod | |
| local infix ` ⊠ `:70 := has_asymm_prod.asymm_prod | |
| local infix ` ⨼ `:70 := has_left_contract.left_contract | |
| local infix ` ⨽ `:70 := has_right_contract.right_contract |
There was a problem hiding this comment.
(unless you know a difference that I don't)
| -- export has_dot (dot) | ||
| -- export has_wedge (wedge) |
There was a problem hiding this comment.
What's the idea behind these?
There was a problem hiding this comment.
This exports a wedge function, without has_wedge.
There was a problem hiding this comment.
Ah, so I should read this as the python wedge = has_wedge.wedge?
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.
| @@ -0,0 +1,155 @@ | |||
| import ring_theory.algebra | |||
There was a problem hiding this comment.
Mind adding a link to the zulip thread here?
Work-in-progress.