group.div_self

Stream: Is there code for X?

[Kevin Buzzard]

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?

[Anne Baanen]

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.

[Eric Wieser]

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

[Kevin Buzzard]

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.

[Eric Wieser]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.