Simple algebra / ring

Stream: Is there code for X?

[Eloi Torrents]

Is there the definition of a simple ring?

[Kevin Buzzard]

Is this a concept from non-commutative ring theory? We're not very good at that yet, the algebraic geometers got here first

[Eric Wieser]

Yeah, it looks like it needs two-sided ideals, which we don't have

[Eric Wieser]

At a guess, maybe it's enough to have quotients by two-sided ideals (which we do have), as something awful like ∀ r : R → R → Prop, nonempty (ring_quot r ≃+* R ⊕ ring_quot r ≃+* unit).

[Eric Wieser]

Which at even more of a guess, is the same as ∀ r : R → R → Prop, (=) < r → subsingleton (ring_quot r)

[Adam Topaz]

We do have quotients. A simple ring is a ring whose only quotients are the trivial ring and the ring itself

[Adam Topaz]

:face_palm: just saw Eric's message

[Eric Wieser]

Maybe what I meant by the simplified version is ∀ r : setoid R, ⊥ < r → subsingleton (ring_quot r.rel)

[Adam Topaz]

We can also say that the quotient map associated to r is injective when the quotient is nontrivial

[Adam Topaz]

What sort of things do you want to prove about simple rings @Eloi Torrents ?

[Eloi Torrents]

At the moment I need an instance has_inv R given is_simple_ring R.

[Kevin Buzzard]

Are two by two matrices over the complexes a simple ring? They have no nontrivial two-sided ideals but they don't have inverses either

[Eloi Torrents]

(deleted)

[Eloi Torrents]

I messed this up, I want to prove that the center of a simple algebra is a field.

[Adam Topaz]

Sounds like you should prove that the center of a simple ring is simple

[Adam Topaz]

(I don't actually know if that's the most straightforward way to prove this)

[Johan Commelin]

Having is_simple_ring R would be really nice. It's time that we do some central simple algebras in Lean (-;

[Eloi Torrents]

Is there some way to write lemmas for left and right ideals at once?

[Riccardo Brasca]

I think that at the moment only left ideals are defined in mathlib.

[Eric Wieser]

Right ideals are submodule (opposite R) R, and ideal = submodule R R is a left-ideal

[Eric Wieser]

We only have API for the left ideals, but lots of it is just copied from the submodule API anyway.

[Eric Wieser]

You could declare a two-sided ideal as:

structure sub_bimodule (R S M : Type*) [semiring R] [semiring S] [add_comm_monoid M]
  [module R M] [module Sᵒᵖ M] extends
    submodule R M, submodule Sᵒᵖ M renaming smul_mem' → op_smul_mem'

def two_sided_ideal := sub_bimodule R R R

[Matthew Ballard]

Do you want commutation of the two actions (as the name bimodule evokes) or would it be better to put that elsewhere?

[Adam Topaz]

Something like the following should work:

import linear_algebra

set_option old_structure_cmd true

structure sub_bimodule (R S M : Type*) [semiring R] [semiring S] [add_comm_monoid M]
  [module R M] [module Sᵒᵖ M] extends
    submodule R M, submodule Sᵒᵖ M renaming smul_mem' → op_smul_mem' :=
(smul_comm' (r : R) (s : S) (m : M) : r • ((opposite.op s) • m) = (opposite.op s) • (r • m))

def two_sided_ideal (R : Type*) [semiring R] := sub_bimodule R R R

[Matthew Ballard]

Having two actions and being closed under both certainly seems like a useful notion in and of itself. Commutation just is a very common use case. Another one: ideals in additive categories

[Adam Topaz]

We should really just define bimodules already...

[Matthew Ballard]

Is $R\otimes_{\mathbb Z} S$-modules a bad idea?

[Adam Topaz]

We played with that idea a little while ago. I don't remember what the conclusion was.

[Matthew Ballard]

I remember seeing it

[Adam Topaz]

I like this renaming trick:

import linear_algebra

set_option old_structure_cmd true

class bimodule (R S M : Type*) [semiring R] [semiring S] [add_comm_monoid M]
  extends module R M, module Sᵒᵖ M renaming
    _to_distrib_mul_action → _to_op_distrib_mul_action
    add_smul → add_op_smul
    zero_smul → zero_op_smul :=
(smul_comm (r : R) (s : S) (m : M) : r • (opposite.op s • m) = (opposite.op s) • (r • m))

[Matthew Ballard]

That seems like the least complex definition. One can then relate it to modules over the tensor product

[Eric Wieser]

Matthew Ballard said:

Do you want commutation of the two actions (as the name bimodule evokes) or would it be better to put that elsewhere?

That's already covered by smul_comm_class R Sᵒᵖ M, so we probably don't want to add a smul_comm' field like @Adam Topaz's message below yours does.

[Eric Wieser]

I didn't include that as a typeclass in my subbimodule definition because it's not needed for the definition

[Eric Wieser]

The question is whether it's actually useful to have [bimodule R S M] vs [module R M] [module Sᵒᵖ M] [smul_comm_class R Sᵒᵖ M]

[Matthew Ballard]

I think bimodule is a common enough thing that mathematicians would prefer the former over always invoking the latter. But I don't think there is anything beyond the existence of the notation

[Eric Wieser]

The downside is that any lemmas you write about [bimodule R S M] won't apply if you only have [module R M] [module Sᵒᵖ M] [smul_comm_class R Sᵒᵖ M] available

[Eric Wieser]

Whereas the reverse is not true. So having bimodule is a fine idea, but actually using it in lemmas makes them much harder to use

[Eric Wieser]

In particular, we would likely need to add an instance : bimodule in every place we currently have instance : smul_comm_class

[Eric Wieser]

And then the question becomes; do we also want bi_distrib_mul_action, bi_mul_action, etc...

[Johan Commelin]

I think before an biactions, we need to settle on a notation class for actions on the right. Eric had some suggestions in his "actions in mathlib" paper. I think •> and <•, right?

[Eric Wieser]

Yes, probably hidden behind a locale so that people who only care about left-actions can continue using and seeing • in the infoview

[Eric Wieser]

We could also replace the <> with some kind of arrow symbol, since less-than/greater-than are not really semantically relevant.

[Eric Wieser]

m ⮈ s and r ⮊ mcould also work

[Eric Wieser]

Or maybe m •⃔ s and r •⃕ m, but those don't render on zulip (or vscode), even as plaintext: m •⃔ s and r •⃕ m

[Eric Wieser]

image.png

[Yaël Dillies]

I feel watched.