# Zulip Chat Archive

## Stream: maths

### Topic: what's the logic with to_additive?

#### Kevin Buzzard (Mar 10 2019 at 19:51):

I need to understand `to_additive`

better because I am making PR's to mathlib which should probably involve them, and I don't want to waste other people's time.

In the above link, `multiples.is_add_submonoid`

is written by a human, but `powers.is_add_submonoid`

gets the attribute.

In the above link, `is_add_submonoid.coe_add`

seems to me to be auto-generated by the attribute.

In the above link, `add_monoid.closure_subset`

is written by a human and `monoid.closure_subset`

does not seem to get the attribute.

What is the logic here?

#### Chris Hughes (Mar 11 2019 at 14:17):

The logic I think is that sometimes autogeneration of lemmas doesn't work, and in those cases the theorems have to be proved by hand. If they don't get the attribute, they probably should have.

#### Kevin Buzzard (Mar 11 2019 at 14:22):

So the attribute is for more than autogenerating the theorems?

#### Kevin Buzzard (Mar 11 2019 at 14:22):

Even if they're generated manually they're supposed to have the attribute -- oh -- this is because later autogenerated results might need them?

#### Chris Hughes (Mar 11 2019 at 14:23):

I think so.

#### Johan Commelin (Mar 11 2019 at 14:27):

I'm just going to quickly log here that there's more stuff where the attribute is missing: https://github.com/leanprover-community/mathlib/blob/master/src/group_theory/subgroup.lean#L489-L511

#### Johan Commelin (Mar 11 2019 at 14:28):

Currently I don't have time to turn this into a PR

#### Kevin Buzzard (Mar 11 2019 at 14:35):

Just after the part you quoted, there is what looks like an incorrect definition of a simple group. We don't want the trivial group to be simple (for the same reason we don't want 1 to be prime)

#### Ramon Fernandez Mir (Apr 17 2019 at 17:20):

I was trying to find in the mathlib the lemma that says that a ring homomorphism is injective if and only iff its kernel is trivial. It turns out it's not there so I thought that that would make a good first PR. It has been proved for group homomorphisms (`is_group_hom`

) but not for additive group homomorphisms (`is_add_group_hom`

). So my first idea was to simply tag the corresponding lemmas in `group_theory/subgroup.lean`

with `to_additive`

and go from there. That didn't work:

lemma inj_of_trivial_ker (f : α → β) [is_group_hom f] (h : ker f = trivial α) : function.injective f := begin intros a₁ a₂ hfa, simp [ext_iff, ker, is_subgroup.trivial] at h, have ha : a₁ * a₂⁻¹ = 1, by rw ←h; exact inv_ker_one f hfa, rw [eq_inv_of_mul_eq_one ha, inv_inv a₂] end attribute [to_additive is_add_group_hom.inj_of_trivial_ker] is_group_hom.inj_of_trivial_ker /- type mismatch at application @trivial.equations._eqn_1 β _inst_2 term _inst_2 has type add_group β but is expected to have type group β -/

I was trying to fix it so I thought that getting rid of that `simp`

would work as it could be changing the term in a way that the tag wasn't happy with. So I did something like:

lemma inj_of_trivial_ker (f : α → β) [is_group_hom f] (h : ker f = trivial α) : function.injective f := begin intros a₁ a₂ hfa, rw ext_iff at h, dsimp only [set.preimage, ker, is_subgroup.trivial] at h, replace h := h (a₁ * a₂⁻¹), iterate 2 { erw set.mem_singleton_iff at h }, have ha : a₁ * a₂⁻¹ = 1, by rw ←h; exact inv_ker_one f hfa, rw [eq_inv_of_mul_eq_one ha, inv_inv a₂] end attribute [to_additive is_add_group_hom.inj_of_trivial_ker] is_group_hom.inj_of_trivial_ker

And it worked! Why? Should it work? Are we doing something wrong with the simplification lemmas? Maybe some `@[simp]`

tags missing? Or is there something wrong with `to_additive`

?

Then I discovered that a much cleaner way of solving it was to simply add:

attribute [to_additive is_add_subgroup.trivial.equations._eqn_1] is_subgroup.trivial.equations._eqn_1

which was the piece of information missing. However, I still think it'd be very useful if someone could clarify what's happening behind the scenes.

#### Ramon Fernandez Mir (Apr 18 2019 at 19:24):

By the way, I've PR-ed this simple change (https://github.com/leanprover-community/mathlib/pull/947)!

#### Patrick Massot (Apr 18 2019 at 19:27):

Did you check it produces the statement you expected?

#### Patrick Massot (Apr 18 2019 at 19:42):

Funny coincidence: I needed this right now for perfectoid spaces. I just added `attribute [to_additive is_add_group_hom.trivial_ker_of_inj] is_group_hom.trivial_ker_of_inj`

to our project

Last updated: May 10 2021 at 08:14 UTC