## Stream: maths

### Topic: bundling submonoids

#### Kevin Buzzard (Aug 05 2019 at 10:33):

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 (Aug 05 2019 at 10:42):

le

#### Kevin Buzzard (Aug 05 2019 at 10:42):

what have you become, Hughes?

#### Chris Hughes (Aug 05 2019 at 10:43):

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

Oh wow!

#### Kevin Buzzard (Aug 05 2019 at 10:43):

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

#### Kevin Buzzard (Aug 05 2019 at 10:44):

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

#### Chris Hughes (Aug 05 2019 at 10:48):

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 (Aug 05 2019 at 10:49):

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?

Good docs.

#### Kevin Buzzard (Aug 05 2019 at 14:16):

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 (Aug 05 2019 at 14:20):

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 (Aug 05 2019 at 14:21):

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

#### Kevin Buzzard (Aug 05 2019 at 14:21):

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 (Aug 05 2019 at 14:22):

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 (Aug 05 2019 at 14:23):

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

#### Yury G. Kudryashov (Sep 28 2019 at 20:25):

Hi, what is the current progress with bundling submonoids?

#### Yury G. Kudryashov (Sep 28 2019 at 20:48):

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

#### Amelia Livingston (Oct 27 2019 at 03:39):

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 (Oct 27 2019 at 05:19):

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 (Oct 27 2019 at 05:22):

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 (Oct 27 2019 at 05:26):

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

#### Johan Commelin (Oct 27 2019 at 05:26):

Because manually duplication will get out of sync fast

#### Amelia Livingston (Oct 27 2019 at 20:06):

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 (Oct 27 2019 at 21:24):

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

#### Simon Hudon (Oct 27 2019 at 21:37):

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 (Oct 27 2019 at 21:49):

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 (Dec 20 2019 at 18:39):

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.

Last updated: May 14 2021 at 18:28 UTC