Zulip Chat Archive

Stream: Is there code for X?

Topic: group.div_self


view this post on Zulip Kevin Buzzard (Mar 12 2021 at 10:03):

Are we really missing these?

import algebra.group.hom

variables {A B : Type*} [group A] [group B]
  (f : A →* B) (a1 a2 : A)

@[simp, to_additive] lemma group.div_self (a : A) : a / a = 1 :=
by simp [div_eq_mul_inv]

@[simp, to_additive] lemma monoid_hom.map_div :
  f (a1 / a2) = f a1 / f a2 :=
by simp [div_eq_mul_inv]

I noticed there was a change to the definition of group recently, with an explicit div being asked for. This has turned out to work really nicely in group cohomology. I really don't want to write g m + -m for a coboundary, and putting the emphasis on add and sub in general rather than add and neg seems to me like a good idea. Am I just not importing the right files for these two lemmas? Or is what's going on that div is now being promoted as the new inv but we didn't around to divifying everything yet?

PS smul_sub is not tagged simp. Is this for a good reason? Should monoid_hom.map_div be simp?

view this post on Zulip Anne Baanen (Mar 12 2021 at 10:08):

Or is what's going on that div is now being promoted as the new inv but we didn't around to divifying everything yet?

That is probably it. The old API was solely mul and inv based, with sub only being defined for add_groups. Now it's div everywhere, but the lemmas haven't caught up yet.

view this post on Zulip Eric Wieser (Mar 12 2021 at 11:07):

is docs#smul_add tagged simp? edit: yes, so I guess smul_sub should be too

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 10:55):

I was about to PR map_div and I'm having second thoughts. I've realised that we do have map_sub, which was what I wanted. I un-to-additived it and ended up with map_div but I'm not sure that anyone really uses division in the non-commutative case.

view this post on Zulip Eric Wieser (Mar 18 2021 at 11:09):

I can't see any reason not to have the lemma

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 12:02):

It opens up a can of worms in the noncommutative case.

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 12:05):

Actually the real reason I don't want to PR it is that I don't need it. I needed map_sub but it's there. There is this weird dichotomy amongst mathematicians. If they're using a structure which is commutative (as addition essentially always is in practice) then sub is a powerful operator. If they're using a structure which is not (e.g. groups with group law * are typically not commutative) then nobody uses div at all because there are two potential definitions, but people will happily multiply by the inverse all day long.


Last updated: May 19 2021 at 02:10 UTC