Zulip Chat Archive

Stream: new members

Topic: preferred definition of subobject?


view this post on Zulip Alex Mathers (Mar 20 2020 at 06:54):

Is there a currently preferred way to define a "subobject" in Lean? I noticed that for groups we have the definition

class is_subgroup (s : set G) extends is_submonoid s : Prop :=
(inv_mem {a} : a  s  a⁻¹  s)

and similarly for subrings, but for submodules we define it as a structure, more specifically it's defined as

structure submodule (α : Type u) (β : Type v) [ring α]
 [add_comm_group β] [module α β] : Type v :=
(carrier : set β),
...

Which is better?

view this post on Zulip Johan Commelin (Mar 20 2020 at 06:59):

We're slowly moving the library over to bundled subobjects (i.e., structures)

view this post on Zulip Johan Commelin (Mar 20 2020 at 07:03):

On the other hand, we might need to support both to some extent...

view this post on Zulip Alex Mathers (Mar 20 2020 at 07:16):

Thanks for the response. This leads me to the follow-up question: what should the definition of the trivial subgroup look like if I'm using the bundled definition? Let's say I want to write

def trivial_subgrp (G : Type*) [grp G] : subgrp G :=
{ carrier := {1},
one_mem' := sorry,
mul_mem' := sorry,
inv_mem' := sorry,
}

Then I want to give the "proof" of one_mem' : (1:G) \in {1}, but it's not obvious to me how to write this. It seems so simple and it's probably just an artifact of me not understanding the way sets are implemented in Lean.

view this post on Zulip Kevin Buzzard (Mar 20 2020 at 07:20):

sets are implemented in a slightly irritating way. If you defined carrier := {x | x = 1} then the proof of one_mem' would be rfl (i.e. "true by definition"). However x \in {1} unfolds to something like x = 1 \or false so it's not true by definition.

view this post on Zulip Kevin Buzzard (Mar 20 2020 at 07:20):

To fix this up, there will be a lemma in the library which says x \in {x}, and you can search for it in one of several ways.

view this post on Zulip Kevin Buzzard (Mar 20 2020 at 07:21):

import data.set.basic

example {α : Type} (a : α) : a  {a} :=
begin
  library_search
end

will tell you a way to do it, although in this case it doesn't find the canonical way to do it.

view this post on Zulip Kevin Buzzard (Mar 20 2020 at 07:25):

The best way to do it is to guess what this lemma might be called. There's a knack to this, and once you have it it really makes writing Lean code a whole lot easier. Basically you have to know the "code" for a lot of the symbols and ideas used in Lean. For example the code for is mem and the code for {x} is singleton, so the lemma you want will be called something like mem_singleton.... The problem is there will be several lemmas about being an element of a singleton set, e.g. x \in {y} \iff x = y, so we will still need to look more. If you try this:

example {α : Type} (a : α) : a  {a} := mem_singleton

in VS Code and then with your cursor just after the n in singleton type ctrl-space, you will get a list of suggested completions. You can scroll up and down them with the arrow keys, until you spot the one you want, and then press tab to get it. It's set.mem_singleton a.

view this post on Zulip Johan Commelin (Mar 20 2020 at 07:28):

@Gabriel Ebner @Mario Carneiro What is the status of the idea of redefining {x} to mean {y | y = x}?

view this post on Zulip Alex Mathers (Mar 20 2020 at 07:30):

This is immensely helpful, thanks.

view this post on Zulip Kevin Buzzard (Mar 20 2020 at 07:30):

Finally, here's how to see that singleton sets are implemented in an annoying way. first switch notation off, and then just keep unfolding the definition to see what the heck is going on.

import data.set.basic

set_option pp.notation false
example {α : Type} (a : α) : a  ({a} : set α) :=
begin
  unfold singleton,
  unfold has_insert.insert,
  unfold set.insert,
  unfold set_of,
  unfold has_emptyc.emptyc,
  unfold has_mem.mem,
  unfold set.mem,
  -- all notation now unfolded
end

If you watch the goal you will see how I have managed to generate this script. I just keep taking apart the types in the goal. Now if you comment out the set_option pp.notation false line you will see the goal has become (a = a) ∨ false which you can prove with left, refl

view this post on Zulip Mario Carneiro (Mar 20 2020 at 07:32):

@Johan Commelin When we last had this conversation (a week ago?) it got redirected to fixing the parse order to {a, b, c} = insert a (insert b (singleton c)), then adding a has_singleton typeclass in core rather than defining singleton a := insert a empty unconditionally

view this post on Zulip Johan Commelin (Mar 20 2020 at 07:33):

So this needs work on the parser. Does that mean C++?

view this post on Zulip Johan Commelin (Mar 20 2020 at 07:33):

Or is this something that can be done in Lean?

view this post on Zulip Mario Carneiro (Mar 20 2020 at 07:33):

unfortunately yes. It wouldn't normally, notations are almost always defined in lean, but {a, ..., z} is magic

view this post on Zulip Kevin Buzzard (Mar 20 2020 at 07:34):

If the has_singleton typeclass got changed then this would just require changes to core Lean lean (and a whole bunch of library fixes). Would this at least mean x \in {a,b} expands to x = b \or x = a?

view this post on Zulip Mario Carneiro (Mar 20 2020 at 07:34):

that's right

view this post on Zulip Mario Carneiro (Mar 20 2020 at 07:36):

We could also fix the order by defining set.insert a s to be {x | x \in s \/ x = a}, but this would cause the or's to be left associated when you iterate it

view this post on Zulip Johan Commelin (Mar 20 2020 at 07:39):

I would prefer fixing the parser

view this post on Zulip Johan Commelin (Mar 20 2020 at 07:40):

It shouldn't be more work in the long run, and the end result is more pleasant, I think.

view this post on Zulip Johan Commelin (Mar 20 2020 at 07:42):

@Alex Mathers Sorry for hijacking your thread. I hope you are now able to solve your problem.
We can take this discussion elsewhere.

view this post on Zulip Alex Mathers (Mar 20 2020 at 07:47):

No problem.

view this post on Zulip Kevin Buzzard (Mar 20 2020 at 07:48):

@Alex Mathers the other thing to say about subobjects is that there is no one right answer here. There is a PR to "bundle subgroups" #2140 by the way. But here is an issue. A normal subgroup is a subgroup plus some extra condition. So do we now bundle normal subgroups as well? If so, how do we prove that a normal subgroup is a subgroup? With the class is_subgroup approach we can use the type class system to do this. With the fully bundled approach, we will perhaps use the coercion system. But then if we want to prove that finitely-generated central subgroups are normal, and hence subgroups, we might end up with coercions of coercions of coercions etc. However my understanding is the community has decided that in the cases we understand best, the fully bundled approach is better than the is_ approach (for reasons I perhaps do not fully understand, although the fully bundled approach does give you access to the powerful "dot notation", where you can write H.has_one for the proof that the subgroup H has a 1, and perhaps this was what swung it).

Another approach is to fully bundle everything, and instead of having (G : Type) [group G] just have G : Group where Group is the category of groups. Again there are advantages and disadvantages to this. The community is basically trying to figure out the best way to do everything. When Lean 4 comes, the best way might change. Currently the approach seems to be to have more than one way to do things, which comes with its own set of advantages and disadvantages :-)

view this post on Zulip Johan Commelin (Mar 20 2020 at 07:53):

I think what also swung it was that simp doesn't (at least didn't) play well with type class inference.

view this post on Zulip Johan Commelin (Mar 20 2020 at 07:54):

With [is_group_hom f] you couldn't simp something like f (x * y) into f x * f y. But with bundled homs you can.

view this post on Zulip Johan Commelin (Mar 20 2020 at 07:54):

Similar things may show up with bundled subgroups.

view this post on Zulip Kevin Buzzard (Mar 20 2020 at 07:59):

And with bundling morphisms (f : group_hom G H instead of (f : G -> H) [is_group_hom f]) there were also pros and cons. One con I ran into recently with bundling morphisms was that if we define group_hom to be the obvious thing, then group_hom G H and monoid_hom G H are two ways of saying the same thing. Because of this, there is some definite agreement amongst the CS people that group_hom G H simply should not exist. But then there are issues with pushing forward and pulling back, e.g. f.map is the construction which sends a subgroup of G to a subgroup of H, except that it isn't: it's the construction which sends a submonoid of G to a submonoid of H, and one has to define e.g. f.gmap to push subgroups forward. This is a very minor issue though, compared to simp breaking.

view this post on Zulip Kevin Buzzard (Mar 20 2020 at 08:01):

The alternative is to define group_hom to be equal to monoid_hom when the inputs are groups, and then duplicate a bunch of code, which the CS people get really shirty about.

view this post on Zulip Johan Commelin (Mar 20 2020 at 08:02):

Kevin Buzzard said:

The alternative is to define group_hom to be equal to monoid_hom when the inputs are groups, and then duplicate a bunch of code, which the CS people get really shirty about.

Hmmmm, not only CS people

view this post on Zulip Johan Commelin (Mar 20 2020 at 08:02):

I think mathematicians are even more hung up about writing code that "has been written before"

view this post on Zulip Kevin Buzzard (Mar 20 2020 at 08:05):

I have always thought that defining group_hom to be a multiplication preserving map and then just proving the finitely many lemmas about group homs again in the correct namespace somehow felt like the right thing to do

view this post on Zulip Kevin Buzzard (Mar 20 2020 at 08:05):

In Shenyang Wu's group cohomology repo this is what we do

view this post on Zulip Kevin Buzzard (Mar 20 2020 at 08:06):

It's great supervising MSc projects, you're not controlled by the mathlib militia :-)

view this post on Zulip Alex Mathers (Mar 20 2020 at 08:17):

@Kevin Buzzard Thanks for the detailed response, this (and the ensuing conversation) is certainly giving me a better idea of the pros and cons of each. I see your point, I think as mathematicians we do implicitly do a lot of repeated "coercions" which might be inconvenient in the long run when getting to more complex objects. I guess we'll see.

view this post on Zulip Kevin Buzzard (Mar 20 2020 at 08:20):

Indeed we'll see. I have a half-written blog post about how mathematicians effortlessly cheat in this way, because it is manifestly legal mathematically to just observe that eg a subring is an additive subgroup -- there is nothing to prove. But when you're making subrings and subgroups this triviality becomes a map and there has to be a system for dealing with these maps in a completely painless way

view this post on Zulip Mario Carneiro (Mar 20 2020 at 08:38):

I just wrote a fix to the C++ parser to reverse the order, although I don't feel like putting in the legwork to fix everything that this breaks

view this post on Zulip Johan Commelin (Mar 20 2020 at 08:39):

I'm fine with helping fixing mathlib. But fixing C++ is not really by cup of tea (-;

view this post on Zulip Mario Carneiro (Mar 20 2020 at 08:40):

there is probably test breakage too

view this post on Zulip Mario Carneiro (Mar 20 2020 at 08:41):

the C++ change is pretty minimal

view this post on Zulip Kevin Buzzard (Mar 20 2020 at 09:13):

This came up when Shenyang and I were duplicating a bunch of code ;-) e.g. defining group_hom.ker and group_hom.range to be group_hom.comap bot (pullback of trivial subgroup) and group_hom.map top (pushforward of entire group). For bot it turned out to go much more smoothly to make it {x | x = 1} because then the kernel being the stuff which mapped to 1 was true by definition.

view this post on Zulip Mario Carneiro (Mar 20 2020 at 10:27):

https://github.com/leanprover-community/lean/pull/153


Last updated: May 06 2021 at 21:09 UTC