preferred definition of subobject?

Stream: new members

[Alex Mathers]

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?

[Johan Commelin]

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

[Johan Commelin]

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

[Alex Mathers]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Johan Commelin]

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

[Alex Mathers]

This is immensely helpful, thanks.

[Kevin Buzzard]

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

[Mario Carneiro]

@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

[Johan Commelin]

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

[Johan Commelin]

Or is this something that can be done in Lean?

[Mario Carneiro]

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

[Kevin Buzzard]

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?

[Mario Carneiro]

that's right

[Mario Carneiro]

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

[Johan Commelin]

I would prefer fixing the parser

[Johan Commelin]

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

[Johan Commelin]

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

[Alex Mathers]

No problem.

[Kevin Buzzard]

@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 :-)

[Johan Commelin]

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

[Johan Commelin]

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.

[Johan Commelin]

Similar things may show up with bundled subgroups.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Alex Mathers]

@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.

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

there is probably test breakage too

[Mario Carneiro]

the C++ change is pretty minimal

[Kevin Buzzard]

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.

[Mario Carneiro]

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