what's the logic with to_additive?

Stream: maths

[Kevin Buzzard]

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.

https://github.com/leanprover-community/mathlib/blob/51c31cea3e506ce8a565a828ee71dc265cc0c8e0/src/group_theory/submonoid.lean#L56

In the above link, multiples.is_add_submonoid is written by a human, but powers.is_add_submonoid gets the attribute.

https://github.com/leanprover-community/mathlib/blob/51c31cea3e506ce8a565a828ee71dc265cc0c8e0/src/group_theory/submonoid.lean#L123

In the above link, is_add_submonoid.coe_add seems to me to be auto-generated by the attribute.

https://github.com/leanprover-community/mathlib/blob/51c31cea3e506ce8a565a828ee71dc265cc0c8e0/src/group_theory/submonoid.lean#L192

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]

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]

So the attribute is for more than autogenerating the theorems?

[Kevin Buzzard]

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]

I think so.

[Johan Commelin]

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]

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

[Kevin Buzzard]

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]

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.leanwith 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]

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

[Patrick Massot]

Did you check it produces the statement you expected?

[Patrick Massot]

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