## Stream: maths

### Topic: Exterior Algebra

#### Adam Topaz (Aug 03 2020 at 16:52):

@Eric Wieser @Utensil Song I made a new branch exterior_algebra with a construction of the exterior algebra (including the universal property), as a quotient of the tensor algebra.

https://github.com/leanprover-community/mathlib/blob/exterior_algebra/src/linear_algebra/exterior_algebra.lean

#### Utensil Song (Aug 03 2020 at 17:11):

I wonder if we should replace it with the ideal one after we get bimodules & two sided ideals done. But it's really awesome to have it now! (also a good test for the tensor algebra API)

#### Adam Topaz (Aug 03 2020 at 17:19):

The exterior algebra has its own universal property, so presumably you shouldn't care about the implementation details anyway :smiling_face:

#### Adam Topaz (Aug 03 2020 at 17:20):

Same goes for the Clifford algebra.

#### Eric Wieser (Aug 04 2020 at 07:49):

One thing that's not clear to me about the current approach to this and tensor algebra - how does one split the algebra into it's constituent grades? That falls out obviously from the definition as a direct sum of tensor powers, but seems hard to reach from only the universal property.

#### Scott Morrison (Aug 04 2020 at 09:24):

I think one has to do the work --- define the submodules corresponding to the different grades (probably by induction?), show they have trivial intersection, show they span.

#### Adam Topaz (Aug 04 2020 at 12:10):

Defining the submodules is "easy". Proving that they span is also easy, by induction. But proving that they're independent (i.e. have trivial intersection, and iso to tensor powers) is harder. My approach would be to define an algebra structure on the direct sum of the tensor powers, and use lift with with universal property to prove this. After all, if two modules are independent after applying a linear map, then they were independent to begin with!

#### Adam Topaz (Aug 04 2020 at 12:11):

You can also just use lift, produce the obvious map in the other direction, and prove that they're inverses of eachother.

#### Scott Morrison (Aug 04 2020 at 12:18):

This seems a pretty reasonable strategy --- just give the alternative definition as a direct sum of tensor powers, then obtain the isomorphism with the "universal" construction.

#### Utensil Song (Aug 05 2020 at 14:08):

Should this belong to linear_algebra or somewhere else? And it seems Exterior Algebra is worth a subdirectory, same for Clifford Algebra.

#### Utensil Song (Aug 05 2020 at 14:10):

I'll attempt to mirror this PR to Clifford Algebra as an exercise, so far it seems very much possible.

#### Utensil Song (Aug 06 2020 at 13:42):

@Adam Topaz Do you have any pure math text on Exterior Algebra, Clifford Algebra or Multilinear algebra in general to follow for formalization? We have a couple of notes or texts (most targeting Mathematical Physics) on hand but are wondering a more "mathlib" choice.

#### Patrick Massot (Aug 06 2020 at 14:03):

Bourbaki is what you are looking for.

#### Utensil Song (Aug 06 2020 at 14:44):

Seems that Éléments de Mathématique Algèbre Chapitre 9 is not translated into English. Arkadiusz Jadczyk wrote a note by reading the French version last year.

#### Utensil Song (Aug 12 2020 at 15:30):

Utensil Song said:

I'll attempt to mirror this PR to Clifford Algebra as an exercise, so far it seems very much possible.

#### Utensil Song (Aug 12 2020 at 15:32):

I ported most simple lemmas mechanically, but:

1. haven't proved ι_add_swap (only stated it)
2. can't state the equivalent of wedge_self_adj* etc.

#### Adam Topaz (Aug 12 2020 at 15:32):

Oh, why don't you take a quotient of the tensor algebra instead?

Sorry, I misread

#### Adam Topaz (Aug 12 2020 at 15:33):

that's exactly what you do :)

#### Utensil Song (Aug 12 2020 at 15:39):

For 1, I have a hard time stating the subgoal, and I'm not really happy with the let ... in ... statement.

For 2, I'm quite confused by expressions like

(ν : fin q.succ → M) {j : fin q.succ} (hj : j.val = 1) (hv : ν 0 = ν j):
ι R M (ν 0) * wedge R M (λ i : fin q, ν i.succ) = 0


#### Adam Topaz (Aug 12 2020 at 15:39):

Ping: @Zhangir Azerbayev

#### Adam Topaz (Aug 12 2020 at 15:40):

I agree about 2. This should be changed in the exterior_algebra branch.

#### Adam Topaz (Aug 12 2020 at 15:42):

I think the best way to do this is to first prove something that the map
$A^n \to A$, $(a_1,\ldots,a_n) \mapsto \prod_i a_i$ is $R$-multilinear whenever $A$ is an $R$-algebra.
The componentwise composition of a multilinear map with linear maps is again multilinear, so this gives multilinearity for things like tensor_algebra.mk. One should then define alternating_map on top of multilinear_map, etc.

#### Adam Topaz (Aug 12 2020 at 15:46):

Also, I think this should all work for $K$ a commutative ring in which $2$ is invertible. (Here I'm referring to the Clifford algebra)

#### Zhangir Azerbayev (Aug 12 2020 at 16:56):

@Utensil Song What the code you've quoted is saying is that if $v_0 = v_1$ then $v_0\prod_{i = 1}^{n+1}v_i = 0$. My rationale for making that a separate lemma was not wanting to do two inductions in the proof of wedge_self_adj, but I am of course open to suggestions for how to make my code more readable or more aligned with mathlib conventions.

#### Eric Wieser (Sep 24 2020 at 14:17):

I'm going to have a go at pulling master into the exterior_algebra branch (in https://github.com/leanprover-community/mathlib/compare/eric-wieser/exterior_algebra), now that we have ring_quot. If I get it working, I assume its ok to push to your branch?

#### Eric Wieser (Sep 24 2020 at 15:37):

The updates to fin are making this painful - I'm struggling to write the proof for

ij: fin q.succ
hij: i.val + 1 = j.val
hv: ν i = ν j
hem: ¬i = 0
hj: j ≠ 0
⊢ (i.pred hem).val.succ = (j.pred hj).val


for which rw [←fin.succ_val, fin.succ_pred, fin.pred_val, ←hij, nat.pred_succ], no longer works as the definitions don't exist any more.

#### Johan Commelin (Sep 24 2020 at 15:45):

.val is deprecated. If you use coercions, everything should be smooth.

#### Johan Commelin (Sep 24 2020 at 15:45):

Lemma names that had val in them should now have corresponding versions with coe in them

#### Eric Wieser (Sep 24 2020 at 15:48):

I think that mostly did the trick, thanks - although the nat.pred_succ step of that proof seems not to work any more

#### Johan Commelin (Sep 24 2020 at 15:50):

nat.add_sub_cancel?

#### Johan Commelin (Sep 24 2020 at 15:51):

I think some .pred and .succ also changed into -1 and +1

#### Eric Wieser (Sep 24 2020 at 15:51):

Yeah, was just typing that

#### Adam Topaz (Sep 24 2020 at 15:51):

@Eric Wieser One thing to keep in mind -- @Zhangir Azerbayev was working on #3770 which was supposed to clean up some of the other work in this branch.

#### Eric Wieser (Sep 24 2020 at 15:52):

I probably won't go near the multilinear map stuff - just wanted to see how much the ring_quot change in master can remove from the branch

#### Adam Topaz (Sep 24 2020 at 15:53):

I think it makes sense to just abandon this old branch, and make a new one with just the construction of the exterior algebra as a ring_quot of the tensor algebra.

#### Adam Topaz (Sep 24 2020 at 15:53):

What do you think?

#### Eric Wieser (Sep 24 2020 at 16:00):

I think I may have just wasted an hour ;)

#### Adam Topaz (Sep 24 2020 at 16:03):

The thing is, it's unclear how long #3770 will take to be merged (if at all), and the multilinear/alternating stuff in the exterior algebra branch would have to be rewritten anyway :expressionless:

#### Eric Wieser (Sep 24 2020 at 16:04):

Given I have the branch building now (at the cost of one sorry), I think it's probably worth at least pushing it

#### Eric Wieser (Sep 24 2020 at 16:05):

If I do the ring_quot cleanup within that branch, then it makes it easier to compute a diff between "just the construction of the exterior algebra as a ring_quot of the tensor algebra." and everything else

Yeah I agree.

#### Eric Wieser (Sep 24 2020 at 16:06):

This was the sorry I couldn't resolve: https://github.com/leanprover-community/mathlib/commit/9ffe7be1ce5c0362c9ec82fe74cabc7788ca65d3#diff-fe77ce1c915c4f2a71bc47e3cdf0db97R176

#### Eric Wieser (Sep 24 2020 at 16:06):

Which I hope will fall out with ring_quot

#### Yakov Pechersky (Sep 24 2020 at 16:13):

Eric Wieser said:

The updates to fin are making this painful - I'm struggling to write the proof for

ij: fin q.succ
hij: i.val + 1 = j.val
hv: ν i = ν j
hem: ¬i = 0
hj: j ≠ 0
⊢ (i.pred hem).val.succ = (j.pred hj).val


for which rw [←fin.succ_val, fin.succ_pred, fin.pred_val, ←hij, nat.pred_succ], no longer works as the definitions don't exist any more.

Here:

lemma fin.pos_of_ne {n : ℕ} {i : fin (n + 1)} (h : i ≠ 0) : 0 < i :=
lt_of_le_of_ne (fin.zero_le i) h.symm

lemma nat.sub_add_one {n : ℕ} (hpos : 0 < n) : n - 1 + 1 = n :=
begin
cases n,
{ exact absurd hpos (lt_irrefl 0) },
simp only [nat.succ_sub_succ_eq_sub, nat.sub_zero],
end

example {q : ℕ} {v : fin q.succ → ℕ} (i j : fin q.succ) (hij : i.val + 1 = j.val)
(hv : v i = v j) (hem : i ≠ 0) (hj : j ≠ 0) :
(i.pred hem).val.succ = (j.pred hj).val :=
begin
simp only [fin.val_eq_coe] at hij,
simp only [←hij, nat.add_succ_sub_one, add_zero, fin.val_eq_coe, fin.coe_pred],
exact nat.sub_add_one (fin.lt_iff_coe_lt_coe.mp (fin.pos_of_ne hem)),
end


#### Eric Wieser (Sep 24 2020 at 16:15):

Thanks @Yakov Pechersky, although I was able to get what I needed with @Johan Commelin's help above

#### Yakov Pechersky (Sep 24 2020 at 16:23):

Do you mind sharing how you solved that? I've been trying to shore up fin API, especially where there are swaps etc involved.

#### Yakov Pechersky (Sep 24 2020 at 16:23):

In general, one shouldn't have to have states where .val appears any more.

#### Eric Wieser (Sep 24 2020 at 16:53):

Yes, the fix was to remove the .val from my lemma statement

#### Eric Wieser (Sep 24 2020 at 17:21):

@Adam Topaz, I pushed the fixes to run against lean /mathlib master to https://github.com/leanprover-community/mathlib/compare/exterior_algebra

#### Eric Wieser (Sep 24 2020 at 17:21):

Do you want me to push ring_quot there too if I get it working?

#### Eric Wieser (Sep 28 2020 at 10:40):

Adam Topaz said:

I think it makes sense to just abandon this old branch, and make a new one with just the construction of the exterior algebra as a ring_quot of the tensor algebra.

#4297

#### Eric Wieser (Oct 02 2020 at 10:24):

rss-bot said:

feat(linear_algebra/exterior_algebra): Add an exterior algebra (#4297)
feat(linear_algebra/exterior_algebra): Add an exterior algebra (#4297)

This adds the basic exterior algebra definitions using a very similar approach to universal_enveloping_algebra.
It's based off the exterior_algebra branch, dropping the wedge stuff for now as development in multilinear maps is happening elsewhere.

Co-authored-by: Adam Topaz <github@adamtopaz.com>
Co-authored-by: Zhangir Azerbayev <zazerbayev@gmail.com>
https://github.com/leanprover-community/mathlib/commit/13e9cc4acf0ba7327e244d1eda8818a808013ec4

docs#exterior_algebra . I've merged master into your branch#exterior_algebra branch @Adam Topaz and @Zhangir Azerbayev, although the build fails for the same reason as #4289.

#### Eric Wieser (Oct 20 2020 at 18:54):

I've pushed to the branch again, this time to remove the work that duplicates docs#multilinear_map.mk_pi_algebra_fin

#### Eric Wieser (Dec 03 2020 at 18:04):

Having looked at the branch again, I think all that's left is a tensor_algebra.ι_multi to mirror docs#exterior_algebra.ι_multi, and some permutation stuff that is already in #3770

Last updated: May 12 2021 at 08:14 UTC