Stream: Is there code for X?

Topic: Ideals over algebras

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

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?

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

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!

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:

1. two-sided ideals.
2. two-sided ideals generated by some set.
3. 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 quotby 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

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

It does I think

src#submodule

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

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

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

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_3 : module 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_refwill 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):

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_refwill contain what's in rel and also some additional equivalencies.

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

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!

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