Ideals over algebras

Stream: Is there code for X?

[Eric Wieser]

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}

[Eric Wieser]

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

[Johan Commelin]

Hmm? Why are you using setoid?

[Johan Commelin]

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

[Reid Barton]

I think probably just the quotient R-module

[Reid Barton]

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

[Eric Wieser]

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

[Reid Barton]

You need an ideal for that

[Eric Wieser]

My ideal is the sorry in the above snippet

[Eric Wieser]

I think

[Eric Wieser]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Reid Barton]

That's a quotient by an ideal, right?

[Eric Wieser]

Yes, I think so

[Reid Barton]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Reid Barton]

Ah I see

[Eric Wieser]

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]

you need it for multiplication

[Reid Barton]

I don't think we have two-sided ideals

[Reid Barton]

In general, noncommutative algebra is underdeveloped.

[Mario Carneiro]

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

[Adam Topaz]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Adam Topaz]

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

[Eric Wieser]

The cdot 1 there is just a coe, right?

[Johan Commelin]

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]

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]

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]

where pre Q is tensor_algebra R M

[Eric Wieser]

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

[Adam Topaz]

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]

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

[Adam Topaz]

Are you sure you want to adjoin things?

[Adam Topaz]

This is an over-ring of the tensor algebra.

[Reid Barton]

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

[Eric Wieser]

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

Yeah, I couldn't find these

[Adam Topaz]

Well, that's a problem...

[Eric Wieser]

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]

When in fact I should not have been

[Adam Topaz]

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]

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]

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]

namely the ideal span of the input set

[Adam Topaz]

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]

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

[Eric Wieser]

There's submodule.quotient too

[Adam Topaz]

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]

Are you looking for submodule.closure or something?

[Eric Wieser]

Nevermind, missed the mul

[Adam Topaz]

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]

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]

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]

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

[Kevin Buzzard]

Does submodule not extend add_subgroup?

[Kevin Buzzard]

Does submodule not extend add_subgroup?

[Eric Wieser]

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

[Eric Wieser]

PR so far is at #3635

[Eric Wieser]

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]

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

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]

Does submodule not extend add_subgroup?

[Adam Topaz]

It does I think

[Adam Topaz]

src#submodule

[Adam Topaz]

add_submonoid

[Kevin Buzzard]

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]

Oh yeah Eric mentioned this above

[Adam Topaz]

Yes of course.

[Adam Topaz]

But the same argument works also for right and left modules

[Eric Wieser]

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]

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

[Adam Topaz]

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]

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

[Eric Wieser]

Yeah, I was thinking the same

[Adam Topaz]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Adam Topaz]

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]

Unfortunately

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

[Utensil Song]

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

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]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Utensil Song]

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

[Scott Morrison]

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]

Should pre be marked private then?

[Eric Wieser]

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

[Kenny Lau]

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]

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]

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

[Adam Topaz]

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]

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]

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]

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

[Utensil Song]

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]

Are you trying to define the Clifford algebra?

[Utensil Song]

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]

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

[Utensil Song]

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?

[Adam Topaz]

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

[Adam Topaz]

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

[Utensil Song]

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]

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]

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

[Adam Topaz]

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]

Where're the *compat* coming from?

[Utensil Song]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Utensil Song]

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

[Adam Topaz]

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]

What's your plan after working on tensor algebra?

[Adam Topaz]

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]

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]

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

[Patrick Massot]

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

[Adam Topaz]

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]

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]

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

[Adam Topaz]

No, the scalar action is just multiplication in an algebra

[Eric Wieser]

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

[Adam Topaz]

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

[Eric Wieser]

Ah, I was forgetting that a quotient map is implemented

[Utensil Song]

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

Done

[Utensil Song]

Thanks! @Simon Hudon

[Scott Morrison]

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]

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.