the future of `subring`

Stream: maths

[Kevin Buzzard]

I am afraid I am still not 100% certain of how to port a file like subring.lean to Lean 4 manually. The mathematically elegant definition

set_option old_structure_cmd true

structure subring (R : Type u) [ring R] extends subsemiring R, add_subgroup R
-- that's it

is, to my understanding, going to be replaced in Lean 4 either by

structure subring (R : Type u) [ring R] extends subsemiring R
-- list all axioms of an add_subgroup which aren't mentioned in subsemiring

or by

structure subring (R : Type u) [ring R] extends add_subgroup R
--- list all axioms of a subsemiring which aren't mentioned in add_subgroup

or perhaps by something even more complex coming from a "spanning tree in the algebra hierarchy" which lots of people seem to understand but which I still don't? @Mario Carneiro you're good at communicating with me, can you explain to me what's going on?

[Eric Wieser]

The choice between your two options is only really one of performance / elaborator happiness (how likely you are to have to insert type ascriptions), as far as I know

[Kevin Buzzard]

I just want someone to tell me the answer

[Eric Wieser]

The easy answer is just to always pick the first base class, since the choice doesn't really matter for the sake of experimental porting. If you write a bunch of theory one way, you can then swap the definition and see if anything breaks.

[Kevin Buzzard]

More precisely I would like someone to suggest Lean 4 definitions of subsemiring, subring, add_subgroup, submonoid and whatever else the CS people need. @Sebastien Gouezel and I played this game for rings already, and the results are in the mathlib4 sandbox (in master). Do you have an opinion on this Sebastien?

[Johan Commelin]

Intuitively, I would guess that the definition of sub_X closely follows the definition of X. So if ring extends semiring, then copy that choice, but if ring extends add_group, then follow that path.

[Kevin Buzzard]

Right but my understanding is that Eric is proposing that subring just be almost syntax sugar for is_subring, ditching the structure choice completely and preserving dot notation, is my understanding of it.

[Kevin Buzzard]

we do it all in the subtype monad

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/busywork/near/244409897

[Johan Commelin]

Kevin Buzzard said:

Right but my understanding is that Eric is proposing that subring just be almost syntax sugar for is_subring, ditching the structure choice completely and preserving dot notation, is my understanding of it.

Then apply my remark to is_sub_X :wink:

[Kevin Buzzard]

@Eric Wieser in Lean 3 right now we have

structure is_subring (S : set R) extends is_add_subgroup S, is_submonoid S : Prop.

This doesn't seem to be an old structure command? Would you envisage this structure being defined in a similar way in Lean 4?

[Kevin Buzzard]

Aah -- these really seem to be disjoint

[Johan Commelin]

Aah, is_sub_X is a prop, so diamonds are not an issue. I agree that using subtype is nice. It allows us to draw a very clear distinction between the data and the props.

[Johan Commelin]

Hmm, diamonds would still be annoying. In the sense that you would have to prove things twice.

[Johan Commelin]

So yes, the actual reason is that they are disjoint.

[Kevin Buzzard]

Johan Commelin said:

Intuitively, I would guess that the definition of sub_X closely follows the definition of X. So if ring extends semiring, then copy that choice, but if ring extends add_group, then follow that path.

Should we then be surprised that currently in Lean 3 is_subring R extends is_add_subgroup R, is_submonoid R but subring R extends subsemiring R and add_subgroup R?

[Johan Commelin]

Yes, that does seem slightly inconsistent.

[Kevin Buzzard]

as opposed to 0=1 inconsistent?

[Eric Wieser]

Johan Commelin said:

Hmm, diamonds would still be annoying. In the sense that you would have to prove things twice.

What type of thing are you thinking of?

[Kevin Buzzard]

If is_subring extended is_subsemiring and is_add_subgroup then you make something a subring from a submonoid add_subgroup by first making it a subsemiring.

[Kevin Buzzard]

but do we really care? Can't we just prove is_submonoid + is_add_subgroup implies is_subring and who cares about the definition?

[Kevin Buzzard]

What's wrong with

def is_subring (S : set R) := is_add_subgroup S ∧ is_submonoid S

? Why are we using structures?

[Eric Wieser]

Why are we using structures?

because it's nice to be able to write h.add_mem given h : is_subring S instead of h.1.add_mem

[Eric Wieser]

With new style structures, lean translates h.add_mem (as notation!) to h.to_is_add_subgroup.to_is_add_submonoid.add_mem automatically, without making the user write any boilerplate

[Eric Wieser]

At least, in lean 3 it does, anyway:

structure foo :=
(x : ℕ)

structure bar extends foo

structure baz extends bar

example (b : baz) : b.x = b.x :=
sorry -- goal state says `b.to_bar.to_foo.x = b.to_bar.to_foo.x`

[Eric Wieser]

Perhaps a better argument for structures is that it's nice to be able to write {add_mem := ..., mul_mem := ...} and not have to remember the order of the conjunction

[Kevin Buzzard]

I guess and is a structure, but the problem is that it would have to represent too many things

[Kevin Buzzard]

you are somehow saying that inductive props are better than logical props because they store data in a more flexible way

[Eric Wieser]

Yes, although I'm also trying to make the reverse claim for data, which is perhaps inconsistent...