AddGroupWithOne

Stream: mathlib4

[Johan Commelin]

Why is docs#AddGroupWithOne defined in a file called Mathlib/Data/Int/Cast/Defs.lean. I would expect stuff about Int.Cast there. But not much more...

[Jireh Loreaux]

This is probably half a porting accident. AddGroupWithOne was new to Lean 4 and backported to Lean 3. So it already existed and material around ad hoc porting always had some special treatment.

In addition, I think the main point is that you can't put it any earlier (as we do with Algebra.Group.Defs) because you actually need the cast first.

[Jireh Loreaux]

docs#AddMonoidWithOne is also in Data.Nat.Cast.Defs

[Johan Commelin]

Right, it can't go earlier, but I still expected it later, outside Int/Cast/*

[Jireh Loreaux]

Fair enough.

[Jireh Loreaux]

I guess we could just split them out into Algebra.Monoid.WithOne and Algebra.Group.WithOne or something like that.

[Yaël Dillies]

Nonono, please don't do that

[Matthew Ballard]

@Yaël Dillies can you expand?

[Yaël Dillies]

Everything under Algebra.Monoid and Algebra.Group is meant to be additivisable. AddMonoidWithOne and AddGroupWithOne are not

[Matthew Ballard]

What would you recommend for a module?

[Yaël Dillies]

Furthermore, AddMonoidWithOne and AddGroupWithOne are exactly where they should be. They are part of the core definitions needed for Nat.cast/Int.cast

[Yaël Dillies]

I would recommend leaving them as is

[Yaël Dillies]

And Jireh is wrong in that it is not a porting accident

[Yaël Dillies]

It was Gabriel Ebner who defined much before the port and put them where they are now

[Jireh Loreaux]

Yaël, did I not say they were in place and then backported? My point is that during porting we didn't think terribly hard about where these should ‌‌/ would go; I know, because I ported them (IIRC).

[Jireh Loreaux]

But nevertheless, I take your point about being additivisable. Is that convention written down anywhere? If not, let's make that happen.

[Eric Wieser]

Yaël Dillies said:

Furthermore, AddMonoidWithOne and AddGroupWithOne are exactly where they should be. They are part of the core definitions needed for Nat.cast/Int.cast

This argument seems stronger to me than the one about additivizability

[Yaël Dillies]

Jireh Loreaux said:

My point is that during porting we didn't think terribly hard about where these should ‌‌/ would go; I know, because I ported them (IIRC).

I'm on my phone right now but I'm sure Eric can show you the PR from 2022 which defined AddMonoidWithOne.

[Yaël Dillies]

Jireh Loreaux said:

But nevertheless, I take your point about being additivisable. Is that convention written down anywhere? If not, let's make that happen.

It is not yet written anywhere because it is not yet true. I'm trying to make it happen but I'm stuck at docs#MonoidHom.End, for which I might have to make an exception.

[Yaël Dillies]

At least once it becomes true (maybe modulo MonoidHom.End) we won't have bogus things like basic files about groups importing rings

[Eric Rodriguez]

We can't have such things be policed by "Yael notices some github discussion and they put a stop to it" - can we put some documentation in the folders?

[Eric Wieser]

The PR Yael is talking about is https://github.com/leanprover-community/mathlib/pull/12182

[Eric Wieser]

Though I think it was indeed motivated by Lean 4's OfNat in some way (relevant message)

[Eric Wieser]

I think the summary is that in Lean 3 we had an Algebra diamond that we could put up with, but in lean 4 we were headed towards having a diamond in numeric literals, which made the problem much more urgent.

[Yaël Dillies]

Eric Rodriguez said:

can we put some documentation in the folders?

Yes actually I am still very much in favour of putting some markdown file inside each (somewhat interesting) folder to explain what is supposed to be in there.