Zulip Chat Archive

Stream: Is there code for X?

Topic: Ideals over algebras


view this post on Zulip Eric Wieser (Jul 29 2020 at 17:21):

There's already code for ideals (over commutative rings), but there's nothing for ideals over algebras.

subalgebra does most of the heavy lifting, but the API seems either lacking or hard for me to follow.

As an example of the type of thing I want in mathlib somewhere:

-- produce the setoid corresponding to the ideal of a subalgebra
def setoid_ideal_of_subalgebra
  {R : Type u} {A : Type u} [comm_ring R] [ring A] [algebra R A]
  (s : subalgebra R A) : setoid A
:= {
  r := λ a b, a - b  s,
  iseqv := 
    λ a, by {rw sub_self, exact subalgebra.zero_mem _},
    λ a b h, by {rw neg_sub, exact subalgebra.neg_mem _ h},
    λ a b c hab hbc, by {
      have hac := subalgebra.add_mem _ hab hbc,
      rw [add_sub, sub_add, sub_self, sub_zero] at hac,
      exact hac,
    }}

instance : has_scalar R (quotient (setoid_ideal_of_subalgebra sorry)) := {
  smul := λ k v, quotient.lift_on v
    (λ v, has_scalar.smul k v)
    $ λ _ _ H, quotient.sound
    $ begin
      change _  _,
      rw  smul_sub,
      refine subalgebra.smul_mem _ H _,
    end}

view this post on Zulip Eric Wieser (Jul 29 2020 at 17:22):

Apologies in advance, my terminology is likely a little off the mark

view this post on Zulip Johan Commelin (Jul 29 2020 at 17:26):

Hmm? Why are you using setoid?

view this post on Zulip Johan Commelin (Jul 29 2020 at 17:26):

I'm confused about the kind of maths that you want

view this post on Zulip Reid Barton (Jul 29 2020 at 17:26):

I think probably just the quotient R-module

view this post on Zulip Reid Barton (Jul 29 2020 at 17:27):

being a subalgebra (closed under *) isn't useful for any sort of quotient I think

view this post on Zulip Eric Wieser (Jul 29 2020 at 17:27):

I think I'm looking for subalgebra.quotient, given the alraedy-existing docs#submodule.quotient

view this post on Zulip Reid Barton (Jul 29 2020 at 17:28):

You need an ideal for that

view this post on Zulip Eric Wieser (Jul 29 2020 at 17:29):

My ideal is the sorry in the above snippet

view this post on Zulip Eric Wieser (Jul 29 2020 at 17:29):

I think

view this post on Zulip Eric Wieser (Jul 29 2020 at 17:30):

Would a patch be accepted that copied docs#submodule.quotient and docs#submodule.quotient_rel to subalgebra.quotient and subalgebra.quotient_rel, and tweaked the associated proofs?

view this post on Zulip Reid Barton (Jul 29 2020 at 17:30):

You have an RR-algebra AA and a subalgebra SS of AA, what do you want to construct in math?

view this post on Zulip Eric Wieser (Jul 29 2020 at 17:31):

To un-#xy, I want to construct the clifford algebra from the tensor algebra

view this post on Zulip Eric Wieser (Jul 29 2020 at 17:31):

I pretty much have what I need, but I had to build too much of it just for this use case

view this post on Zulip Reid Barton (Jul 29 2020 at 17:31):

That's a quotient by an ideal, right?

view this post on Zulip Eric Wieser (Jul 29 2020 at 17:31):

Yes, I think so

view this post on Zulip Reid Barton (Jul 29 2020 at 17:31):

I guess I'm confused by (s : subalgebra R A) then

view this post on Zulip Eric Wieser (Jul 29 2020 at 17:32):

s is my ideal, but the type isn't quite right

view this post on Zulip Eric Wieser (Jul 29 2020 at 17:32):

I can't actually use ideal A, because A is not commutative

view this post on Zulip Reid Barton (Jul 29 2020 at 17:32):

Ah I see

view this post on Zulip Eric Wieser (Jul 29 2020 at 17:33):

I suppose an ideal is stricter than just a subalgebra though, but it seems I haven't actually needed the quotient to be an ideal yet...

view this post on Zulip Reid Barton (Jul 29 2020 at 17:35):

you need it for multiplication

view this post on Zulip Reid Barton (Jul 29 2020 at 17:38):

I don't think we have two-sided ideals

view this post on Zulip Reid Barton (Jul 29 2020 at 17:42):

In general, noncommutative algebra is underdeveloped.

view this post on Zulip Mario Carneiro (Jul 29 2020 at 17:50):

Are you telling me that not all rings are commutative? They lied to me!

view this post on Zulip Adam Topaz (Jul 29 2020 at 17:53):

I think you need to take the two-sided ideal generated by things of the form v2Q(v)1v^2 - Q(v) \cdot 1 where QQ is your quadratic form.
This is inside the tensor algebra of VV over KK.

view this post on Zulip Adam Topaz (Jul 29 2020 at 17:53):

The Clifford algebra would be the quotient by this two-sided ideal.

view this post on Zulip Eric Wieser (Jul 29 2020 at 17:53):

Yeah, that's what I'm doing, except I'd hoped I could call it a subalgebra not an ideal

view this post on Zulip Eric Wieser (Jul 29 2020 at 17:53):

I've since been told I should know better than to try that!

view this post on Zulip Eric Wieser (Jul 29 2020 at 17:54):

(I'm building on top of your PR, @Adam Topaz)

view this post on Zulip Adam Topaz (Jul 29 2020 at 17:54):

It's not a subalgebra, since it doesn't contain 11.

view this post on Zulip Eric Wieser (Jul 29 2020 at 17:54):

The cdot 1 there is just a coe, right?

view this post on Zulip Johan Commelin (Jul 29 2020 at 17:55):

Mario Carneiro said:

Are you telling me that not all rings are commutative? They lied to me!

Only non-commutative rings are non-commutative...

view this post on Zulip Adam Topaz (Jul 29 2020 at 17:56):

The Q(v)1Q(v) \cdot 1 is the same as the map from the base field. But I don't think I introduced this coersion in the PR you're looking at.

view this post on Zulip Eric Wieser (Jul 29 2020 at 17:56):

I'm currently using

def ga_ideal : subalgebra R (pre Q) := algebra.adjoin R {
  i |  v, univ R M v * univ R M v - algebra_map R (pre Q) (Q v) = i
}

view this post on Zulip Eric Wieser (Jul 29 2020 at 17:57):

where pre Q is tensor_algebra R M

view this post on Zulip Eric Wieser (Jul 29 2020 at 17:57):

Which as you annoyingly point out, is wrong because an ideal is not a subalgebra

view this post on Zulip Adam Topaz (Jul 29 2020 at 18:04):

I'm fairly sure mathlib has quotients of rings by two sided ideals, so I don't think the whole pre dance is necessary here.

view this post on Zulip Adam Topaz (Jul 29 2020 at 18:05):

wait. I'm confused. Whats going on there?

view this post on Zulip Adam Topaz (Jul 29 2020 at 18:05):

Are you sure you want to adjoin things?

view this post on Zulip Adam Topaz (Jul 29 2020 at 18:06):

This is an over-ring of the tensor algebra.

view this post on Zulip Reid Barton (Jul 29 2020 at 18:06):

oh, I didn't even find two-sided ideals

view this post on Zulip Eric Wieser (Jul 29 2020 at 18:07):

I'm fairly sure mathlib has quotients of rings by two sided ideals

Yeah, I couldn't find these

view this post on Zulip Adam Topaz (Jul 29 2020 at 18:08):

Well, that's a problem...

view this post on Zulip Eric Wieser (Jul 29 2020 at 18:08):

Are you sure you want to adjoin things?

No, I definitely don't - I was just looking for the a plausible subalgebra constructor

view this post on Zulip Eric Wieser (Jul 29 2020 at 18:08):

When in fact I should not have been

view this post on Zulip Adam Topaz (Jul 29 2020 at 18:08):

What you can do is define a relation using the generators of the ideal, compatibility with addition, multiplication, etc., and take the quotient by that.

view this post on Zulip Adam Topaz (Jul 29 2020 at 18:09):

But in reality, mathlib should have code for:

  1. two-sided ideals.
  2. two-sided ideals generated by some set.
  3. quotients by two-sided iddeals.

view this post on Zulip Mario Carneiro (Jul 29 2020 at 18:12):

two-sided ideals form a closure system (they are closed under arbitrary intersection), so you get ideal spans for free. As for quotients, you can quotient by an arbitrary set, and prove that the kernel of such a quotient is a two sided ideal

view this post on Zulip Mario Carneiro (Jul 29 2020 at 18:12):

namely the ideal span of the input set

view this post on Zulip Adam Topaz (Jul 29 2020 at 18:14):

How do you take the quotient by a set? You have to define some relation which identifies the elements of the set with 00, and ensures compatibility with the algebra operations. Does mathlib already have some code to do this?

view this post on Zulip Alex J. Best (Jul 29 2020 at 18:20):

There is quot for quotients by arbitrary relations, quotient for equivalence relations, and for additive groups quotient_add_group

view this post on Zulip Eric Wieser (Jul 29 2020 at 18:21):

There's submodule.quotient too

view this post on Zulip Adam Topaz (Jul 29 2020 at 18:24):

Sure, you can define a relation like this:

variables (A : Type*) [ring A]

inductive rel (S : set A) : A  A  Prop
| of {s} : s  S  rel s 0
| add_compat_left {a b c} : rel a b  rel (a + c) (b + c)
| add_compat_right {a b c} : rel a b  rel (c + a) (c + b)
| mul_compat_left {a b c} : rel a b  rel (a * c) (b * c)
| mul_compat_right {a b c} : rel a b  rel (c * a) (c * b)

What I'm wondering is whether mathlib already has some code to automate this.

view this post on Zulip Eric Wieser (Jul 29 2020 at 18:26):

Are you looking for submodule.closure or something?

view this post on Zulip Eric Wieser (Jul 29 2020 at 18:27):

Nevermind, missed the mul

view this post on Zulip Adam Topaz (Jul 29 2020 at 18:27):

When you take quotby such a relation, you get the quotient of the ring AA by the two-sided ideal generated by SS.

view this post on Zulip Adam Topaz (Jul 29 2020 at 18:45):

I guess you can get by with the submodule (with a left action) closure of the set of all elements of the form sas \cdot a where sSs\in S and aAa\in A.

view this post on Zulip Eric Wieser (Jul 30 2020 at 10:28):

Seems like the way to go here is make ideal not defeq submodule, but instead extending add_subgroup

I've made a start on this locally, and spawned the trivial PR #3631

view this post on Zulip Eric Wieser (Jul 30 2020 at 11:48):

This turns out to be quite a massive undertaking, as every lemma about add_subgroup has to be wrapped

view this post on Zulip Kevin Buzzard (Jul 30 2020 at 11:54):

Does submodule not extend add_subgroup?

view this post on Zulip Kevin Buzzard (Jul 30 2020 at 11:55):

Does submodule not extend add_subgroup?

view this post on Zulip Eric Wieser (Jul 30 2020 at 12:25):

Yes, I suppose it does (well, add_submonoid, which sort of implies add_subgroup if add_group is around somewhere)

view this post on Zulip Eric Wieser (Jul 30 2020 at 12:26):

PR so far is at #3635

view this post on Zulip Eric Wieser (Jul 30 2020 at 12:27):

Most of the tedious work is taking the proof in submodule and replacing statements about mem_smul with either mem_mul_left or mem_mul_right

view this post on Zulip Adam Topaz (Jul 30 2020 at 13:22):

@Eric Wieser , have you considered doing something like this?

import algebra

variables (A : Type*) [ring A]

structure two_sided_ideal extends submodule A A :=
(right_mul {a b : A} : b  carrier  b * a  carrier)

view this post on Zulip Adam Topaz (Jul 30 2020 at 13:30):

Of course, the mathematically correct way to do this is to define bimodules, so that two sided ideals are sub-bimodules of the ring.

https://en.m.wikipedia.org/wiki/Bimodule

view this post on Zulip Kevin Buzzard (Jul 30 2020 at 13:32):

Does submodule not extend add_subgroup?

view this post on Zulip Adam Topaz (Jul 30 2020 at 13:33):

It does I think

view this post on Zulip Adam Topaz (Jul 30 2020 at 13:35):

src#submodule

view this post on Zulip Adam Topaz (Jul 30 2020 at 13:35):

add_submonoid

view this post on Zulip Kevin Buzzard (Jul 30 2020 at 13:37):

Sorry, I have ropey internet right now, hence multiple messages (I only posted once). A submonoid of a module is not the same as a subgroup, but when you add the ring action you can use a multiplication by -1 trick to show they're the same.

view this post on Zulip Adam Topaz (Jul 30 2020 at 13:37):

Oh yeah Eric mentioned this above

view this post on Zulip Adam Topaz (Jul 30 2020 at 13:38):

Yes of course.

view this post on Zulip Adam Topaz (Jul 30 2020 at 13:39):

But the same argument works also for right and left modules

view this post on Zulip Eric Wieser (Jul 30 2020 at 15:23):

Just to be clear, the bimodule route would look something like:

  • Rename the current semimodule to semileftmodule
  • Rename the current submodule to leftsubmodule
  • Create copies of all the left code for right
  • Create bimodule as extends semileftmodule, semirightmodule
  • Create subbimodule similarly
  • alias semimodule R M to semibimodule R R M
  • alias submodule R M to subbimodule R R M
  • split has_smul into has_right_smul and has_left_smul
  • ...

This feels like a very substantial amount of work

view this post on Zulip Adam Topaz (Jul 30 2020 at 15:32):

Another approach is to define an ABAB-bimodule as a (left) module over ABopA \otimes B^{op}.

view this post on Zulip Adam Topaz (Jul 30 2020 at 15:34):

So a two-sided ideal in AA is a submodule of AA considered as a module over AAopA \otimes A^{op} where a basic tensor aba \otimes b acts on xAx \in A as axba \cdot x \cdot b.

view this post on Zulip Jalex Stark (Jul 30 2020 at 15:40):

the best implementation of the left_ and right_ approach probably requires metaprogramming (cf. to_additive)

view this post on Zulip Eric Wieser (Jul 30 2020 at 15:40):

Yeah, I was thinking the same

view this post on Zulip Adam Topaz (Jul 30 2020 at 15:41):

There may also be notation issues with a right scalar multiplication...

view this post on Zulip Eric Wieser (Jul 30 2020 at 15:41):

Frankly, looking at subgroup vs submonoid, it feels like there's already a dire need for metaprogramming

view this post on Zulip Eric Wieser (Jul 30 2020 at 15:42):

So many of the lemmas and they're proofs are textually identical other than the type names

view this post on Zulip Eric Wieser (Jul 30 2020 at 15:42):

But of course some_lemma in one file is not the same lemma as some_lemma in the other file

view this post on Zulip Eric Wieser (Jul 30 2020 at 15:42):

So a proof that is by simp only [some_lemma] still has to be repeated

view this post on Zulip Eric Wieser (Jul 30 2020 at 15:44):

#3634 is a good example, the lemmas there are copy-pasted

view this post on Zulip Adam Topaz (Jul 30 2020 at 15:51):

import ring_theory.tensor_product

open_locale tensor_product

variables (A : Type*) [semiring A]
variables (B : Type*) [semiring B]
variables (M : Type*) [add_comm_monoid M]

#check semimodule (A [] Bᵒᵖ) M

view this post on Zulip Adam Topaz (Jul 30 2020 at 15:53):

Unfortunately

example : semimodule (A [] Aᵒᵖ) A := by apply_instance -- fails

view this post on Zulip Utensil Song (Aug 03 2020 at 07:37):

@Adam Topaz @Eric Wieser

I wonder if we really need the ideal. Could we just use quotient type like in the tensor_algebra code?

view this post on Zulip Utensil Song (Aug 03 2020 at 07:37):

I have a #mwe which is not working yet:

import linear_algebra.tensor_algebra
import linear_algebra.quadratic_form

variables (R : Type*) [field R]
variables (M : Type*) [add_comm_group M] [module R M] [quadratic_form R M]

namespace clifford_algebra

open tensor_algebra

instance : has_coe (pre R M) (tensor_algebra R M) := quot.mk _⟩

inductive cliff_rel : (pre R M)  (pre R M)  Prop
-- clifford equiv
| contraction {v : M} [qv: quadratic_form R M] : cliff_rel ((pre.mul (pre.of v) (pre.of v))) ((pre.of_scalar (qv v)))

end clifford_algebra

/-
failed to synthesize type class instance for
R : Type u_1,
_inst_1 : field R,
M : Type u_2,
_inst_2 : add_comm_group M,
_inst_3 : module R M,
_inst_4 : quadratic_form R M
⊢ quadratic_form R M
-/
def clifford_algebra := quot (clifford_algebra.cliff_rel R M)

view this post on Zulip Utensil Song (Aug 03 2020 at 07:40):

Q1: How to "inherit" an inductive type?

Namely tensor_algebra.rel here, so that the final cliff_refwill contain what's in rel and also some additional equivalencies.

view this post on Zulip Utensil Song (Aug 03 2020 at 07:41):

Q2: Why "failed to synthesize type class instance" for quadratic_form when there's already quadratic_form?

view this post on Zulip Eric Wieser (Aug 03 2020 at 07:44):

Q2: quadratic_form is not a class, so will not be inferred

view this post on Zulip Eric Wieser (Aug 03 2020 at 07:45):

I'd make qv an argument of cliff_rel or pre instead

view this post on Zulip Utensil Song (Aug 03 2020 at 07:49):

Q3: How to use the contractors in tensor_algebra.pre like of or of_scalar? They seem to disappear after the quotient.

view this post on Zulip Scott Morrison (Aug 03 2020 at 08:02):

I think you shouldn't attempt to use the constructors. Indeed, after the universal property has been defined no one should ever interact with .pre again.

view this post on Zulip Eric Wieser (Aug 03 2020 at 08:17):

Should pre be marked private then?

view this post on Zulip Eric Wieser (Aug 03 2020 at 08:18):

of is exposed as \iota, of_scalar is algebra_map K T I guess

view this post on Zulip Kenny Lau (Aug 03 2020 at 08:43):

Eric Wieser said:

Just to be clear, the bimodule route would look something like:

  • Rename the current semimodule to semileftmodule
  • Rename the current submodule to leftsubmodule
  • Create copies of all the left code for right
  • Create bimodule as extends semileftmodule, semirightmodule
  • Create subbimodule similarly
  • alias semimodule R M to semibimodule R R M
  • alias submodule R M to subbimodule R R M
  • split has_smul into has_right_smul and has_left_smul
  • ...

This feels like a very substantial amount of work

In the future, module will be renamed into left_noncommunitalsemiring_addcommgroup_module

view this post on Zulip Eric Wieser (Aug 03 2020 at 08:53):

It does feel like there are a lot of places where wikipedia / wolfram defines something over a ring, but then mathlib says "actually a semiring is enough" and either ends up with X and semiX, or needs [ring K] [X K ...]to get the definition used by others. Is there any consensus on which of these two options is preferred?

view this post on Zulip Adam Topaz (Aug 03 2020 at 12:26):

What's the problem with defining bimodules as modules over ABopA \otimes B^{op}?

view this post on Zulip Adam Topaz (Aug 03 2020 at 12:29):

And yeah, one should never use pre. Iota is not exactly of, but rather it's the composition of of with the quotient map

view this post on Zulip Utensil Song (Aug 03 2020 at 12:41):

I didn't want to use pre initially. But it seems that there's no similar way to construct the tensor algebra after the quotient.

view this post on Zulip Adam Topaz (Aug 03 2020 at 12:44):

Anything you can do with pre, you can do by using iota, the algebra_map, and the ring structure of the tensor algebra.

view this post on Zulip Adam Topaz (Aug 03 2020 at 12:45):

Sorry, I meant to say the semiring structure of the tensor algebra :wink:

view this post on Zulip Utensil Song (Aug 03 2020 at 12:48):

I see. One can only access it as what it is (after the quotient), but not what it was (before the quotient). I was confused by not seeing the general pattern.

view this post on Zulip Adam Topaz (Aug 03 2020 at 12:50):

Are you trying to define the Clifford algebra?

view this post on Zulip Utensil Song (Aug 03 2020 at 12:50):

Adam Topaz said:

What's the problem with defining bimodules as modules over ABopA \otimes B^{op}?

That route seems fine. I was trying to figure out if it's the only way and if one more concept is necessary.

view this post on Zulip Utensil Song (Aug 03 2020 at 12:50):

Yes, @Eric Wieser and I are working on this.

view this post on Zulip Utensil Song (Aug 03 2020 at 12:51):

Utensil Song said:

Q1: How to "inherit" an inductive type?

Namely tensor_algebra.rel here, so that the final cliff_refwill contain what's in rel and also some additional equivalencies.

Any comments on Q1?

view this post on Zulip Adam Topaz (Aug 03 2020 at 12:54):

If you start by defining your relation on the tensor algebra itself, those relations already hold true!

view this post on Zulip Adam Topaz (Aug 03 2020 at 12:55):

So I suggest defining your cliff_rel as a relation on the tensor algebra

view this post on Zulip Utensil Song (Aug 03 2020 at 12:56):

Kenny Lau said:

Eric Wieser said:

Just to be clear, the bimodule route would look something like:

  • Rename the current semimodule to semileftmodule
  • Rename the current submodule to leftsubmodule
  • Create copies of all the left code for right
  • Create bimodule as extends semileftmodule, semirightmodule
  • Create subbimodule similarly
  • alias semimodule R M to semibimodule R R M
  • alias submodule R M to subbimodule R R M
  • split has_smul into has_right_smul and has_left_smul
  • ...

This feels like a very substantial amount of work

In the future, module will be renamed into left_noncommunitalsemiring_addcommgroup_module

@Eric Wieser Have you heard of The red herring principle?

I'm afraid the inaccuracies of the names are inevitable, one has to settle on what's short and about right.

view this post on Zulip Utensil Song (Aug 03 2020 at 12:58):

Adam Topaz said:

If you start by defining your relation on the tensor algebra itself, those relations already hold true!

I tried that first, then stuck at Q3 so I fell back to pre. Now as Q3 is resolved, it seems that I can go back on that route.

view this post on Zulip Utensil Song (Aug 03 2020 at 13:01):

But I'm still seeking a general pattern here, about "inheriting" an inductive type.

view this post on Zulip Adam Topaz (Aug 03 2020 at 13:04):

import linear_algebra.quadratic_form
import linear_algebra.tensor_algebra

variables (K : Type*) [field K]
variables (V : Type*) [add_comm_group V] [module K V]
variables (Q : quadratic_form K V)

open tensor_algebra

inductive cliff_rel : tensor_algebra K V  tensor_algebra K V  Prop
| of {v : V} :  cliff_rel ((ι K V v) * (ι K V v)) (algebra_map _ _ (Q v))
| add_compat {x y z} : cliff_rel x y  cliff_rel (x + z) (y + z)
| mul_compat_left {x y z} : cliff_rel x y  cliff_rel (x * z) (y * z)
| mul_compat_right {x y z} : cliff_rel x y  cliff_rel (z * x) (z * y)

def clifford_algebra := quot (cliff_rel K V Q)

view this post on Zulip Utensil Song (Aug 03 2020 at 13:12):

Where're the *compat* coming from?

view this post on Zulip Utensil Song (Aug 03 2020 at 13:13):

What's the convention of using of? (Maybe it hints that this is the essence of the definition?)

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

The compat stuff ensures the quotient inherits a ring structure from the tensor algebra.

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

Of is because these are essentially the generators of the ideal.

view this post on Zulip Utensil Song (Aug 03 2020 at 13:20):

How much is the definition above (without ideal) different from the one with ideal? Mostly technical, I presume?

view this post on Zulip Adam Topaz (Aug 03 2020 at 13:24):

This is the relation that generates the equivalence relation you would get from the two sided ideal. But mathlib doesn't (yet) have two sided ideals...

view this post on Zulip Utensil Song (Aug 03 2020 at 13:27):

What's your plan after working on tensor algebra?

view this post on Zulip Adam Topaz (Aug 03 2020 at 13:28):

I would be happy to help you with the Clifford algebra, if you like. I did the tensor algebra stuff because someone mentioned they needed the exterior algebra for something, and I think Scott suggested to define the tensor algebra first.

view this post on Zulip Utensil Song (Aug 03 2020 at 13:32):

Yes, we would really appreciate that! We would like to work on Clifford algebra and it would be awesome to have more guidance on how to do it mathematically correctly and possibly a roadmap with sorry and we'll try to work out the details.

view this post on Zulip Utensil Song (Aug 03 2020 at 13:33):

The path might be: two sided ideals -> Grassmann Algebra -> Clifford Algebra

view this post on Zulip Patrick Massot (Aug 03 2020 at 13:34):

About the motivation for exterior algebras, I think the main expected milestone is to get differential forms.

view this post on Zulip Adam Topaz (Aug 03 2020 at 13:42):

I agree differential forms are the main motivation. I would eventually also like to define Milnor K-theory, which is defined as a certain quotient of the tensor algebra (and is related to logarithmic differential forms).

view this post on Zulip Utensil Song (Aug 03 2020 at 13:42):

The natural next step for Geometric Algebra (a reformulation from Clifford Algebra mainly for geometric applications) is Geometric Calculus and somewhere in the middle we'll need to have differential forms. But Grassmann Algebra, on its own, also has many important geometric applications that we're interested in.

view this post on Zulip Eric Wieser (Aug 03 2020 at 14:03):

@Adam Topaz, that code sample above is missing a function to lift a scalar to the algebra, right?

view this post on Zulip Adam Topaz (Aug 03 2020 at 14:05):

No, the scalar action is just multiplication in an algebra

view this post on Zulip Eric Wieser (Aug 03 2020 at 14:06):

I'm probably missing something silly then - how would I define the canonical K → clifford_algebra K V Q function?

view this post on Zulip Adam Topaz (Aug 03 2020 at 14:07):

Compose the algebra map to the tensor algebra and the quotient map

view this post on Zulip Eric Wieser (Aug 03 2020 at 14:09):

Ah, I was forgetting that a quotient map is implemented

view this post on Zulip Utensil Song (Aug 03 2020 at 17:04):

@maintainers could I (github username utensil have push access to non-master branches of mathlib? @Eric Wieser and I plan to work on Clifford Algebra and its dependencies. Thanks!

view this post on Zulip Simon Hudon (Aug 03 2020 at 17:56):

Done

view this post on Zulip Utensil Song (Aug 03 2020 at 17:58):

Thanks! @Simon Hudon

view this post on Zulip Scott Morrison (Aug 03 2020 at 22:44):

Another thing we should do now that we have the tensor algebra is define the universal enveloping algebra of a Lie algebra (@Oliver Nash?), prove the universal property, and show that it preserves representation categories.

view this post on Zulip Oliver Nash (Aug 04 2020 at 18:06):

I have had this same thought @Scott Morrison and had been anxiously waiting for the tensor algebra PR to merge for this reason. Unfortunately however I am likely to have a lot less time for Mathlib for the next month or two so I personally don't expect to PR this (or much at all) in the near future.


Last updated: May 19 2021 at 02:10 UTC