Zulip Chat Archive

Stream: maths

Topic: Exterior Algebra


view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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:

view this post on Zulip Adam Topaz (Aug 03 2020 at 17:20):

Same goes for the Clifford algebra.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Aug 06 2020 at 14:03):

Bourbaki is what you are looking for.

view this post on Zulip 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.

view this post on Zulip 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.

So far, it looks like this: https://github.com/leanprover-community/mathlib/blob/clifford_algebra/src/linear_algebra/clifford_algebra/basic.lean

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Aug 12 2020 at 15:32):

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

view this post on Zulip Adam Topaz (Aug 12 2020 at 15:33):

Sorry, I misread

view this post on Zulip Adam Topaz (Aug 12 2020 at 15:33):

that's exactly what you do :)

view this post on Zulip 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

view this post on Zulip Adam Topaz (Aug 12 2020 at 15:39):

Ping: @Zhangir Azerbayev

view this post on Zulip Adam Topaz (Aug 12 2020 at 15:40):

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

view this post on Zulip Adam Topaz (Aug 12 2020 at 15:42):

I think the best way to do this is to first prove something that the map
AnAA^n \to A, (a1,,an)iai(a_1,\ldots,a_n) \mapsto \prod_i a_i is RR-multilinear whenever AA is an RR-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.

view this post on Zulip Adam Topaz (Aug 12 2020 at 15:46):

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

view this post on Zulip Zhangir Azerbayev (Aug 12 2020 at 16:56):

@Utensil Song What the code you've quoted is saying is that if v0=v1v_0 = v_1 then v0i=1n+1vi=0v_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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 24 2020 at 15:45):

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

view this post on Zulip Johan Commelin (Sep 24 2020 at 15:45):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 24 2020 at 15:50):

nat.add_sub_cancel?

view this post on Zulip Johan Commelin (Sep 24 2020 at 15:51):

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

view this post on Zulip Eric Wieser (Sep 24 2020 at 15:51):

Yeah, was just typing that

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Sep 24 2020 at 15:53):

What do you think?

view this post on Zulip Eric Wieser (Sep 24 2020 at 16:00):

I think I may have just wasted an hour ;)

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Sep 24 2020 at 16:06):

Yeah I agree.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Sep 24 2020 at 16:06):

Which I hope will fall out with ring_quot

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Sep 24 2020 at 16:23):

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

view this post on Zulip Eric Wieser (Sep 24 2020 at 16:53):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Sep 24 2020 at 17:21):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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