Add a definition of blades, and prove the vectors are 1-blade and the scalars 0-blades #3
Conversation
… scalars 0-blades
| theorem zero_is_orthogonal (a : G₁) : is_orthogonal 0 a := begin | ||
| unfold is_orthogonal, | ||
| unfold sym_prod_vec, | ||
| unfold prod_vec, |
There was a problem hiding this comment.
This could be simplified to dsimp I guess.
| unfold is_orthogonal, | ||
| unfold sym_prod_vec, | ||
| unfold prod_vec, | ||
| simp |
There was a problem hiding this comment.
I kind of like to use squeeze_simp to replace the output with simp only [rw_rule1, rw_rule2, ...] to stabilize the behavior.
There was a problem hiding this comment.
| simp | |
| simp only [add_zero, zero_mul, mul_zero, add_monoid_hom.map_zero], |
| unfold is_orthogonal, | ||
| unfold sym_prod_vec, | ||
| unfold prod_vec, |
There was a problem hiding this comment.
| unfold is_orthogonal, | |
| unfold sym_prod_vec, | |
| unfold prod_vec, | |
| dsimp only [is_orthogonal, sym_prod_vec, prod_vec], |
| unfold vector.nil, | ||
| simp, |
There was a problem hiding this comment.
| unfold vector.nil, | |
| simp, | |
| simp only [vector.nil, vector.cons_tail, vector.cons_head, list.foldl], |
| | graded {n : ℕ} : | ||
| -- or a product of orthogonal vectors | ||
| (∃ (v : {l : vector G₁ (n + 1) // l.val.pairwise (λ a b, is_orthogonal a b ∧ a ≠ b)}), | ||
| b = list.foldl (λ (b : G) (a : G₁), fᵥ a * b) (fᵥ v.val.head) v.val.tail.val) |
There was a problem hiding this comment.
We could do two things here:
- use https://github.com/leanprover-community/mathlib/blob/master/src/algebra/big_operators.lean instead of the
foldlto make it look like math formula more - have a lemma to do the unfold/simp stuff, so the actual proof can focus on the real goal
There was a problem hiding this comment.
There was a problem hiding this comment.
Another approach would be to up-convert all the vectors to G and use list.prod. I suspect an explicit foldl might be easier to recourse over, but have little intuition there.
There was a problem hiding this comment.
What I had in mind was to first prove GA is a vector space, and reuse the theorems there to prove the stuff about basis, generated, span etc. I still trying to figure out how to construct stuff based on theorems.
As for graded algebra, previously I found commutative differential graded algebras to be a good reference implementation. It seems that I don't really need the bases to define the grade operations.
No description provided.