Haruhisa Enomoto

Stream: new members

[Haruhisa Enomoto]

Hello everyone, my name is Haruhisa Enomoto. I'm a postdoc majoring in the representation of algebras (= studying modules over non-commutative rings).
I became interested in Lean from Natural number game, and I recentely proved some basic facts in ring theory in Lean which are not in mathlib now (characterizing Jacobson radical ideal and local ring in non-commutative ring).
I have some questions.

1. What level and kinds of maths is mathlib aiming at? I noticed e.g. some theorems in 100 theorems (and clearly "Liquid Tensor Experiment"!) are not in mathlib, so are there any criteria?
   Maybe undergrad level will be welcomed, but should graduate level math or too specialized maths be done independently from mathlib?

2. If so, how about basic non-commutative ring theory, such as Jacobson radial, non-commutative Nakayama, Artin-Wedderburn, and Hopkins-Levitzki (left artinian ring is left noetherian)?

3. Probably at least the notion of two-sided ideal and quotient ring by two-sided ideal is worth being formalized in mathlib. Are there anyone working on it?

[Kyle Miller]

Here's an overview of things that are in mathlib, to give you an idea: https://leanprover-community.github.io/mathlib-overview.html

The criteria for mathlib inclusion is roughly (1) has anyone heard of it? (2) has it been refined enough to be library code? (for example, has everything been generalized and modularized enough? is the "API" well-designed? does it seem like it will support formalizations of related theorems?)

Refinement takes a good amount of work, and there is a lot of Lean code out there that's just not in mathlib yet. Usually people work on projects and contribute little pieces as they become ready.

Noncommutative algebra is definitely in scope. I've wanted to see Jacobson radicals, Jacobson-semisimple rings, and the Artin-Wedderburn theorem.

[Kyle Miller]

There has been some discussion here on the Zulip about noncommutative algebra and how to deal with two-sided ideals. Even questions as basic as "what is the right way to talk about group representations" are still somewhat unanswered (but I think I saw a tentative(?) solution in the last week). One popular solution to two-sided modules seems to be using $A\otimes A^{op}$ modules. I sort of would like to see actual left and right actions (along with having certain constructions flip the side of the action in the natural way, which I think makes certain theorems in noncommutative algebra rather nice), but then you need to deal with figuring out how to make theorems about left modules also apply to right modules without lots of code duplication. Like a @[to_right] attribute sort of like the @[to_additive].

[Kevin Buzzard]

Hi! Yes this stuff is definitely in scope for mathlib, but as Kyle says there are some surprising problems with getting it into a suitable form. I wish I knew the way forward.

[Johan Commelin]

@Haruhisa Enomoto Welcome! I think Jacobson radical is already done (docs#ideal.jacobson). Two-sided ideals, and quotients by them, are also done.

[Johan Commelin]

The rest is very welcome, as others have said.

[Junyan Xu]

docs#ideal is left ideal, not two-sided, and docs#ideal.has_quotient and docs$ideal.jacobson assume comm_ring. #10716 seems to be the latest(?)of a series of PRs to support development of noncommutative algebra.
By the way, someone recently re-formalized Ore localization of monoids (earlier formalization).

[Johan Commelin]

Ooh, my bad. I should have double checked. I thought that docs#ideal had been refactored to two-sided ideal some time ago.

[Kevin Buzzard]

I have sometimes felt personally responsible for this "ideal = ideal of commutative ring" situation, because it was a historically early push by me and others to develop commutative algebra in Lean (when we still didn't know the answer to the question "can this system actually do MSc level commutative algebra?" back in 2017). I had thought that a more measured "Bourbaki-like" approach to ring theory (including the non-commutative case for as long as possible) might have saved us a bunch of mess later but more recently I'm wondering whether actually we got lucky, and trying to make the commutative case work earlier would have been really disspiriting.

I realise now that I am a bit unclear on the problems. Is it simply a reluctance on the part of people to have a bunch of code duplication, i.e. some new \bub_r for a right action and then a ton of duplicated code? Until we have an algorithm which writes this for us, is there a case for just biting the bullet like we did in category theory, where many limit files are 50% limits and then 50% colimits with the same structure? Or are there more fundamental issues with non-commutative algebra? I feel like at times I understand the problems well but then I don't think about them and forget.

[Eric Wieser]

Right now the problem with right actions basically come down to:

• The fails_quickly linter doesn't like the typeclass instances in #10716
• Defining x •ᵣ r (or x <• r as I've suggested before) as op r • x runs into some minor ambiguity problems (I don't recall the example right now)
• Inevitably we'll need right actions by nat and int, which create diamonds if we don't make add_comm_group uncomfortably bigger with new rnsmul and rzsmul fields

[Haruhisa Enomoto]

Thank all of you for comments! For (1), I now understand the scope of mathlib.
Acutually my code is long (using lots of tactic mode) and should be refined a lot. Since I'm a newbie, I'll learn how to write good codes by read others' code.

For right actions, I understand first we should only consider commutative rings (since there're lots of commutative ring users than non-commutative ring!).
If we consider statements about only "right" ideal or "right" modules, then we can just use the opposite ring, so maybe we don't have to care about duplication.
But when considering two-sided ideals or (left R, right S)-bimodule, then I obviously want biaction framework, and cosidering bimodule is very fundamental in module theory.
I see Eric Wieser's #10716 built such a framework.
I'm not familiar with how mathlib grows, but will this PR be available in future? What fails_quickly error means?

[Johan Commelin]

(Quick aside: tactic mode is not an issue. It is used all over the place in mathlib.)
I can't speak for Eric, but I think it's definitely the plan to have something like that PR get merged into mathlib. It has laid dormant a bit in the past few weeks (months?), but it can certainly be reprioritised if people are working on non-commutative ring theory again.

[Eric Wieser]

Arguably the framework for bimodules exists (I mention it briefly in arxiv#2108.10700), and #10716 just hooks algebra into this framework

[Eric Wieser]

I don't quite have the level of interest needed to dig into the linter failures, but am happy to keep resolving the merge conflicts every few months

[Haruhisa Enomoto]

@Eric Wieser Thank you for letting me know your paper, I'll look through it, and thank you for your a lot of contribution!

[Haruhisa Enomoto]

Then I have a (maybe general) question. If I want to contribute some ring theory using two-sided ideals now (it's just an assumption), should I use just mathlib in the current version, or use #10716 in some sense?

[Eric Wieser]

I dont think you need #10716 for that

[Eric Wieser]

You'd only need it for two-sided submodules of algebras. If you define a new sub_bi_module R S M type, then you can use sub_bi_module R R R for two-sided ideals. #10716 only comes into play if you want to start talking about sub_bi_module R A A, and that's not interesting anyway as it's the same as submodule R A.

[Haruhisa Enomoto]

OK I see, I misunderstood the aim of #10716. Thank you.

[Julian Külshammer]

Hi Haruhisa, good to see you here. I don't have much to add to the question about what is difficult to the non-commutative setting. My impression from the times I have tried was that it is quite difficult for a beginner to do large refactors of the library, one runs into unexpected time-outs and diamonds, one is not really equipped to deal with. For example this was the case when I tried to do the task (which at the time seemed not too complicated to me) to extend the polynomial ring in one variable from being over a commutative ring to a non-commutative ring. For possible directions, it seems to me that adding some basic notions of category theory / homological algebra is within the realm of possibility, maybe not for a total beginner, but for someone intermediate. For example, I wondered whether getting the definition of a (Quillen) exact category into mathlib could be a potential target. Then one can probably go on and add a lot of basic theory as laid out e.g. in "Exact categories in functional analysis". I mention it, because I would imagine you being interested in this as well.

[Eric Wieser]

Julian Külshammer said:

For example this was the case when I tried to do the task (which at the time seemed not too complicated to me) to extend the polynomial ring in one variable from being over a commutative ring to a non-commutative ring.

Wasn't this for multivariate polynomials?

[Eric Wieser]

I agree though, this type of refactor can be a substantial amount of work

[Eric Wieser]

None of which is particularly amenable to publication :(

[Julian Külshammer]

I don't quite remember, so you might be right that it was rather polynomial ring in commuting variables over a non-commutative ring.

[Haruhisa Enomoto]

Now I wrote a code about Jacobson radical and local ring for the noncommutative setting, which is available at my solo Github page:
https://github.com/haruhisa-enomoto/lean-noncommutative-ring/blob/master/src/nc_jacobson_ideal.lean
This contains:

• The intersection of all maximal left ideals (Jacobson radical) coincides with that of all maximal right ideals (expressed via opposite ring)
• The famous characterization of an elements in the Jacobson radical.
• A ring has a unique maximal left ideal (nc-local) iff it has a unique maximal right ideal (expressed via opposite ring).
• The famous characterization of nc-local rings.

Would it be worth contributing to mathlib?

[Alex J. Best]

This looks really well written and absolutely the sort mathematics that mathlib is interested in. So I would say definitely yes it is worth contributing.

[Kevin Buzzard]

Wooah that code looks really great! Well done! Have you been using Lean long? I am not an expert in the non-commutative side of things in Lean (all I know is that there are subtleties which I don't understand) but my gut feeling is that this stuff would be very much in scope.

[Yaël Dillies]

Could be mistaken for a mathlib file! Congrats!

[Yaël Dillies]

Little trick, you can use "dot notation" on your lemmas if you name them correctly. If hu : is_unit u, then to get is_unit (op u) you must do is_unit_op_of_is_unit hu. Yuck, too long. If you instead name it is_unit.op, then hu.op will do. Much shorter, and doesn't need brackets around.

[Haruhisa Enomoto]

Thank you! So could someone give me access to mathlib repository? Github name is haruhisa-enomoto.
And maybe there are two ways. First is to create a new file, second is to add noncommutative parts to ring_theory.jacobon and ring_theory.ideal.local_ring. Which is better?
I think noncommutative part is quite long (and almost trivial for commutative ring's user), it's better to separate a file.

[Kevin Buzzard]

@maintainers can GH user haruhisa-enomoto have write access to non-master branches?

[Kevin Buzzard]

Making a new file is often a good option.

[Scott Morrison]

@Haruhisa Enomoto, I've just given you write access to the mathlib repository! Looking forward to your PRs. :-)

[Haruhisa Enomoto]

Yaël Dillies said:

Little trick, you can use "dot notation" on your lemmas if you name them correctly. If hu : is_unit u, then to get is_unit (op u) you must do is_unit_op_of_is_unit hu. Yuck, too long. If you instead name it is_unit.op, then hu.op will do. Much shorter, and doesn't need brackets around.

Thanks for your advice! I'm not familiar with the dot notation, and in particular how it works.
In Structures and Records (Theorem proving in lean), the dot notation is mentioned (and it is the only one explanataion about dot notations I can find). From this I understand that the notation p.foo makes sense if the type of p is an inductive type (e.g. T) and T.foo is defined somewhere.
But in the above case, the type of hu is is_unit u (and I can't see whether it is an inductive type), and why hu.op together with is_unit.op then works?

[Haruhisa Enomoto]

Or are there any good references for the dot notation in Lean?

[Eric Rodriguez]

docs#is_unit

[Eric Rodriguez]

seems the answer is that it works with defs too :)

[Kevin Buzzard]

Either dot notation works with basically every type, or every type for which you want dot notation to work with is inductive; what I'm saying is that "inductive" is a red herring. The rule is simply the one you said: if x : T then x.foo means T.foo x or more generally T.foo _ _ .. _ x where the x is put as the first explicit input of type T in the function T.foo.

[Haruhisa Enomoto]

Thanks, I understand how to use dot notation for definitions, but I'm a little confused. In the above example, we have hu : is_unit u, so it seems to me that hu.op should mean something like (is_unit u).op hu, but we only have is_unit.op. What's happening here?

[Eric Wieser]

(is_unit u).op is resolved by lean to Prop.op (is_unit u) because is_unit u : Prop. Does that help at all?

[Eric Wieser]

Lean looks at the type of your expression, extracts the name of the head symbol, then looks for that namespace

[Haruhisa Enomoto]

Thanks, now I see.