Exterior Algebra

Stream: maths

[Adam Topaz]

@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]

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]

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

[Adam Topaz]

Same goes for the Clifford algebra.

[Eric Wieser]

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]

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]

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]

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

[Scott Morrison]

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]

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

[Utensil Song]

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

[Utensil Song]

@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]

Bourbaki is what you are looking for.

[Utensil Song]

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]

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

[Utensil Song]

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]

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

[Adam Topaz]

Sorry, I misread

[Adam Topaz]

that's exactly what you do :)

[Utensil Song]

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]

Ping: @Zhangir Azerbayev

[Adam Topaz]

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

[Adam Topaz]

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]

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]

@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]

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]

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]

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

[Johan Commelin]

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

[Eric Wieser]

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]

nat.add_sub_cancel?

[Johan Commelin]

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

[Eric Wieser]

Yeah, was just typing that

[Adam Topaz]

@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]

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]

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]

What do you think?

[Eric Wieser]

I think I may have just wasted an hour ;)

[Adam Topaz]

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]

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]

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

[Adam Topaz]

Yeah I agree.

[Eric Wieser]

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

[Eric Wieser]

Which I hope will fall out with ring_quot

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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]

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

[Eric Wieser]

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