bundling submonoids

Stream: maths

[Kevin Buzzard]

I've embarked on a refactor changing is_submonoid to submonoid. Do people have opinions about whether we should have

instance : has_le (submonoid M) := ⟨λ S T, S.carrier ⊆ T.carrier⟩

or

instance : has_subset (submonoid M) := ⟨λ S T, S.carrier ⊆ T.carrier⟩

or both?

[Chris Hughes]

le

[Kevin Buzzard]

what have you become, Hughes?

[Chris Hughes]

Also, we shouldn't have subset for sets, just le

[Kevin Buzzard]

Oh wow!

[Kevin Buzzard]

Having learnt something about lattices, I am beginning to understand this point of view.

[Kevin Buzzard]

One might wonder about a "mathematician's interface" to Lean though.

[Chris Hughes]

I think it's almost always easier to learn some slightly different notation, than to force Lean into doing something that doesn't work very well in Lean. It's really not that hard to use le instead of subset.

[Kevin Buzzard]

I agree. But I am currently being an "engineer", editing mathlib. What about the undergraduate mathematician who doesn't care about the details but wants the interface that they expect?

[Chris Hughes]

Good docs.

[Kevin Buzzard]

inductive in_closure (s : set M) : M → Prop
| basic {a : M} : a ∈ s → in_closure a
| one : in_closure 1
| mul {a b : M} : in_closure a → in_closure b → in_closure (a * b)

def closure (s : set M) : submonoid M :=
{ carrier := in_closure s,
  one_mem' := in_closure.one s,
  mul_mem' := λ _ _, in_closure.mul}

There are two ways to do monoid closure of a subset. One is this inductive prop way, and the other is just taking the Inf of all the submonoids containing s. Should both be in mathlib? If not, which one?

[Chris Hughes]

It doesn't matter so long as you prove they're equivalent. You definitely want to define the recursor if you use the Inf definition.

[Johan Commelin]

Does it matter? The API should make sure that the user can not find out what the definition is (-;

[Kevin Buzzard]

I don't know if it matters. I just noted that for submonoids we had the inductive prop and for submodules we had the Inf

[Kevin Buzzard]

Does it matter? The API should make sure that the user can not find out what the definition is (-;

Oh right! I'll go back and mark everything as irreducible :-)

[Johan Commelin]

I wouldn't mind if mathlib would experiment more with this (-;

[Yury G. Kudryashov]

Hi, what is the current progress with bundling submonoids?

[Yury G. Kudryashov]

Let me tag @Kevin Buzzard @Johan Commelin @Chris Hughes

[Amelia Livingston]

Hi, what is the current progress with bundling submonoids?

Hi @Yury G. Kudryashov and others; sorry for the delay as I haven't been doing much Lean since term started. But the branch bundled_submonoids_etc is ready to PR (I think; I want to check it through in the morning). Unbundled submonoids are still there but bundled ones are too. The only things in the library that can be refactored to depend on these before we've also bundled subgroups are some lemmas in group_theory\coset.lean, algebra\commute.lean and ring_theory\localization.lean. I've done the first two but in this PR I haven't touched localization, because I've refactored that to PR a couple of PRs after this one.

There are also a couple of lemmas that I needed for later stuff about congruence relations/localization/etc.

I've started bundling subgroups, not on a branch, but I'm not prioritising it at the moment and I'm also unsure how to approach it. I extended bundled submonoids, and now I could just duplicate every lemma in group_theory\submonoid.lean so that given a subgroup S you can write S.list_prod_mem instead of having to write S.1.list_prod_mem or S.to_submonoid.list_prod_mem, for example. Or the user could just be told in the docs to write S.1 instead of S for some lemmas. I don't know. (I've got the same question about the localization refactor; I've commented out tons of lemmas where you can essentially use the version for localizations of comm monoids, which is another file, but it might confuse users.)

[Johan Commelin]

I don't know the answer to this question. Can @Mario Carneiro or @Rob Lewis or @Reid Barton shed some light on how to deal with this? It sounds like bad design to duplicate the API. But S.to_submonoid.foobar isn't very nice either.

[Mario Carneiro]

I think the easiest thing to do would be to just duplicate the api. The theorems should just be redirects, but note that the statements are actually different - things like \mem will be finding a different typeclass instance so it's not exactly the same thing (it is defeq though so the proof should be trivial)

[Johan Commelin]

We have a similar thing with {mv_,}power_series and *_hom. Are we approaching enough examples to try to automate this?

[Johan Commelin]

Because manually duplication will get out of sync fast

[Amelia Livingston]

Thanks Mario! I've realised I haven't refactored algebra\commute.lean nearly as much as I could; I made a start and almost-duplicated whatever I needed to. This makes naming difficult though. Might just leave that file as it was last night for this PR.
Bundling substructures does in general seem to lead to a lot of almost-duplication and convoluted names and I'm not familiar with that file, what's best for it, or how much depends on it.

I'm gonna open a PR; I don't know how to use git so I branched off bun_subs_with_new_toadditive to make bundled_submonoids_etc and deleted the added files that I'm PR'ing after this, so it's gonna say I want to merge about 80 commits because of all the commits on bun_subs_with_new_toadditive. Does this matter if everything gets squashed in the end?

[Kevin Buzzard]

I've seen plenty of PR's with a gazillion commits with names like "oops" and nobody seems to care.

[Simon Hudon]

When you write a PR, the goal is to make the reviewers jobs easier. We don't want to squash the commits until we merge so that if we look several times at your PR, it's easier to identify what changed. As for meaningful commit messages, if you just fix a typo, no need for a long explanation. If you make a significant change, it's good to see where it happens and have a hint in the message as to what happened in there.

[Amelia Livingston]

Okay. Most of the commit messages are vaguely meaningful, but the majority are about files not in the PR.
I can note in the PR where most of the relevant commits are.

[James Weaver]

I've always found in software projects that having a policy of doing at least a rebase -i before raising a PR helps with keeping the history of the master branch a lot cleaner.