Zulip Chat Archive

Stream: maths

Topic: what's the logic with to_additive?


view this post on Zulip 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.

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?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 11 2019 at 14:22):

So the attribute is for more than autogenerating the theorems?

view this post on Zulip 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?

view this post on Zulip Chris Hughes (Mar 11 2019 at 14:23):

I think so.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 11 2019 at 14:28):

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

view this post on Zulip 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)

view this post on Zulip 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.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.

view this post on Zulip 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)!

view this post on Zulip Patrick Massot (Apr 18 2019 at 19:27):

Did you check it produces the statement you expected?

view this post on Zulip 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