ideals in non-comm rings

Stream: maths

[Winston Yin]

I'm thinking about how to extend ring_theory.ideal.basic to cover two-sided ideals for non-commutative rings. Until recently, ideal was only defined for comm_semirings, and now it is defined as left-ideals of (non-commutative) semirings as submodule R R. What would be a good way to define two-sided ideals for semirings? I can think of two options:

• Define a new structure lrideal, so that lots of lemmas for submodule would have to be copied over.
• Treat two-sided ideals as left-ideals (ideal) with an additional hypothesis that it's closed under right multiplication by ring elements.
  Are there more approaches? I'm not experienced enough to tell which is a better approach.

[Scott Morrison]

To make matters worse, there is the third option of defining two sided ideals to be left ideals under the R (x) R^op action.

[Winston Yin]

Do you mean forall (x in I) (r in R), r * x * r in I? Isn't that a bit weaker than a two-sided ideal?

[Winston Yin]

I might go with defining a new structure and show equivalence for other approaches

[Johan Commelin]

Scott means $\forall (r,s) \in R \times R^{\text{op}}, \forall x \in I, (r,s) \bullet x \in I$, which unfolds to $r * x * s \in I$.

[Winston Yin]

Actually I'll try using this for the moment to avoid defining new things, and see how annoying it gets down the road

[Julian Külshammer]

I think the agreement before was that (two-sided) ideals should be defined as a special case of bimodules (like left ideals are defined as a special class of modules). Let me paste some private communication with Aaron here: "Bimodules could be easy (smul_comm_class is already there) but subbimodules are confusing. Basically, I think we might have to go down to the bottom of that hierarchy, going through bi_mul_action etc. Here's the discussion from last December: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Bimodules "

[Johan Commelin]

Hmm, that's an interesting idea, to start all the way down at bi_mul_action.

[Winston Yin]

Just looked through the thread you linked. Very interesting! So the idea is to implement bi_mul_action, etc, bi_module, as well as their corresponding sub-objects? Then, two-sided ideal would just be sub_bi_module R R^op R?

[Johan Commelin]

bi_submodule R R^op R, I guess.

[Winston Yin]

Yes, of course

[Winston Yin]

Sounds like a lot of work but I'm happy to look into this a bit

[Winston Yin]

And at every stage, we define type class instances for the corresponding "non-bi" objects for the left multiplication and right multiplication

[Scott Morrison]

I would be very happy to have a proper theory of bimodules. They are, of course, the fundamental objects. (The R (x) R^op trick I mentioned of course only works in a braided category. :-)

[Eric Wieser]

https://m.youtube.com/watch?v=GsDGvwhxq5U has a discussion of right actions and bimodules in the future work section

[Scott Morrison]

I like your proposed notation <• for the right scalar action. Maybe we should even introduce •> as an alias for •.

[Winston Yin]

Mirroring module and submodule, this would be the overall structure of bimodule and sub_bimodule:

import group_theory.group_action.defs
import group_theory.submonoid.basic
import algebra.opposites
import algebra.module.basic

notation m ` •ᵣ `:72 a:72 := (opposite.op a) • m

class bi_mul_action (α : Type*) (β : Type*) (γ : Type*) [monoid α] [monoid β] [has_scalar α γ] [has_scalar βᵒᵖ γ]
  extends smul_comm_class α βᵒᵖ γ :=
(one_smul_l : ∀ c : γ, (1 : α) • c = c)
(one_smul_r : ∀ c : γ, c •ᵣ (1 : β) = c)
(mul_smul_l : ∀ (x y : α) (c : γ), (x * y) • c = x • y • c)
(mul_smul_r : ∀ (x y : β) (c : γ), c •ᵣ (x * y) = c •ᵣ y •ᵣ x)

class bi_distrib_mul_action (M : Type*) (N : Type*) (A : Type*) [monoid M] [monoid N] [add_monoid A] [has_scalar M A] [has_scalar Nᵒᵖ A]
  extends bi_mul_action M N A :=
(smul_add_l : ∀ (r : M) (x y : A), r • (x + y) = r • x + r • y)
(smul_zero_l : ∀ (r : M), r • (0 : A) = 0)
(smul_add_r : ∀ (r : N) (x y : A), (x + y) •ᵣ r = x •ᵣ r + y •ᵣ r)
(smul_zero_r : ∀ (r : N), (0 : A) •ᵣ r = 0)

class bimodule (R : Type*) (S : Type*) (M : Type*) [semiring R] [semiring S] [add_comm_monoid M] [has_scalar R M] [has_scalar Sᵒᵖ M] extends bi_distrib_mul_action R S M :=
(add_smul_l : ∀ (r s : R) (x : M), (r + s) • x = r • x + s • x)
(zero_smul_l : ∀ (x : M), (0 : R) • x = 0)
(add_smul_r : ∀ (r s : S) (x : M), x •ᵣ (r + s) = x •ᵣ r + x •ᵣ s)
(zero_smul_r : ∀ (x : M), x •ᵣ (0 : S) = 0)

section
set_option old_structure_cmd true

structure sub_bi_mul_action (R : Type*) (S : Type*) (M : Type*) [has_scalar R M] [has_scalar Sᵒᵖ M] :=
(carrier : set M)
(smul_mem_l' : ∀ (c : R) {x : M}, x ∈ carrier → c • x ∈ carrier)
(smul_mem_r' : ∀ (c : S) {x : M}, x ∈ carrier → x •ᵣ c ∈ carrier)

structure sub_bimodule (R : Type*) (S : Type*) (M : Type*) [semiring R] [semiring S] [add_comm_monoid M] [module R M] [module Sᵒᵖ M] extends add_submonoid M, sub_bi_mul_action R S M

end

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

How does this look? Btw, the <• suggestion is great!

[Scott Morrison]

Hopefully Eric will give an opinion: I suspect he's thought about this the most so far.

A minor request: could we write bimodule R M S instead (i.e. the rings on either side of the bimodule), just like in the mathematical notation ${}_R M_S$?

[Eric Wieser]

https://m.youtube.com/watch?v=GsDGvwhxq5U has a discussion of right actions and bimodules in the future work section

[Yakov Pechersky]

The classes should probably extend has_scalar, similar to how mul_action does.

[Yakov Pechersky]

And should be generalized to "mul_one_class" etc

[Eric Wieser]

(apologies, I have no idea why zulip sent that twice hours apart)

[Eric Wieser]

I think having a separate bimodule R S M typeclass is probably as reasonable as having integral_domain in that it is just a shorthand for a collection of typeclasses. But most lemmas would probably end up stated about the three separate typeclasses, since then you can relax them individually. If we have it, it should provide a bimodule.to_module : module R M and bimodule.to_right_module : module Sᵒᵖ M

[Eric Wieser]

So not as you have it written above

[Eric Wieser]

Can we make open_locale bimodule change the pretty printer to use •> for • and add the other notation?

[Johan Commelin]

Ooh, that would be sweet!

[Eric Wieser]

(for the record, I think that having docs#integral_domain is annoying because if you have only comm_ring, no_zero_divisors and nontrivial you have to insert an awkward letI because typeclass search can't deal with the loops formed by two different ways to express the same thing; but there's clear pedagogical value to integral_domain as a spelling - the same view applies to bimodule)

[Eric Wieser]

My above comment about bimodule.to_module is wrong; it produces a dangerous instance. I think the best approach would be

abbreviation right_module (R M) := module Rᵒᵖ M

abbreviation bimodule (R S M) := smul_comm_class R Sᵒᵖ M

[Winston Yin]

What I've tried so far is to define bimodule as

class bimodule (R : Type*) (M : Type*) (S : Type*)
[semiring R] [semiring S] [add_comm_monoid M]
[module R M] [module Sᵒᵖ M]
extends smul_comm_class R Sᵒᵖ M

[Winston Yin]

This way, writing bimodule R M S would require first module R M and module Sᵒᵖ M

[Winston Yin]

I then defined

variables
... [module_RM : module R M] [module_SM : module Sᵒᵖ M] [bimodule R M S]

def to_left_module : module R M := module_RM
def to_right_module : module Sᵒᵖ M := module_SM

[Winston Yin]

Avoiding dangerous type class instances

[Winston Yin]

sub_bimodule is defined as

structure sub_bimodule (R : Type*) (M : Type*) (S : Type*)
[semiring R] [semiring S] [add_comm_monoid M]
[module R M] [module Sᵒᵖ M] [bimodule R M S]
extends add_submonoid M :=
(smul_mem_l' : ∀ (c : R) {x : M}, x ∈ carrier → c • x ∈ carrier)
(smul_mem_r' : ∀ (c : S) {x : M}, x ∈ carrier → x <• c ∈ carrier)

Then some lemmas for submodule just have to be duplicated with _l and _r versions

[Johan Commelin]

Winston Yin said:

I then defined

variables
... [module_RM : module R M] [module_SM : module Sᵒᵖ M] [bimodule R M S]

def to_left_module : module R M := module_RM
def to_right_module : module Sᵒᵖ M := module_SM

What is the benefit of this? After all the instance was already there as assumption.
This would make sense if you extends module R M, module Sᵒᵖ M, smul_comm_class R Sᵒᵖ M

[Winston Yin]

You're right...

[Eric Wieser]

I would mildly caution against having bimodule actually take [module R M] assumptions; I think there's a lower risk of pain down the road (like we experienced with the old module/semimodule split) if you simply assume [has_scalar R M] instead, even though that's somewhat misleading

[Jakob von Raumer]

@Winston Yin Has this made it into a PR yet?

[Jakob von Raumer]

Any opinions on changing compatible_smul to

class compatible_smul [distrib_mul_action R'ᵒᵖ N] :=
(op_smul_tmul : ∀ (r : R') (m : M) (n : N), (r • m) ⊗ₜ n = m ⊗ₜ[R] (op r • n))

in the long run, given we make sure that op r properly simplifies to r in the case of commutative rings?

[Eric Wieser]

docs#tensor_product.compatible_smul for reference

[Eric Wieser]

Presumably once we start thinking about tensor products of bimodules, we first need to change docs#tensor_product.eqv.of_smul to

| of_smul : ∀ (r : R) (m : M) (n : N), eqv
    (free_add_monoid.of (op r • m, n)) (free_add_monoid.of (m, r • n))

and have tensor products require [module Rᵒᵖ M] [module R N]

[Eric Wieser]

Or do I have the convention backwards? It seems natural to me to put the scalar in the middle so that (m <• r) ⊗ₜ n = m ⊗ₜ[R] (r •> n) where r : R, but convention wins over my personal opinion of what is natural

[Eric Wieser]

Hmm, I think we have a problem here. In the bimodule world where M is an S-R bimodule and N is an R-T bimodule, we presumably want

   s • (m ⊗ₜ[R] n) = (s • m) ⊗ₜ[R] n
op t • (m ⊗ₜ[R] n) =       m ⊗ₜ[R] (op t • n)

However, the latter case matches the former case with s = op t, and while probably gives a propositionally equal action in the cases where typeclasses match, certainly does not give a definitionally equal one.

[Jakob von Raumer]

I don't necessaily need bimodules, just the tensor product for modules on non-commutative rings, even if it doesn't bear an R-action itself

[Jakob von Raumer]

Eric Wieser said:

Presumably once we start thinking about tensor products of bimodules, we first need to change docs#tensor_product.eqv.of_smul to

| of_smul : ∀ (r : R) (m : M) (n : N), eqv
    (free_add_monoid.of (op r • m, n)) (free_add_monoid.of (m, r • n))

and have tensor products require [module Rᵒᵖ M] [module R N]

Yes, that's a change I also did locally

[Jakob von Raumer]

The issue is that in the commutative case we have everything cluttered with op and ᵒᵖ then :pensive:

[Jakob von Raumer]

Maybe changing the definition of tensor_product but creating an instance of compatible_smul R R M N for the commutative case could be an option. (The instance requires transfering all sorts of classes, like module R M to module Rᵒᵖ M)

[Jakob von Raumer]

I think this issue is part of a bigger one: How do we reconcile commutative algebraic structures with their ops? Since opposite is irreducible we can't state r = opposite.op r without a cast...

[Jakob von Raumer]

section comm_op

local attribute [reducible] opposite

@[simp] def comm_op {R : Type*} [comm_semiring R] (r : R) : opposite.op r = r := rfl

end comm_op

This seems to be a way?

[Eric Wieser]

That's solving the wrong problem

[Eric Wieser]

You want lean to know that op r • m = r • m

[Eric Wieser]

Rewriting op r to r just makes things worse, because your statement was originally

@has_scalar (opposite R) M opposite.has_scalar (op r) m = @has_scalar R M _ r m

but your lemma turns it into the very wrong

@has_scalar (opposite R) M opposite.has_scalar r m = @has_scalar R M _ r m

which is using R, but the action from opposite R

[Eric Wieser]

We need a typeclass that says the left and right actions are the same

[Eric Wieser]

class is_symmetric_smul (R M) [has_scalar R M] [has_scalar (opposite R) M] :=
(op_smul_eq_smul : forall r m, op r • m = r • m)

You'll then want to add instances for:

• is_symmetric_smul R R when comm_semigroup R
• is_symmetric_smul R (prod A B) when is_symmetric_smul R A and is_symmetric_smul R B
• pi
• ulift
• ...
• probably most of the things we currently have has_scalar instances for.

[Jakob von Raumer]

Do you think it's still reasonable to have both

class compatible_smul_op [distrib_mul_action R'ᵒᵖ N] :=
(smul_tmul_op : ∀ (r : R') (m : M) (n : N), (r • m) ⊗ₜ n = m ⊗ₜ[R] (op r • n))

and

class compatible_smul [distrib_mul_action R' N] :=
(smul_tmul : ∀ (r : R') (m : M) (n : N), (r • m) ⊗ₜ n = m ⊗ₜ[R] (r • n))

with is_symmetric_smul present?

[Jakob von Raumer]

Eric Wieser said:

class is_symmetric_smul (R M) [has_scalar R M] [has_scalar (opposite R) M] :=
(op_smul_eq_smul : forall r m, op r • m = r • m)

You'll then want to add instances for:

• is_symmetric_smul R R when comm_semigroup R

You mean what we need is the following?

instance {R α : Type*} [comm_semigroup R] [has_scalar R α] : is_symmetric_smul R α := _

But then at this point we do need a (low priority? local?) instance forhas_scalar (opposite R) α

[Jakob von Raumer]

Eric Wieser said:

class is_symmetric_smul (R M) [has_scalar R M] [has_scalar (opposite R) M] :=
(op_smul_eq_smul : forall r m, op r • m = r • m)

You'll then want to add instances for:

• is_symmetric_smul R R when comm_semigroup R

You mean what we need is the following?

instance {R α : Type*} [comm_semigroup R] [has_scalar R α] : is_symmetric_smul R α := _

But then at this point we do need a (low priority? local? we want to keep the option of having a right action that's different from the left action, even if R is commutative, right?) instance forhas_scalar (opposite R) α

[Eric Wieser]

I'm not sure we need both, I'd focus on adding the first one and then reassess

[Eric Wieser]

The is_symmetric_smul R α instance you suggest doesn't type check, there's no has_scalar Rᵒᵖ α for it to be about

[Eric Wieser]

Which is why I said you only want the R R instance

[Jakob von Raumer]

Eric Wieser said:

The is_symmetric_smul R α instance you suggest doesn't type check, there's no has_scalar Rᵒᵖ α for it to be about

Yes, an instance for has_scalar Rᵒᵖ α given has_scalar R α what I suggested adding...

[Eric Wieser]

Oh, we do not need that instance

[Eric Wieser]

has_scalar Rᵒᵖ R is enough, and we already have that

[Eric Wieser]

For instance, has_scalar Rᵒᵖ (fin 3 → R) can be found today via docs#pi.has_scalar

[Oliver Nash]

Jakob von Raumer said:

I don't necessaily need bimodules, just the tensor product for modules on non-commutative rings, even if it doesn't bear an R-action itself

Right, just like for linear maps. Even when the scalars are non-commuative we have docs#linear_map.add_comm_monoid but we need some form of commutativity for docs#linear_map.module

[Oliver Nash]

I haven't studied this thread carefully enough to understand your objectives beyond noting you want tensor product with non-commutative scalars (which I too would love to have) but this old thread of mine might also be food for thought:
https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.234773.20base.20change/near/240929318

[Jakob von Raumer]

Eric Wieser said:

has_scalar Rᵒᵖ R is enough, and we already have that

I think I don't quite get the connection yet. Does this involve defining op r • m by (op r • (1 : R)) • m?

[Eric Wieser]

No, what I said above doesn't; but we can use that to almost get away without is_symmetric_smul:

import group_theory.group_action.basic
import algebra.module.opposites
import algebra.module.prod

open opposite

instance comm_semigroup.op_is_scalar_tower {R} [comm_semigroup R] : is_scalar_tower Rᵒᵖ R R :=
⟨λ a b c, opposite.rec (by exact λ a', mul_right_comm b a' c) a⟩

-- this works around a typeclass bug in pi types
instance comm_monoid.op_is_scalar_tower {R} [comm_monoid R] : is_scalar_tower Rᵒᵖ R R :=
comm_semigroup.op_is_scalar_tower

-- we were able to prove this without `is_symmetric_smul`
lemma op_smul_eq_smul {R M} [monoid R] [mul_action R M] [mul_action Rᵒᵖ M]
  [is_scalar_tower Rᵒᵖ R M] (r : R) (m : M) :
  op r • m = r • m :=
by rw [←one_smul R m, ←smul_assoc (op r) (1 : R) m, op_smul_eq_mul, smul_smul, one_mul, mul_one]

variables {R : Type*} [comm_monoid R] (r : R)

example (m : R) : op r • m = r • m := op_smul_eq_smul _ _
example (m : R × R) : op r • m = r • m := op_smul_eq_smul _ _
example (m : fin 3 → R) : op r • m = r • m := op_smul_eq_smul _ _  -- needs the workaround above

we still need it if we want to talk about actions by non-monoids

[Eric Wieser]

I think I don't quite get the connection yet

Can you give me an example of something that doesn't have a right action today, but should?

[Eric Wieser]

My claim is that the instance you suggest would just conflict with ones we already have, and there's no situation that you need it anyway

[Jakob von Raumer]

Eric Wieser said:

I think I don't quite get the connection yet

Can you give me an example of something that doesn't have a right action today, but should?

No I was just saying that I don't quite understand yet how the has_scalar Rᵒᵖ R instance actually helps making sense of op r • m

[Eric Wieser]

Because for almost every choice of m you make, there's already an actionhas_scalar Rᵒᵖ M defined in terms of has_scalar Rᵒᵖ R

[Jakob von Raumer]

Where is it defined?

[Eric Wieser]

In the same place as has_scalar R M

[Eric Wieser]

The location of which depends on your choice of M. See for instance docs#prod.has_scalar, docs#pi.has_scalar

[Jakob von Raumer]

I'm completely lost.

[Eric Wieser]

Pick a concrete example of R and M and I can show you

[Jakob von Raumer]

What do you mean by concrete? I want to M to be an arbitrary R-module

[Jakob von Raumer]

I just don't get what has_scalar Rᵒᵖ R has to do with this if we don't have a full scalar_tower Rᵒᵖ R M

[Eric Wieser]

By concrete I mean M = R × R, M = polynomial R etc. I don't understand the question you're asking

[Eric Wieser]

Under the original proposal:

class is_symmetric_smul (R M : Type*) [has_scalar R M] [has_scalar (opposite R) M] :=
(op_smul_eq_smul : ∀ (r : R) (m : M), op r • m = r • m)

open is_symmetric_smul (op_smul_eq_smul)

instance comm_semigroup.is_symmetric_smul {R} [comm_semigroup R] : is_symmetric_smul R R :=
⟨λ r m, mul_comm _ _⟩

instance prod.is_symmetric_smul {R α β}
  [has_scalar R α] [has_scalar R β] [has_scalar Rᵒᵖ α] [has_scalar Rᵒᵖ β]
  [is_symmetric_smul R α] [is_symmetric_smul R β] : is_symmetric_smul R (α × β) :=
⟨λ r m, prod.ext (op_smul_eq_smul _ _) (op_smul_eq_smul _ _)⟩

instance pi.is_symmetric_smul {R} {ι : Type*} {α : ι → Type*}
  [Π i, has_scalar R (α i)] [Π i, has_scalar Rᵒᵖ (α i)] [Π i, is_symmetric_smul R (α i)] :
  is_symmetric_smul R (Π i, α i) :=
⟨λ r m, funext $ λ i, op_smul_eq_smul _ _⟩

-- hack that hopefully lean4 doesn't need
instance function.is_symmetric_smul {R} {ι : Type*} {α : Type*}
  [has_scalar R α] [has_scalar Rᵒᵖ α] [is_symmetric_smul R (α)] :
  is_symmetric_smul R (ι → α) :=
pi.is_symmetric_smul

Any lemma about a symmetric bimodule would be stated as:

lemma some_lemma [module R M] [module Rᵒᵖ M] [is_symmetric_smul R M] : sorry

[Eric Wieser]

You don't need to worry about where module Rᵒᵖ M comes from, that's the caller's problem

[Eric Wieser]

And the caller either:

1. Is working with a concrete type, and so has the instance available
2. Is working on a variable type, so passes the obligation on to their caller

[Jakob von Raumer]

(deleted)

[Jakob von Raumer]

I thought you meant that in order to have

instance {R α : Type*} [comm_semigroup R] [has_scalar R α] : is_symmetric_smul R α := _

instead of adding an argument has_scalar Rᵒᵖ α, an argument has_scalar Rᵒᵖ R would be enough.

[Jakob von Raumer]

But I guess you said we shouldn't have that instance at all? So everyone using tensor products as before would have to supply the is_symmetric_smul?

[Eric Wieser]

You don't need is_symmetric_smul to use tensor_product; only the lemmas that require it

[Jakob von Raumer]

Okay, I guess now I get it. I'll see how much need for refactoring this causes outside of linear_algebra.tensor_product...

[Eric Wieser]

Unfortunately there's a nasty typeclass issue that looks like it makes both is_symmetric_smul and [is_scalar_tower Rᵒᵖ R M] non-viable quite annoying (until lean4)

[Eric Wieser]

I edited the message above with some is_symmetric_smul instances to get you started

[Jakob von Raumer]

Thanks for all the help!

[Jakob von Raumer]

One thing that's not obvious to me is how to fix the following: The current construction of compatible_smul.is_scalar_tower now needs the following instance to go through:

instance has_scalar_op_op {R R' : Type*} [has_scalar R' R] : has_scalar R'ᵒᵖ Rᵒᵖ :=
⟨λ r' r, opposite.op (opposite.unop r' • opposite.unop r)⟩

It fails if the instance of has_scalar R'ᵒᵖ Rᵒᵖ is anything other than this, because we need op (r • b) = op r • op b. But then, compatible_smul.is_scalar_tower doesn't generalise to compatible_smul R R M N anymore because mul_action.is_scalar_tower.left uses an instance of has_scalar Rᵒᵖ Rᵒᵖ which is not defeq to has_scalar_op_op. I solved this by just adding a manual compatible_smul.self : compatible_smul R R M N, but the previous construction was obviously a bit nicer...

[Eric Wieser]

Your has_scalar_op_op instance looks dangerous to me

[Jakob von Raumer]

Well it's needed to make sense of is_scalar_tower R'ᵒᵖ Rᵒᵖ N in this context. But maybe we should keep it local?

[Eric Wieser]

My hunch is that you probably should take [has_scalar R'ᵒᵖ R ] as an argument there too; and if you need it to satisfy op (r • b) = op r • op b, then work out a way to express that with typeclasses

[Eric Wieser]

Adding compatible_smul.self seems like a much more conservative bet than adding your instance

[Eric Wieser]

then work out a way to express that with typeclasses

Here's that way:

-- you need this instance
instance (R M) [has_scalar R M] [has_scalar Rᵒᵖ M] [is_symmetric_smul R M] :
  is_symmetric_smul R Mᵒᵖ := ⟨λ r m, unop_injective (op_smul_eq_smul r m.unop : _)⟩

example (R M) [has_scalar R M] [has_scalar Rᵒᵖ M] [is_symmetric_smul R M] (r : R) (m : M) :
  op (r • m) = op r • op m :=
(op_smul_eq_smul r (op m)).symm

[Eric Wieser]

Perhaps it's worth pointing out the difference between your "add an instance" and my "add an instance"; you're adding data instances which can introduce diamonds and incompatible actions, my instances are only proofs, so can't introduce these things.

[Jakob von Raumer]

That's a neat idea.

[Jakob von Raumer]

It does away with the need for the double-op instance. I doesn't solve the issue of needing a separate compatible_smul.self : compatible_smul R R M N, though since that would require is_symmetric_smul R R which sounds like a bad idea for non-commutative rings

[Eric Wieser]

is_symmetric_smul R R isn't true on non-commutative rings

[Eric Wieser]

And I don't think compatible_smul R R M N is either, although I don't know what your new definition of compatible_smul is

[Eric Wieser]

Do you have a branch you're working on this in?

[Jakob von Raumer]

Not yet, I'll push it later on

[Jakob von Raumer]

I pushed my state of things here, but there's so much left do be done, and I haven't even started to check where things break in other files

[Jakob von Raumer]

Ah, I just noticed it's more canonical to assume that R operates on the right on M and not on N, so I made some bad choices here...

[Eric Wieser]

I thought that was what you had?

[Eric Wieser]

Ah nevermind, you fixed it in https://github.com/javra/mathlib/commit/efea1e30f00a9237590e134bb029ee2d67a5d75b

[Jakob von Raumer]

Now for add_comm_monoid we'd need a right action of ℕ on M, that doesen't seems unnatural either :unamused:

[Yury G. Kudryashov]

Will this create yet another diamond in case M = nat?

[Yury G. Kudryashov]

Because we already have an action of opposite nat on nat.

[Yury G. Kudryashov]

I wonder if there is a way to deal with these diamonds without adding lots of fields to monoid.

[Jakob von Raumer]

Yury G. Kudryashov said:

Will this create yet another diamond in case M = nat?

I think they both reduce to the inverted multiplication, so should be definitionally equal

[Yury G. Kudryashov]

How do you define the new action?

[Yury G. Kudryashov]

Isn't it just nsmul?

[Jakob von Raumer]

Good question. That _does_ yield the wrong operation on M = nat...

[Eric Wieser]

Eric Wieser said:

Hmm, I think we have a problem here. In the bimodule world where M is an S-R bimodule and N is an R-T bimodule, we presumably want

   s • (m ⊗ₜ[R] n) = (s • m) ⊗ₜ[R] n
op t • (m ⊗ₜ[R] n) =       m ⊗ₜ[R] (op t • n)

However, the latter case matches the former case with s = op t, and while probably gives a propositionally equal action in the cases where typeclasses match, certainly does not give a definitionally equal one.

I think my message above was describing a more general case of this diamond?

Edit: nevermind, but this is another diamond to worry about.

[Notification Bot]

This topic was moved by Eric Wieser to #general > right actions by nat

[Eric Wieser]

(to clarify, just the nat diamond bit was)

[Jakob von Raumer]

(deleted)

[Jakob von Raumer]

It's still super hard to adapt that file. The annoying thing is that the most general conditions for the tensor product having a left action and having a right action are so asymmetric. There's one of the actions on M and N thats requirted to be a distrib_mul_action while the other one can be an arbitrary has_scalar, depending on whether it comes from tensor_product.left_has_scalar or from tensor_product.right_has_scalar, and these are of course not separated well in the current state of the file :tired:

[Jakob von Raumer]

Currently thinking of just splitting the files. I had to separate linear_algebra.tensor_product and linear_algebra.tensor_product_basis a while ago anyway due to cyclic dependencies, might as well make a folder with a file for the defn, the left module structure coming from the left module N, the right module structure coming from the right module M

[Jakob von Raumer]

Jakob von Raumer said:

It's still super hard to adapt that file. The annoying thing is that the most general conditions for the tensor product having a left action and having a right action are so asymmetric. There's one of the actions on M and N thats requirted to be a distrib_mul_action while the other one can be an arbitrary has_scalar, depending on whether it comes from tensor_product.left_has_scalar or from tensor_product.right_has_scalar, and these are of course not separated well in the current state of the file :tired:

Oh right, that's exactly the diamond you were talking about, @Eric Wieser

[Jakob von Raumer]

The overlap could be solved in the manner we solved additive vs multiplicative operations. Stating lemmas for smul explicitely and transfer them automatically to lemmas about rsmul...

[Jakob von Raumer]

Eric Wieser said:

Oh, we do not need that instance

Are you sure about that? I still think in the commutative algebra world such an instance should be at least inferrable since user will not want to worry about which side of a module a commutative ring acts on?

[Eric Wieser]

Yes, I'm pretty sure, because having that instance would create diamonds. Can you give an example of a case you're thinking of?

[Jakob von Raumer]

I meant from a user point of view where the current approach would be to require [has_scalar R M] [has_scalar (opposite R) M] [is_symmetric_smul R M] every time, which does seem unwieldy. This would e.g. pop up every time one wants (r • m) ⊗ₜ n = m ⊗ₜ (r • m) instead of (m <• r) ⊗ₜ n = m ⊗ₜ (r • m). I'm not depp into commutative algebra, but I think that's what they want?

[Eric Wieser]

Yes, they would indeed need to do that when working over an arbitrary R and M

[Jakob von Raumer]

Maybe collecting the three instances into has_symmetric_scalar R M could be an option. It's just a use case that pops up a lot in mathlib

[Eric Wieser]

That would be super annoying, because you'd then need has_symmetric_mul_action, has_symmetric_distrib_mul_action, has_symmetric_module, ...

[Jakob von Raumer]

Hm, you're right

[Eric Wieser]

Maybe all that users really care about is has_symmetric_module, but if we had that we'd still end up stating the lemmas in mathlib about is_symmetric_smul to be maximally general

[Jakob von Raumer]

This is probably quite a useful instance, right?

instance is_scalar_tower.is_symmetric_smul {R α} [monoid R] [mul_action R α] [has_scalar Rᵒᵖ α]
  [is_scalar_tower Rᵒᵖ R α] : is_symmetric_smul R α :=
⟨λ r a, by rw [←one_smul R a, ←smul_assoc, one_smul, op_smul_eq_mul, one_mul]⟩

[Jakob von Raumer]

Do you think it's okay for users who use right scalars to be confronted with the fact that if they want to prove something about all r : Rᵒᵖ, they'll be confronted with left scalars instead until they rewrite along ←op_unop?

[Eric Wieser]

I'm not sure; is it also true in the other direction?

[Jakob von Raumer]

Only in the commutative case

[Eric Wieser]

Are all the other assumptions equally strong, or can some be weakened?

[Jakob von Raumer]

I think we need them all:

instance is_symmetric_smul.is_scalar_tower {R α} [comm_monoid R] [mul_action R α] [has_scalar Rᵒᵖ α]
  [is_symmetric_smul R α] : is_scalar_tower Rᵒᵖ R α :=
⟨λ r' r a, by { rw [←unop_smul_eq_smul r' (r • a), smul_smul],
                change (_ * _) • _ = _, rw [mul_comm] } ⟩

[Eric Wieser]

Then it sounds like the first instance is harmless, but I'm not sure how useful it is

[Jakob von Raumer]

It wasn't harmless :grinning:

[Jakob von Raumer]

I'm slowly making progress. One thing I'm not too happy about is that tensor_product.left_has_scalar in the commutative case automatically induces an action of opposite R (a right action on the tensor product by a right action on M), while it only induces a left action if M is really a bimodule. I think that's a bit confusing.

[Jakob von Raumer]

If $R$ is commutative, do people still want asymmetric $R$-$R$-bimodules?

[Eric Wieser]

Probably not, but remember you need to not create instance diamonds in places where you don't know if R is commutative

[Jakob von Raumer]

Well, this is about deleting instances, not adding some...

[Eric Wieser]

Which instance are you considering deleting?

[Jakob von Raumer]

smul_comm_class R R M for commutative R, that would solve the issue...

[Jakob von Raumer]

...but probably cause other issues

[Jakob von Raumer]

The alternative is to just make all the constructions in the commutative case depend on an instance [is_symmetric_smul R M], which prevents us from ending up in the confusing situation I described above

[Julian Külshammer]

Regarding the question whether one wants asymmetric actions for R-R-bimodules even if R is commutative, definitely yes for some people. A typical example I'm not an expert on, but have seen is if R is a field of characteristic p and the right action is given by twisting with the Frobenius $x\mapsto x^p$ while the left action is regular. Another example I am more familiar with is to consider k-linear categories with finitely many objects as monoid objects in the category of L-L-bimodules where L is a product of fields, as many as objects in the category. Also the action here is not central.

[Jakob von Raumer]

Okay, I now did some changes based on the following situation:

• In some situations, even when $R$ is commutative, we want a left action on $M \otimes_R N$ where $M$ is a potentially asymmetric $R$-$R$-bimodule.
• In other cases we want to have $r (m \otimes n) = (rm) \otimes n (= (mr) \otimes n) = m \otimes (rn)$, this is encapsulated in the fact that we have an instance of is_symmetric_smul on the tensor product whenever we have one on $M$.

I do think this accomodates all users, but since some constructions, especially the UMP of the tensor product, seem to lie in the second case, this sometimes requires a ridiculous amount of instance arguments, like here:

theorem ext_fourfold
  [module Rᵒᵖ (Q →ₗ[R] S)] [is_symmetric_smul R (Q →ₗ[R] S)]
  [module Rᵒᵖ (P →ₗ[R] Q →ₗ[R] S)] [is_symmetric_smul R (P →ₗ[R] Q →ₗ[R] S)]
  {g h : ((M ⊗[R] N) ⊗[R] P) ⊗[R] Q →ₗ[R] S}
  (H : ∀ w x y z, g (((w ⊗ₜ x) ⊗ₜ y) ⊗ₜ z) = h (((w ⊗ₜ x) ⊗ₜ y) ⊗ₜ z)) : g = h :=
begin
  ext w x y z,
  exact H w x y z,
end

What's your thoughts on this?

[Jakob von Raumer]

So the current state is this. There's just one lemma missing from the old file, which requires me to come up with a good solution on how to derive has_scalar (opposite (units S)) M from has_scalar (opposite S) M(probably can't avoid to do it manually)...

Do you think I should PR this already to get more people to look at it? I'm afraid of already putting too much time in this...

[Oliver Nash]

@Jakob von Raumer I see you're working from a fork. Are you aware that you can request permission to create branches on the Mathlib repo and save yourself the overhead of managing a fork?

[Oliver Nash]

Glancing at your work, I see it already comprises over 1000 lines. The code looks great so I'm sure we'll be able to get this merged but this is a large amount of code so the sooner you start PRing the better. For example the results about bases of tensor products (which I actually wanted for something else recently) look like a PR on their own.

[Jakob von Raumer]

Yes, I do have the permission

[Oliver Nash]

OK cool, if you prefer a fork then that's fine too!

[Jakob von Raumer]

Oliver Nash said:

Glancing at your work, I see it already comprises over 1000 lines. The code looks great so I'm sure we'll be able to get this merged but this is a large amount of code so the sooner you start PRing the better. For example the results about bases of tensor products (which I actually wanted for something else recently) look like a PR on their own.

None of this is new, it's just the old linear_algebra.tensor_product and linear_algebra.tensor_product_basis reorganized and partly generalised to non-commutative rings. Some proofs had to be adapted by most of it is just copied over.

[Oliver Nash]

Ah OK I see. I couldn't easily figure out how to get a diff and made the wrong assumption.

[Oliver Nash]

Incidentally since we're finally talking seriously about tensor products over non-commutative rings, is anyone thinking about the corresponding results for linear maps?

[Oliver Nash]

E.g.,

import linear_algebra.basic

variables (R M N : Type*) [semiring R]
variables [add_comm_monoid M] [module R M] [add_comm_monoid N] [module R N]

example : add_comm_monoid (M →ₗ[R] N) := by apply_instance -- works

example : module R (M →ₗ[R] N) := by apply_instance -- fails because `R` not commutative!

[Oliver Nash]

I wondered if this would come up as part of the tensor product work. Did it?

[Jakob von Raumer]

The fact that these are missing actually prevents some generalisations!

[Jakob von Raumer]

The current implementation doesn't really depend on R being commutative, but having a commutative action on N.

[Oliver Nash]

Yes but if R is not commutative the definition will not provide a linear map.

[Oliver Nash]

Oh sorry, misread your remark.

[Jakob von Raumer]

Made a pull request.

[Oliver Nash]

Mathematically, if R, S, T are rings, M is an (R, S)-bimodule, and N is an (R, T)-bimodule then we can speak of R-linear maps M → N and these are an (S, T)-bimodule. I'd love to have this in Mathlib.

[Oliver Nash]

Jakob von Raumer said:

Made a pull request.

Thanks! I'll review this evening.

[Jakob von Raumer]

Oliver Nash said:

Mathematically, if R, S, T are rings, M is an (R, S)-bimodule, and N is an (R, T)-bimodule then we can speak of R-linear maps M → N and these are an (S, T)-bimodule. I'd love to have this in Mathlib.

Isn't this here?

[Jakob von Raumer]

Ah, nevermind, that's weaker than what you said.

[Oliver Nash]

I'm definitely a bit of out date as I haven't touched this stuff in ages. We might be much closer to this than I realise.

[Jakob von Raumer]

Staring at it a bit more it does use the left action on both the domain and the codomain, which prevents your generalisation, it's roughly the same problem as with the tensor product.

[Jakob von Raumer]

(Which I guess shouldn't be surprising with them being adjoints and all...)

[Oliver Nash]

I suspected this might be a prerequisite for tensor products but perhaps not.

[Jakob von Raumer]

I guess it's a prerequesite from freeing the lemmas which mix tensor products and linear maps from the commutativity presumption, which I haven't done. Maybe it should be done and both go in the same huge PR :scared:

[Oliver Nash]

Huge PRs should be a last resort. I've often been surprised at how easy it is to package up something like this into smaller pieces.

[Oliver Nash]

Btw this generalisation is well worth fighting for and very valuable. I suspect many people here are quite excited about the theory of bimodules coming to life.

[Jakob von Raumer]

Thanks for the encouragement! this actually came out of me wanting to teach Lean to some non-commutative algebraists, and I was a bit suprised about how much of mathlib relies on commutativity.

[Jakob von Raumer]

In order to fix the files depending on the tensor product: Is there a way to get a list of all files that depend on a certain file by transitivity?

[Oliver Nash]

This is probably possible with https://github.com/leanprover-community/leancrawler but I think you'll probably end up with a far bigger list than you want because if one little lemma in a file low down in the dependency tree uses tensor products you'll get a huge chunk of Mathlib.

[Alex J. Best]

You can also use leanproject for this and run some tools on the output of https://leanprover-community.github.io/leanproject.html#import-graphs

[Alex J. Best]

If you tell me a specific list of filenames I can do this for you too fairly easily, me and Johan have some WIP tools that will help with this, and I'm happy to run them

[Jakob von Raumer]

It's just linear_algebra.tensor_product on the current master branch

[Alex J. Best]

I think that list is way too big to do anything useful with, there are 590 files there

[Alex J. Best]

I can't even paste it into a zulip message

[Alex J. Best]

tensorlist

[Alex J. Best]

Probably you're best off just letting lean --make src or CI tell you what breaks

[Jakob von Raumer]

That's what would have been my plan otherwise. I guess it does trigger a lot of big recompilations to just start at at random spot, though. Maybe the best heuristic is to start with the direct descendants and hope that most of the indirect imports don't break.

[Alex J. Best]

Those are:

 linear_algebra.direct_sum.tensor_product,
 algebra.category.Module.monoidal,
 topology.algebra.affine,
 linear_algebra.affine_space.affine_equiv,
 algebra.algebra.bilinear,
 topology.algebra.continuous_affine_map,
 linear_algebra.multilinear.tensor_product

I guess grep can also find this list though!

[Jakob von Raumer]

The mathlibs docs show them as well :)

[Scott Morrison]

Jakob von Raumer said:

Thanks for the encouragement! this actually came out of me wanting to teach Lean to some non-commutative algebraists, and I was a bit suprised about how much of mathlib relies on commutativity.

Certain people wandering around on zulip, pretending they've never met a noncommutative ring...

[Jakob von Raumer]

One thing I noticed is that at many points it would be more elegant to separate the lemmas about commutative rings from the non-commutative ones, if e.g. instead of semiring R we would assume comm_semigroup R and the_other_ring_axioms R separately, with the drawback that this would make usage more verbose.
@Sebastian Ullrich mentioned that in Lean 4 it should be possible to infer one of these from the other and vice versa which seems to make separating the assumptions more attractive...

[Kevin Buzzard]

Commutative ring theory has been one of the success stories of mathlib.

[Kevin Buzzard]

I wonder whether this would have been the case if we'd tried to take the noncommutative story into account at the time. Historically what happened was that very early on I was pushing for schemes, a story where we needed a lot of commutative ring stuff, and there was nobody arguing for the noncommutative case at the time so me and my minions just defined ideals of commutative rings and then prime ideals etc etc and just kept PRing stuff

[Kevin Buzzard]

It was pointed out that there would be trouble ahead but I could never get straight from the noncommutative people whether ideal was supposed to mean left ideal or bi-ideal so I just kept pushing the commutative story, and then other people showed up and joined in (Justus Springer, Devon Tuma, the Berkeley graduate students, others I've forgotten, and now the new crowd doing products of schemes) and the commutative story just kept growing

[Scott Morrison]

Kevin has a good point. I think a great way to build a good library is to build an extremely tall and pointy lopsided one, and then hope that people come along to stop it from falling over. :-)

[Scott Morrison]

Happily in mathlib that happens.

[Patrick Massot]

This happens only if the tower builders PR to mathlib... :rolling_eyes:

[Kevin Buzzard]

I do genuinely feel guilty that this approach has caused trouble down the line, especially as I was warned that this would happen, but ultimately as Scott says we made some really tall stuff and that has had advantages because it got us noticed.

[Scott Morrison]

(I wasn't even counting non-mathlib stuff as part of the tower. They are just ephemeral dreams. :-)

[Patrick Massot]

I know, I was only trying to remind the perfectoid spaces projects authors that they should feel guilty.

[Yaël Dillies]

But I also feel very attacked with my two 5k lines branches.

[Scott Morrison]

Hopefully "attacked" in the most constructive and loving way. :-) Otherwise, sorry!

[Jakob von Raumer]

Kevin Buzzard said:

It was pointed out that there would be trouble ahead but I could never get straight from the noncommutative people whether ideal was supposed to mean left ideal or bi-ideal so I just kept pushing the commutative story, and then other people showed up and joined in (Justus Springer, Devon Tuma, the Berkeley graduate students, others I've forgotten, and now the new crowd doing products of schemes) and the commutative story just kept growing

I will definitvely quiz additional non-commutative people on their customs :D

[Kevin Buzzard]

Oh thanks!

[Jakob von Raumer]

I need to write a version of the bundled Module with a symmetric action (i.e. Module extended by an is_symmetric_smul). Any naming ideas?

[Eric Wieser]

SymmetricBiModule?

[Jakob von Raumer]

How about this: I shelve the current PR for now and do the following PRs separately and in order:

1. Create a PR fixing the use of modules towards more compatibility with non-comm algebra, meaning replacing occurrences of module R M by a symmetric R-R-action or (weaker) an R-R-bimodule wherever the non-comm generalisation would currently require it.
2. Generalise the module structure on linear maps in the way @Oliver Nash proposed it above.
3. Generalise the tensor product (the current PR).

[Kevin Buzzard]

Will this mean that whenever an undergraduate wants to talk about a vector space they'll have to say a k-k-bimodule?

[Oliver Nash]

This sounds like a very good plan to me except that I don't have a clear picture of what you have in mind for 1. Is there a simple example of such a fix?

[Oliver Nash]

(Or rather of such a situation, requiring a fix.)

[Jakob von Raumer]

Kevin Buzzard said:

Will this mean that whenever an undergraduate wants to talk about a vector space they'll have to say a k-k-bimodule?

Would symm_module k V be acceptable?

[Oliver Nash]

I presume we could have typeclass instances that provide symm_module k V from module k V + comm_ring k?

[Jakob von Raumer]

Oliver Nash said:

(Or rather of such a situation, requiring a fix.)

Well a good part of this entire thread is about such a situation: Every point where $r (m \otimes n)$ would mean $(r m) \otimes n$ instead of $(m r) \otimes n$, for example, and by exension any situation which requires the tensor product of two $R$-modules to be an $R$-module.

[Jakob von Raumer]

Oliver Nash said:

I presume we could have typeclass instances that provide symm_module k V from module k V + comm_ring k?

It would be a great help in the usage if we could have such an instance. @Julian Külshammer above said, that we might have situations, even with commutative $k$, where the canonical left and right action don't coincide. So if at all, we'd make your proposed instance low priority?

[Oliver Nash]

Jakob von Raumer said:

It would be a great help in the usage if we could have such an instance. Julian Külshammer above said, that we might have situations, even with commutative $k$, where the canonical left and right action don't coincide. So if at all, we'd make your proposed instance low priority?

Hmm this is a good point. I'm less confident we could do this and it would indeed require some care with priorities.

[Jakob von Raumer]

(It would make all the fixes needed for the current tensor product PR tremendously easier ;))

[Jakob von Raumer]

(And the usage by people like @Kevin Buzzard's linear algebra students, if $k$ is commutative)

[Oliver Nash]

Wait though, why won't we still have just plain left modules still?

[Jakob von Raumer]

We will, we just don't have the instance of their tensor product or the space of linear maps being a plain left module.

[Oliver Nash]

Right!

[Oliver Nash]

OK so the problem to be solved should only be at the level of the instances and not at the types.

[Oliver Nash]

I think this should work, subject to carefully-chosen instance priorities.

[Jakob von Raumer]

The core of the problem is that we have two different conventions in the commutative and the non-commutative world, and the best way to solve the dilemma seems to be to say "okay, let's assume the commutative case as a special situation of bimodules where needed"

[Jakob von Raumer]

Oliver Nash said:

I think this should work, subject to carefully-chosen instance priorities.

Do you mean the whole thing or the symmetry-instance in the commutative case?

[Oliver Nash]

I meant the whole thing but of course it's hard to really be sure.

[Jakob von Raumer]

Something concrete that needs to be made symmetric in order for the changes linear_algebra.tensor_product to go through is to have the ℤ action on a module to be symmetric, since otherwise compatible_smul.int and thus the ℤ actiono n the tensor product doesn't work.

[Oliver Nash]

I'm not precisely sure what this means. If m, n are elements of additive groups M, N, then there are three different things that are all mathematically equal:

• m ⊗ₜ n + m ⊗ₜ n + ... + m ⊗ₜ n
• m ⊗ₜ (n + n + ... + n)
• (m + m + ... + m) ⊗ₜ n

and at most two of these can be definitionally equal. Is this related to your question?

[Jakob von Raumer]

Not entirely. The definitional equality will always be between the first and the third term. It's just that this equality comes out of the general statement of "if $M$ is an $S$-$R$-bimodule, then $M \otimes_R N$ is an $S$-module", so we need ℤ to play the role of both $R$ and $S$ and thus act symmetrically on the left and on the right of $M$.

[Reid Barton]

I haven't been following this discussion closely but it seems like this encoding using opposite is causing a lot of trouble, how about having left_module, right_module with separate operations, bimodule, and then module R M extends bimodule R R M with the "symmetry" compatibility law?

[Reid Barton]

this is a slightly weird definition in the commutative case but it's similar to "a metric space has a metric and a topology that agree"

[Jakob von Raumer]

The intuitive argument against that for me was that it is a way bigger change. But maybe that's not a good argument.

[Jakob von Raumer]

The annoying thing then is: module R M and left_module R M are equivalent and differ only by notation. For which one do we proof all the lemmas about arbitrary modules?

[Reid Barton]

module would be only for commutative rings

[Jakob von Raumer]

That then complicates the cases @Julian Külshammer mentions above, where we do want differeent left and right actions even if the ring is commutative.

[Oliver Nash]

I don't think so, they'd just be bimodules.

[Reid Barton]

I didn't really answer your question but my intended answer would be something like "if you're doing commutative algebra, use module otherwise use left_module"

[Reid Barton]

There's probably problems with this idea because I haven't thought this through at all

[Jakob von Raumer]

Oliver Nash said:

I don't think so, they'd just be bimodules.

But if both the left and the right action are somewhat canonical structures on some M, each will make M a module and to get the desired bimodule, we'll have to locally downgrade them to a left_module and a right_module respectively, right?

[Jakob von Raumer]

Reid Barton said:

There's probably problems with this idea because I haven't thought this through at all

I think it would be the preferred idea if there was less overlap between non-commutative and commutative algebra. The overlap, I guess, is where things can go wrong.

[Oliver Nash]

Reid Barton said:

There's probably problems with this idea because I haven't thought this through at all

I think it's very hard / impossible to foresee what problems any approach may encounter. Your suggestion has the very tempting sociological advantage that it's how most / all of us actually think about this.

[Jakob von Raumer]

Reid Barton said:

I haven't been following this discussion closely but it seems like this encoding using opposite is causing a lot of trouble, how about having left_module, right_module with separate operations, bimodule, and then module R M extends bimodule R R M with the "symmetry" compatibility law?

This raises the question on whether we'd need a transfer command to create right_module lemmas from left module lemmas?

[Jakob von Raumer]

Maybe I should head over to #mathlib4 and ask whether to_additive has been ported already...

[Reid Barton]

Jakob von Raumer said:

Oliver Nash said:

I don't think so, they'd just be bimodules.

But if both the left and the right action are somewhat canonical structures on some M, each will make M a module and to get the desired bimodule, we'll have to locally downgrade them to a left_module and a right_module respectively, right?

I don't think this one is a problem in practice, basically because the math situation is the same. You just won't define a module structure for one or both of the actions

[Jakob von Raumer]

Reid Barton said:

I don't think this one is a problem in practice, basically because the math situation is the same. You just won't define a module structure for one or both of the actions

If it's not already there. Maybe you first want to tread each action separately and happily use module before, in a more specialised setting, wanting to use both. But yes, there are ways around this and it might be a super rare occasion anyway.

[Reid Barton]

M would be something you just created to describe this specific object, though.

[Reid Barton]

So the instances aren't there

[Reid Barton]

Like one construction is you have a complex vector space $V$ and you let $z$ act by $z$ on the left and by $\overline{z}$ on the right. You need a new name for this guy no matter what, and that's what gets the bimodule instance

[Jakob von Raumer]

Julian Külshammer said:

A typical example I'm not an expert on, but have seen is if R is a field of characteristic p and the right action is given by twisting with the Frobenius $x\mapsto x^p$ while the left action is regular.

Here maybe the left action is the one that's already a full module already, right?

[Jakob von Raumer]

Reid Barton said:

Like one construction is you have a complex vector space $V$ and you let $z$ act by $z$ on the left and by $\overline{z}$ on the right. You need a new name for this guy no matter what, and that's what gets the bimodule instance

Ah, okay, yes, changing the name of the carrier is a good solution.

[Jakob von Raumer]

On a slight tangent, am I the only one who thinks that smul_comm_class is a really bad name? We usually dont include "class" in the name of a type class?

[Johan Commelin]

I agree. But the lemma is already called smul_comm. So we need another name for the class. Suggestions welcome!

[Yaël Dillies]

To be fair, I much more regret has_scalar_tower. I'd be happy to have them called smul_comm_class and smul_assoc_class. But if you want to get rid of the _class we can go for is_smul_comm/is_comm_smul and is_smul_assoc/is_assoc_smul.

[Yaël Dillies]

It follows the principle that Prop-valued classes should be called is_.

[Jakob von Raumer]

Isn't it is_scalar_tower?

[Jakob von Raumer]

Since it's has_scalar, maybe scalar_comm could be a name for the class, while smul_comm is the lemma?

[Yaël Dillies]

I think we should rename has_scalar to has_smul. It's has_add, not has_addition.

[Eric Wieser]

I think "rename all the typeclasses" is reasonable, but probably deserves it's own thread

[Eric Wieser]

Also it will mean my scalar actions paper refers to things that no longer exist!

[Jakob von Raumer]

has_lsmul and has_rsmul?

[Yaël Dillies]

Eric Wieser said:

Also it will mean my scalar actions paper refers to things that no longer exist!

Paper rot :scream:

[Yaël Dillies]

Jakob von Raumer said:

has_lsmul and has_rsmul?

Sounds reasonable

[Eric Wieser]

Jakob von Raumer said:

has_lsmul and has_rsmul?

Before embarking on such a change, I'd recommend collecting the rationale for doing so into a chunk of prose and making a github issue about it.

[Eric Wieser]

(my current stance is mild opposition, mainly because I think we need a clear argument for it being useful before doubling the amount of work we do)

[Eric Wieser]

I'd also be tempted to go ahead and PR the is_symmetric_smul stuff, since I found a number of other places where I wanted it

[Jakob von Raumer]

Did you read the thread above? What's your opinion in changing the current definition of module?

[Eric Wieser]

Are you actually suggesting changing module, or just renaming it to left_module and creating something new to replace module?

[Jakob von Raumer]

Well it was @Reid Barton's suggestion at first, but I tend to agree with it the more I think about where I'd otherwise need to plug in is_symmetric_smul R M. Make module R M mean symmetric R-R-bimodule, and derive an instance for it from left_module R M whenever R is commutative.

[Eric Wieser]

Surely we want to derive a left_module instance from module though too (module.to_left_module), since all bi-modules are unimodules? We can't have both directions.

[Jakob von Raumer]

Ah, damn, you're right. Sounds pretty promising that in Lean 4 we will be able to have both...

[Jakob von Raumer]

But then maybe we should stick to the previous plan and lazily add is_symmetric_smul where needed?

[Jakob von Raumer]

Eric Wieser said:

I'd also be tempted to go ahead and PR the is_symmetric_smul stuff, since I found a number of other places where I wanted it

What other places for example?

[Jakob von Raumer]

But I'd be happy for you to PR it, happy for everything that breaks my PR into smaller pieces ^^

[Jakob von Raumer]

There's a few additional closure properties in here

[Eric Wieser]

what other places for example?

IMO docs#star_module should be stated in terms of a right action on one side, but that's annoying in commutative actions without is_symmetric_smul

[Jakob von Raumer]

Eric Wieser said:

IMO docs#star_module should be stated in terms of a right action on one side, but that's annoying in commutative actions without is_symmetric_smul

Oh, does that also contain the potential of having issues opposite (opposite R)when applied twice? :thinking:

[Heather Macbeth]

Jakob von Raumer said:

Oh, does that also contain the potential of having issues opposite (opposite R)when applied twice? :thinking:

Let me advertise two theories for a refactor that could deal with this:

• eta for structures
• some class is_opposite R S packaging an isomorphism between Rᵒᵖ and S

[Jakob von Raumer]

Ah, thanks. is "eta for structures" really a solution? We won't have eta for structures in Lean 4 either

[Heather Macbeth]

I think it was under consideration?
https://github.com/leanprover/lean4/issues/777#issuecomment-964207928

[Jakob von Raumer]

Oh cool :) I proposed it to Sebastian a while ago, and he didn't sound like Leo and him liked it

[Eric Wieser]

See the topic on left vs right modules in tensor products for some related discussion about left and right modules (which was moved from here)

[Jireh Loreaux]

What's the current status of this discussion? It would be nice to have a way to talk about bimodules and two-sided ideals in non-commutative rings sometime soon.

[Yaël Dillies]

cc @Christopher Hoskin :grinning:

[Eric Wieser]

R-S-Bimodules are possible as [module R M] [module Sᵐᵒᵖ M] [smul_comm_class R Sᵐᵒᵖ M], what we're missing is sub-bimodules

[Jireh Loreaux]

Ah, okay. I only looked for two-sided ideals. Silly me. Should I define those, or wait for something else someone is working on?

[Eric Wieser]

I think we probably want subbimodule R S M and then can define biideal R as subbimodule R R R

[Eric Wieser]

Likely with better names

[Jireh Loreaux]

ah, I was thinking just bimodule R R I but I see now why sub-bimodule makes more sense.

[Oliver Nash]

I just opened #14399 which defines right ideals. I confess I have lost track of where we are with this. Other than code duplication, is there any reason why this is a silly approach?

Actually I just wanted the result that a division ring is Artinian but I got annoyed when I realised I could only handle the left case so I copied near-minimal amount of left ideal API to allow me do what I wanted. The PR is thus a silly mixture of two things; I'm happy to split it up but first I thought I'd check here.

Is this crazy? Do we actually want to go in this direction?

[Oliver Nash]

(the obvious alternative is just to work with ideal Rᵐᵒᵖ but then all elements live in a different type which will be pain)

[Yaël Dillies]

Coming from the order theory library where everything is dualized by hand (still longing for a to_dual attribute), I would say that you should duplicate everything. It's not twice harder to write twice almost the same thing.

[Yaël Dillies]

The only problem I see is that docs#mul_opposite is irreducible, so you can't use it to easily dualize lemmas as we do with docs#order_dual.

[Yaël Dillies]

Maybe you can make it locally reducible when dualizing lemmas?

[Yaël Dillies]

... and left_ideal and right_ideal are different structures, so you can't rely on that trick when the statement mentions them.

[Eric Wieser]

the obvious alternative is just to work with ideal Rᵐᵒᵖ but then all elements live in a different type which will be pain

My vague memory was that this doesn't actually mean the right thing; but perhaps I told @Haruhisa Enomoto something wrong in their PR

[Oliver Nash]

IIUC, you are referring to this comment on #13862. I agree with your comment there.

[Oliver Nash]

For the sake of definiteness, given a (semi)ring R there are four things one can consider:

1. submodule R R -- Left ideal of R
2. submodule Rᵐᵒᵖ R -- Right ideal of R
3. submodule Rᵐᵒᵖ Rᵐᵒᵖ -- Left ideal of Rᵐᵒᵖ (corresponds to right ideal of R)
4. submodule R Rᵐᵒᵖ -- Right ideal of Rᵐᵒᵖ (corresponds to left ideal of R)

[Oliver Nash]

And you were correctly pointing out that 2 and 3 are not equal (though they do "correspond" --- mathematically, the point is that when Rᵐᵒᵖ appears as the second argument in submodule, its multiplicative structure has been forgotten so there's no difference between it and R).

[Oliver Nash]

Looking this morning, we are very nearly able to work with sub-bimodules. The only missing piece is:

import ring_theory.tensor_product

open_locale tensor_product

variables (R S M : Type*) [semiring R] [semiring S]
variables [add_comm_monoid M] [module R M] [module Sᵐᵒᵖ M] [_i : smul_comm_class R Sᵐᵒᵖ M]

example : module (R ⊗[ℕ] Sᵐᵒᵖ) M := by apply_instance -- Currently fails

[Oliver Nash]

I'll try to PR something that fixes this (today if I get time, though I'm travelling so it could be Monday).

[Oliver Nash]

For emphasis, we just need to fill the sorry below:

import ring_theory.tensor_product

open_locale tensor_product

variables (R S M : Type*) [semiring R] [semiring S]
variables [add_comm_monoid M] [module R M] [module Sᵐᵒᵖ M] [_i : smul_comm_class R Sᵐᵒᵖ M]

instance foo : module (R ⊗[ℕ] Sᵐᵒᵖ) M := sorry

-- YAY: a subbimodule:
#check submodule (R ⊗[ℕ] Sᵐᵒᵖ) M

/-- A two-sided ideal. -/
def bi_ideal := submodule (R ⊗[ℕ] Rᵐᵒᵖ) R

[Oliver Nash]

However I think we should still have a definition of def right_ideal := submodule Rᵐᵒᵖ R as proposed in my #14399.

[Oliver Nash]

(my only mild concern is that when we have true rings as opposed to semirings we might want to work with R ⊗[ℤ] Sᵐᵒᵖ but I think this shouldn't really be a problem)

[Eric Wieser]

Do we run into trouble with diamonds when M = (R ⊗[ℕ] Sᵐᵒᵖ)?

[Eric Wieser]

Oliver Nash said:

And you were correctly pointing out that 2 and 3 are not equal (though they do "correspond" --- mathematically, the point is that when Rᵐᵒᵖ appears as the second argument in submodule, its multiplicative structure has been forgotten so there's no difference between it and R).

I think I was confused when I wrote this and thought they didn't even correspond, but you're obviously right that they do. Indeed, the definition of docs#mul_opposite.has_scalar confirms that the multiplicative structure is forgotten.

[Julian Külshammer]

I should probably emphasise again that a two-sided ideal should not be called a bi-ideal. That is something else: https://ncatlab.org/nlab/show/biideal Personally, my preference would be to to rename the current ideal to left_ideal, and name a two-sided ideal just ideal, but if that is not wished for, just call it a two_sided_ideal.

[Oliver Nash]

Thanks @Julian Külshammer I do now remember you making this important point before. I'm hoping finally to push through definitions of right- and two-sided ideals in the next few days and will make sure to remember not to say "bi-ideal" anywhere.

[Oliver Nash]

As to the terminology, I wonder if we could have notation, localized to commutative/non-commutative locales that controlled whether ideal meant two-sided or left. For now I think we'll probably have to stick with ideal meaning left though.

[Oliver Nash]

I've just pushed #14465 which I think should provide a convenient theory for two-sided submodules of bimodules and in particular allow us to define two-sided ideals easily.

[Oliver Nash]

Eric Wieser said:

Do we run into trouble with diamonds when M = (R ⊗[ℕ] Sᵐᵒᵖ)?

In fact we don't because (R ⊗[ℕ] Sᵐᵒᵖ) is not a module over Sᵐᵒᵖ because our definition of tensor product only picks up auxiliary actions from the left factor. However even if we did I think this would be a diamond we could live with.

[Oliver Nash]

Highlighting a related discussion from GitHub in case anyone wants to comment.

[Oliver Nash]

The nub is that if $M$ and $N$ are $A$-modules and $A$ is an $R$-algebra, then $M \otimes_R N$ is naturally an $A$-module in two different ways, depending on whether we define: $a \cdot (m \otimes n) = (a \cdot m) ⊗ n$ (the "left option") or $a \cdot (m \otimes n) = m \otimes (a \cdot n)$ (the "right option").

If we want to work with these two different $A$-module structures using typeclasses, we need two different types indicating whether we want to pick up the left or right $A$-action. Currently in Mathlib, we just arbitrarily always take the left action (thus ignoring the action of $A$ on $N$).

I sketched out some thoughts about how to resolve this ages ago here https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.234773.20base.20change/near/240929258

[Oliver Nash]

In the case at hand, we are defining an $A \otimes_R B$-module structure on a module $M$ that carries commuting $A$-module and $B$-module structures (for $R$-algebras $A$, $B$ over a commutative ring $R$). This fine except for the case $M = A \otimes_R A$ (for $A$ commutative) when our left-only convention makes $A \otimes_R A$ admissible and get a weird module structure on $A \otimes_R A$ such that $(a \otimes b) \cdot (a' \otimes b') = (aba') \otimes b'$.

[Haruhisa Enomoto]

Oliver Nash said:

The nub is that if $M$ and $N$ are $A$-modules and $A$ is an $R$-algebra, then $M \otimes_R N$ is naturally an $A$-module in two different ways, depending on whether we define: $a \cdot (m \otimes n) = (a \cdot m) ⊗ n$ (the "left option") or $a \cdot (m \otimes n) = m \otimes (a \cdot n)$ (the "right option").

My naive mathematical feeling is that, in this case, $M \otimes_R N$ should be considered as a left $A \otimes_R A$-module, and picking up left or right $A$-action corresponds to considering ring morphisms $A \to A \otimes_R A$ defined by $a \mapsto a \otimes 1$ and $a \mapsto 1 \otimes a$.

[Oliver Nash]

@Haruhisa Enomoto I agree and I have a plan that should make this work (though it's not my current priority).

[Oliver Nash]

Oliver Nash said:

I've just pushed #14465 which I think should [...] allow us to define two-sided ideals easily.

I just returned to this PR and have put it up for review again.

[Jireh Loreaux]

I missed this during my hiatus. I'm super excited. I'll review it, but I'm not sure I'll have anything intelligent to say. I definitely would have missed that diamond previously mentioned.

[Eric Wieser]

I should have some time to look on Thursday

[Oliver Nash]

Thank you both. No rush but any comments very gratefully received!

[Oliver Nash]

Now that #14465 has been merged, it might be a good time for somebody to develop the theory of two-sided ideals. Here is how I imagine one might start:

import algebra.module.bimodule

open_locale tensor_product
open mul_opposite

local attribute [instance] tensor_product.algebra.module

/-- A two-sided ideal in a semiring `R` is a left `submodule` of `R` as a `module` over
`R ⊗[ℕ] Rᵐᵒᵖ`. -/
@[reducible] def two_sided_ideal (R : Type*) [semiring R] := submodule (R ⊗[ℕ] Rᵐᵒᵖ) R

namespace two_sided_ideal

variables (R : Type*) [semiring R] (I : two_sided_ideal R) {a b : R}

lemma mul_mem_left (h : b ∈ I) : a * b ∈ I :=
begin
  convert I.smul_mem (a ⊗ₜ 1) h,
  simp [tensor_product.algebra.smul_def],
end

lemma mul_mem_right (h : a ∈ I) : a * b ∈ I :=
begin
  convert I.smul_mem (1 ⊗ₜ op b) h,
  simp [tensor_product.algebra.smul_def],
end

/-- Forgetting the right action, a `two_sided_ideal` is just a left `ideal`. -/
def to_ideal : ideal R := subbimodule.to_submodule I

-- TODO Lots more boilerplate, presumably can be modelled on existing `ideal` API.

end two_sided_ideal

[Oliver Nash]

Note that these still require the ring to be unital but it's still some progress.

[Jireh Loreaux]

Speaking of needing the rings to be unital: this is because of the module restriction, right? We also need modules over non-unital rings. My student is currently developing the theory of Hilbert modules but currently she is doing it over a unital C*-algebra because of this requirement.

[Oliver Nash]

Yes, unitality is forced on us with the proposed setup because docs#module requires a docs#semiring rather than a docs#non_unital_semiring . To remove this I suppose we'd have to introduce some sort of non_unital_module class with the same axioms as docs#module except without the one_smul axiom (ultimately coming from docs#mul_action). And then I guess docs#submodule would then be redefined using non_unital_module (since the identity plays no role for docs#submodule) and then we would be able to have non-unital docs#submodule and left docs#ideal s.

[Oliver Nash]

I think that should do it in terms of changes to the typeclass hierarchy (just one new class) but there would also be some more work to do so that we know that A ⊗[R] B is a docs#non_unital_comm_semiring when A and B are: we currently only know this for docs#comm_semiring.

[Oliver Nash]

Hopefully that's all correct, I'm typing this off the top of my head late just before I fall asleep.

[Eric Wieser]

Is it likely that we need to generalize mul_actions too?

[Jireh Loreaux]

Let's only define non-unital mul_actions if we need to. I suspect it's less (or not at all?) necessary, but I've been wrong before!

[Junyan Xu]

How about simply define non_unital_module R M as module (unitization ℕ R) M? By the way someone should fix src#unitization.comm_semiring now that we have docs#non_unital_comm_semiring.

[Jireh Loreaux]

I'll fix docs#unitization.comm_semiring tonight. I think the unitization trick might work, and it could actually be fairly convenient.

[Junyan Xu]

If unitization is a trick then defining bimodules using action of the tensor product is definitely a bigger trick :)

[Jireh Loreaux]

#16048 for the docs#unitization.comm_semiring fix. Somebody can pop it on the queue once it passes CI (just waiting for the linter).

[Julian Külshammer]

@Oliver Nash How much of the boilerplate do you think is necessary to make your draft a valid PR? I'm imagening that some stuff would already benefit from just being able to talk about two-sided ideals, e. g. the definition of the Jacobson radical of a two-sided ideal in #13862.

[Jireh Loreaux]

Regarding the unitization trick for modules over non-unital rings: what I really want in order to make this nice is an instance module (unitization 𝕜 R) M given a hypothesis module (unitization ℕ R) M where 𝕜 is a comm_ring. In other words, in practice I want to be able to replace the ring unitization with the C⋆-algebra unitization (where 𝕜 = ℂ and R is a non-unital C⋆-algebra). Is this feasible?

[Oliver Nash]

@Julian Külshammer I'm not sure. Certainly such a PR should include lemmas like zero_mem, add_mem, sub_mem, ext, ... I'd take a careful look at the existing API for docs#submodule and docs#ideal and probably add quite a lot of what they have since code like this is fairly uncontroversial (and easy to write).

However I think there are two questions to answer before embarking on such a task:

1. Should we make two_sided_ideal a specialisation of a new subbimodule R S M structure? [probably]
2. Should we wait till we've resolved the issue that submodule R M currently requires R to be unital? [probably not]

[Oliver Nash]

If I ever get a chance to return to this PR #14399 (defining right ideals) then it should give an example of a minimal API for a new definition like this.

[Oliver Nash]

@Jireh Loreaux I think that would not be feasible because the carrier type 𝕜 in such an instance would be undetermined.

[Oliver Nash]

IIUC if you wanted to pursue this you would have to introduce a type synonym for M and use that in the instance.

[Jireh Loreaux]

Yeah, it definitely felt like this instance was "going the wrong way"

[Oliver Nash]

It makes mathematical sense though and I think we'll be able to do this sort of thing in Lean 4.

[Oliver Nash]

For now a type synonym (that captures 𝕜) should work.

[Jireh Loreaux]

Well, I'm certainly wondering at what point it makes sense to specialize all (okay, I only mean most) of the C⋆-algebra theory to ℂ, and this might be one situation.