# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Ideals over algebras

#### Eric Wieser (Jul 29 2020 at 17:21):

There's already code for `ideal`

s (over commutative rings), but there's nothing for ideals over `algebra`

s.

`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}
```

#### Eric Wieser (Jul 29 2020 at 17:22):

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

#### Johan Commelin (Jul 29 2020 at 17:26):

Hmm? Why are you using `setoid`

?

#### Johan Commelin (Jul 29 2020 at 17:26):

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

#### Reid Barton (Jul 29 2020 at 17:26):

I think probably just the quotient R-module

#### Reid Barton (Jul 29 2020 at 17:27):

being a subalgebra (closed under `*`

) isn't useful for any sort of quotient I think

#### Eric Wieser (Jul 29 2020 at 17:27):

I think I'm looking for `subalgebra.quotient`

, given the alraedy-existing docs#submodule.quotient

#### Reid Barton (Jul 29 2020 at 17:28):

You need an ideal for that

#### Eric Wieser (Jul 29 2020 at 17:29):

My ideal is the `sorry`

in the above snippet

#### Eric Wieser (Jul 29 2020 at 17:29):

I think

#### 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?

#### Reid Barton (Jul 29 2020 at 17:30):

You have an $R$-algebra $A$ and a subalgebra $S$ of $A$, what do you want to construct in math?

#### Eric Wieser (Jul 29 2020 at 17:31):

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

#### 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

#### Reid Barton (Jul 29 2020 at 17:31):

That's a quotient by an ideal, right?

#### Eric Wieser (Jul 29 2020 at 17:31):

Yes, I think so

#### Reid Barton (Jul 29 2020 at 17:31):

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

then

#### Eric Wieser (Jul 29 2020 at 17:32):

`s`

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

#### Eric Wieser (Jul 29 2020 at 17:32):

I can't actually use `ideal A`

, because `A`

is not commutative

#### Reid Barton (Jul 29 2020 at 17:32):

Ah I see

#### 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...

#### Reid Barton (Jul 29 2020 at 17:35):

you need it for multiplication

#### Reid Barton (Jul 29 2020 at 17:38):

I don't think we have two-sided ideals

#### Reid Barton (Jul 29 2020 at 17:42):

In general, noncommutative algebra is underdeveloped.

#### Mario Carneiro (Jul 29 2020 at 17:50):

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

#### Adam Topaz (Jul 29 2020 at 17:53):

I think you need to take the two-sided ideal generated by things of the form $v^2 - Q(v) \cdot 1$ where $Q$ is your quadratic form.

This is inside the tensor algebra of $V$ over $K$.

#### Adam Topaz (Jul 29 2020 at 17:53):

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

#### 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

#### Eric Wieser (Jul 29 2020 at 17:53):

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

#### Eric Wieser (Jul 29 2020 at 17:54):

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

#### Adam Topaz (Jul 29 2020 at 17:54):

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

#### Eric Wieser (Jul 29 2020 at 17:54):

The `cdot 1`

there is just a `coe`

, right?

#### 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...

#### Adam Topaz (Jul 29 2020 at 17:56):

The $Q(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.

#### 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
}
```

#### Eric Wieser (Jul 29 2020 at 17:57):

where `pre Q`

is `tensor_algebra R M`

#### Eric Wieser (Jul 29 2020 at 17:57):

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

#### 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.

#### Adam Topaz (Jul 29 2020 at 18:05):

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

#### Adam Topaz (Jul 29 2020 at 18:05):

Are you sure you want to adjoin things?

#### Adam Topaz (Jul 29 2020 at 18:06):

This is an over-ring of the tensor algebra.

#### Reid Barton (Jul 29 2020 at 18:06):

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

#### 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

#### Adam Topaz (Jul 29 2020 at 18:08):

Well, that's a problem...

#### 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

#### Eric Wieser (Jul 29 2020 at 18:08):

When in fact I should not have been

#### 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.

#### Adam Topaz (Jul 29 2020 at 18:09):

But in reality, mathlib should have code for:

- two-sided ideals.
- two-sided ideals generated by some set.
- quotients by two-sided iddeals.

#### 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

#### Mario Carneiro (Jul 29 2020 at 18:12):

namely the ideal span of the input set

#### 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 $0$, and ensures compatibility with the algebra operations. Does mathlib already have some code to do this?

#### 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`

#### Eric Wieser (Jul 29 2020 at 18:21):

There's `submodule.quotient`

too

#### 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.

#### Eric Wieser (Jul 29 2020 at 18:26):

Are you looking for submodule.closure or something?

#### Eric Wieser (Jul 29 2020 at 18:27):

Nevermind, missed the mul

#### Adam Topaz (Jul 29 2020 at 18:27):

When you take `quot`

by such a relation, you get the quotient of the ring $A$ by the two-sided ideal generated by $S$.

#### 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 $s \cdot a$ where $s\in S$ and $a\in A$.

#### 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

#### 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

#### Kevin Buzzard (Jul 30 2020 at 11:54):

Does submodule not extend add_subgroup?

#### Kevin Buzzard (Jul 30 2020 at 11:55):

Does submodule not extend add_subgroup?

#### 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)

#### Eric Wieser (Jul 30 2020 at 12:26):

PR so far is at #3635

#### 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`

#### 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)
```

#### 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

#### Kevin Buzzard (Jul 30 2020 at 13:32):

Does submodule not extend add_subgroup?

#### Adam Topaz (Jul 30 2020 at 13:33):

It does I think

#### Adam Topaz (Jul 30 2020 at 13:35):

#### Adam Topaz (Jul 30 2020 at 13:35):

add_submonoid

#### 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.

#### Adam Topaz (Jul 30 2020 at 13:37):

Oh yeah Eric mentioned this above

#### Adam Topaz (Jul 30 2020 at 13:38):

Yes of course.

#### Adam Topaz (Jul 30 2020 at 13:39):

But the same argument works also for right and left modules

#### 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

#### Adam Topaz (Jul 30 2020 at 15:32):

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

#### Adam Topaz (Jul 30 2020 at 15:34):

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

#### Jalex Stark (Jul 30 2020 at 15:40):

the best implementation of the `left_`

and `right_`

approach probably requires metaprogramming (cf. `to_additive`

)

#### Eric Wieser (Jul 30 2020 at 15:40):

Yeah, I was thinking the same

#### Adam Topaz (Jul 30 2020 at 15:41):

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

#### 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

#### 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

#### 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

#### Eric Wieser (Jul 30 2020 at 15:42):

So a proof that is `by simp only [some_lemma]`

still has to be repeated

#### Eric Wieser (Jul 30 2020 at 15:44):

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

#### 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
```

#### Adam Topaz (Jul 30 2020 at 15:53):

Unfortunately

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

#### 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?

#### 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)
```

#### 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_ref`

will contain what's in `rel`

and also some additional equivalencies.

#### 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`

?

#### Eric Wieser (Aug 03 2020 at 07:44):

Q2: `quadratic_form`

is not a class, so will not be inferred

#### Eric Wieser (Aug 03 2020 at 07:45):

I'd make qv an argument of `cliff_rel`

or `pre`

instead

#### 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.

#### 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.

#### Eric Wieser (Aug 03 2020 at 08:17):

Should `pre`

be marked private then?

#### Eric Wieser (Aug 03 2020 at 08:18):

`of`

is exposed as `\iota`

, of_scalar is `algebra_map K T`

I guess

#### 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`

#### 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?

#### Adam Topaz (Aug 03 2020 at 12:26):

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

#### 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

#### 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.

#### 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.

#### Adam Topaz (Aug 03 2020 at 12:45):

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

#### 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.

#### Adam Topaz (Aug 03 2020 at 12:50):

Are you trying to define the Clifford algebra?

#### Utensil Song (Aug 03 2020 at 12:50):

Adam Topaz said:

What's the problem with defining bimodules as modules over $A \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.

#### Utensil Song (Aug 03 2020 at 12:50):

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

#### 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_ref`

will contain what's in`rel`

and also some additional equivalencies.

Any comments on Q1?

#### 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!

#### Adam Topaz (Aug 03 2020 at 12:55):

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

#### 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.

#### 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.

#### Utensil Song (Aug 03 2020 at 13:01):

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

#### 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)
```

#### Utensil Song (Aug 03 2020 at 13:12):

Where're the `*compat*`

coming from?

#### 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?)

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

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

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

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

#### 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?

#### 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...

#### Utensil Song (Aug 03 2020 at 13:27):

What's your plan after working on tensor algebra?

#### 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.

#### 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.

#### Utensil Song (Aug 03 2020 at 13:33):

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

#### 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.

#### 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).

#### 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.

#### 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?

#### Adam Topaz (Aug 03 2020 at 14:05):

No, the scalar action is just multiplication in an algebra

#### 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?

#### Adam Topaz (Aug 03 2020 at 14:07):

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

#### Eric Wieser (Aug 03 2020 at 14:09):

Ah, I was forgetting that a quotient map is implemented

#### 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!

#### Simon Hudon (Aug 03 2020 at 17:56):

Done

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

Thanks! @Simon Hudon

#### 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.

#### 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