RingHom for not-a-ring

Stream: mathlib4

[Alex Meiburg]

I've got a structure S that's "ugly": it's a commutative additive and multiplicative monoid, it's MulZeroOneClass, but it doesn't distribute. Sad! Well, I've got an injective function from the reals into S, and it preserves addition, mutiplication, zero and one. (It's a ZeroHom, OneHom, AddHom, and MulHom). I thought I would state this function as a RingHom, naturally.

But RingHom requires that both the input and output structures are NonAssocSemiring, sadly. This means I can't use it. I've jerry-rigged the following definition, but I don't like it:

class MinimalRing (β : Type*) extends AddZeroClass β, MulZeroOneClass β

instance (β : Type*) [NonAssocSemiring β] : MinimalRing β where

structure MinimalRingHom (α : Type*) (β : Type*) [MinimalRing α] [MinimalRing β] extends
  α →* β, α →+ β, α →ₙ* β, α →*₀ β

I then made the appropriate MinimalRingHomClass, and

instance MinimalRingHomClass.toRingHomClass [NonAssocSemiring α] [NonAssocSemiring β]
    [MinimalRingHomClass F α β] : RingHomClass F α β

and instance of MinimalRing for my structure of interest.

This gets me ... some stuff. But it's a mess and I'm wondering if there's something I should be doing differently.

[Alex Meiburg]

A few questions:

• Why does ring hom list all four of α →* β, α →+ β, α →ₙ* β, α →*₀ β? Isn't this highly redundant? What benefits does it have, and do I need to do that too?
• I could give my structure S a Module Real S structure, this part does work out. Then I guess my map would be a LinearMap, but that wouldn't say anything about multiplicative structure.
• I could define MulSemiringAction, but I also don't know if that gets me anything better.

[Alex Meiburg]

(to be clear: this is not a project that I intend to try to PR to mathlib. it's a question about how/why Mathlib defines RingHom's this way, and how I should best use it.)

[Ruben Van de Velde]

"why" is probably "because nobody considered such exotic setups" :)

[Alex Meiburg]

Sure. :) But I guess my question amounts to something more basic, like... in the definition

structure MonoidHom (M : Type u_10) (N : Type u_11) [MulOneClass M] [MulOneClass N] extends OneHom M N, M →ₙ* N :
Type (max u_10 u_11)

I see no reason _why_ there should be a MulOneClass in the definition. I mean, it makes it a "Monoid" Hom, but not just a "MulOneHom"? It should then be theorems that require the assumption MulOneClass. They need to assume it anyway to be able to talk about a MonoidHom.

It seems as though a RingHom should (in principle) only require [Add M] [Mul M] [Zero M] [One M] (and likewise for N), and then relevant theorems use the relevant properties. Right?

[Ruben Van de Velde]

My questions would be: does that actually give you a meaningful improvement? That is, are there more than about three lemmas that are true without the stronger assumptions? And would this cause a noticeable showdown? (Not saying that it would, but the kind of change that would make me nervous)

[Alex Meiburg]

As an example of some things that could be relaxed...

• Nat.uniqueRingHom could change from {R : Type u_3} [NonAssocSemiring R] : Unique (ℕ →+* R) to {R : Type u_3} [AddMonoidWith R] [Mul R] : Unique (ℕ →+* R)
• Similary for Int.castRingHom
• Appropriate versions of map_sub, map_neg, map_inv can be derived with other moderate assumptions on the input and output types (that are not quite immediate otherwise). Having these be @simp-able would be nice.
• You get the ability to do .comp, most of the stuff about injectivity / surjectivity still holds.
• Most of the theory of RingHom.ker works fine anyway, you get some ideal structure on the domain even if the codomain is ugly

[Alex Meiburg]

I have no idea about slowdowns, I have no sense for such things. (Trying to learn!)

[Junyan Xu]

See #mathlib4 > two-sided ideals @ 💬 for slowdown caused by relaxing MulAction and Module. The issue is blocking some PRs.

[Alex Meiburg]

That is a very and complicated thread xD oh no

[Alex Meiburg]

It seems like this choice dates back to 2020 in mathlib3: https://github.com/leanprover-community/mathlib3/commit/4f75760089a9a13cdeeca4a26353f93340e0e987
First, there was add_monoid_hom, which only acted on add_monoids. Understandable. That PR split it into add_hom and zero_hom, but then it was required that an add_monoid_hom actually required it to be an add_monoid.

Then in https://github.com/leanprover-community/mathlib3/commit/5f1b4500f21b62968aad9bd939625cdf2b2372a6 it was changed from
structure add_monoid_hom (M : Type*) (N : Type*) [add_monoid M] [add_monoid N] extends zero_hom M N, add_hom M N
to
structure add_monoid_hom (M : Type*) (N : Type*) [add_zero_class M] [add_zero_class N] extends zero_hom M N, add_hom M N when the add_zero_class was introduced, relaxing associativity.

[Alex Meiburg]

This was then preserved when it was ported: https://github.com/leanprover-community/mathlib4/pull/659

[Alex Meiburg]

@Eric Wieser @Winston Yin (尹維晨) is there a reason not to simply have

structure AddMonoidHom (M : Type*) (N : Type*) [Zero M] [Zero N] [Add M] [Add N]
  extends ZeroHom M N, AddHom M N

dropping AddZeroClass assumptions? So that it simply states that it preserves the additive and zero structure, which is all this object itself is really doing. All downstream theorems should continue to just work, since they have all the necessary assumptions anyway; then slowly assumptions on those can be relaxed where appropriate.

(And similar questions for MonoidHom, MonoidWithZeroHom, NonUnitalRingHom, and RingHom.)

[Alex Meiburg]

Just brainstorming for a sec, not too seriously here -- out of 2^4-1 = 15 different combinations of +*01 that we can have, there are homs for 9 combinations of these. The missing six would be:

+* -- pretty weird
+1 -- ?? PNatCastHom ??
*0 -- MulZeroHom
01 -- pretty weird
+*1  -- pretty weird
+01 -- AddMonoidWithOneHom

I think AddMonoidWithOneHom could maybe merit existing but the others have no reason

[Eric Wieser]

Alex Meiburg said:

Eric Wieser Winston Yin (尹維晨) is there a reason not to simply have

structure AddMonoidHom (M : Type*) (N : Type*) [Zero M] [Zero N] [Add M] [Add N]
  extends ZeroHom M N, AddHom M N

dropping AddZeroClass assumptions? So that it simply states that it preserves the additive and zero structure, which is all this object itself is really doing.

This has twice as many typeclass arguments so the terms are twice as big

[Eric Wieser]

Try instantiating with NormedField M and see how the two explicit terms compare

[Eric Wieser]

If you're lucky you get some common subterm elimination, but I don't think there's any guarantee of common subterms appearing.

[Alex Meiburg]

I tried a version where I split out an AddZero class which carries the Add / Zero data. Changes needed to make things work were minimal, and benchmarks improved if anything:

https://github.com/leanprover-community/mathlib4/pull/28702

[Eric Wieser]

Yes, I would expect that to avoid the performance issue

[Junyan Xu]

Looks like the overall effect is build +0.331%, lint +0.507%, though there's known benchmark noisiness at the moment. (Also benchmark summary stopped working again?)
image.png

[Junyan Xu]

Instead of introducing AddZero, why don't you just use [Add _] [Zero _]?

[Alex Meiburg]

For the reason Eric mentioned above - that then the types of any AddMonoidHom are twice as long, because you need two separate typeclasses to be inferred

[Eric Wieser]

I'd be interested to see what the performance drop is for that case

[Alex Meiburg]

As in, if it's small enough, we do that instead, to avoid the (maintainability) overhead of AddZero?

[Junyan Xu]

Some thought experiment breaking Semiring R down to "atomic" classes:

[Add R] [Zero R] [AddZeroClass R] [Std.Commutative add] [Std.Associative add]
[SMul Nat R] [CompatibleNSMul R]
[Mul R] [One R] [MulOneClass R] [Std.Associative mul]
[Pow R Nat] [CompatibleNPow R]
[NatCast R] [CompatibleNatCast R]
[MulZeroClass R] [LeftDistribClass R] [RightDistribClass R]

AddZeroClass, MulZeroClass, MulOneClass need to be "unbundled" and takes Add, Zero, Mul, One instances
CompatibleNSMul takes SMul Nat, Add, Zero
CompatibleNatCast takes NatCast, Add, Zero, One
CompatibleNPow takes Pow _ Nat, Mul, One

and I'd also be interested to see the performance impact ...

[Weiyi Wang]

If I am new to mathlib and I see these instead of [Ring R] I might panic

[Aaron Liu]

Weiyi Wang said:

If I am new to mathlib and I see these instead of [Ring R] I might panic

This is the main reason why this hasn't been done

[Junyan Xu]

I think there are talks to introduce something to expand Ring R to such a sequence of instance variable declarations. I think it's when people complained that sheafification similarly requires a long sequence of instances.

[Aaron Liu]

Junyan Xu said:

and I'd also be interested to see the performance impact ...

Based on what happened with unbundling ordered algebra I think the performance impact would be immense

[Junyan Xu]

Oh, it's called a macro. See #Is there code for X? > pushforward/pullback of sheaves @ 💬

[Alex Meiburg]

In general there could always be separate "data" classes and "prop" classes.

e.g. for semirings you have
class SemiringData T extends MulOne T, AddZero T, NatCast T, NatSMul T, NatPow T. Realistically, that would be grouped together a bit more so something like
extends MonoidData T, AddMonoidData T.

And then class Semiring is the mixin providing all appropriate axioms, and would look similar to the current definition of semiring (e.g. extending NonUnitalSemiring, NonAssocSemiring, MulOneClass)

[Alex Meiburg]

This would be kind of extreme though..

[Junyan Xu]

In my opinion NatCast, NatSMul, NatPow are inessential data and should be unbundled. Similarly I'd like to see TopologicalSpace unbundled from UniformSpace, etc.

[Junyan Xu]

If you don't require defeq for those fields and only require them to be compatible, it makes the job much easier to introduce PNatPow for Semigroup, for example.

[Violeta Hernández]

Aaron Liu said:

Junyan Xu said:

and I'd also be interested to see the performance impact ...

Based on what happened with unbundling ordered algebra I think the performance impact would be immense

Immense in which direction?

[Eric Wieser]

Alex Meiburg said:

As in, if it's small enough, we do that instead, to avoid the (maintainability) overhead of AddZero?

No, rather so that when it's large we can write down why we needed to use the approach you chose.

[Alex Meiburg]

Finished running the comparison. The performance hit from having Add/Zero synthesized separately is, as expected, pretty bad. https://github.com/leanprover-community/mathlib4/pull/28889/

[Johan Commelin]

Wait, why was this expected to have pretty bad performance?

[Eric Wieser]

Because of the larger terms, and the fact that TC search has to run more

[Johan Commelin]

But we also expect the TC search to be much simpler... but maybe that pay-off only becomes apparent when a lot more of the hierarchy has been unbundled?

[Eric Wieser]

The TC search will only be simpler for concrete types

[Eric Wieser]

Right now the issue is a theorem assuming [NormedField X] has to walk all the way down to Zero X and Add X, and cannot necessarily share any of its progress when doing so

[Eric Wieser]

Unbundling can help a little, but you're still probably in trouble when you need to define Add (Foo X) you need IsNormedField X

[Johan Commelin]

Right, but that is quite uncommon.

[Eric Wieser]

For quotient types it's pretty common I think

[Alex Meiburg]

There is (for example) 1145 hits on Loogle for theorem statements that involve Add (Prod _ _), so I think this kind of thing is fairly common.

https://loogle.lean-lang.org/?q=%28_+%3A+Prod+_+_%29+%2B+_

[Alex Meiburg]

is #28702 something we could consider merging then?

[Eric Wieser]

Not without a PR description explaining what it does and why it is a good ida

[Alex Meiburg]

Oops, yes haha. Alrighty, there ya go