Zulip Chat Archive

Stream: general

Topic: to_additive and punit


view this post on Zulip Adrián Doña Mateo (Mar 23 2021 at 20:57):

Why does to_additive fail here? There definitely is a has_add instance for punit.

import algebra.punit_instances

example : add_group punit := infer_instance

@[to_additive foo']
lemma foo {G : Type*} [group G] : G ≃* punit := sorry

view this post on Zulip Johan Commelin (Mar 23 2021 at 20:59):

What is the error message that it gives?

view this post on Zulip Adrián Doña Mateo (Mar 23 2021 at 21:03):

type mismatch at application
  G ≃+ punit
term
  @distrib.to_has_mul punit (@ring.to_distrib punit (@comm_ring.to_ring punit punit.comm_ring))
has type
  has_mul punit
but is expected to have type
  has_add punit

view this post on Zulip Johan Commelin (Mar 23 2021 at 21:08):

ouch... it's getting the multiplication from the ring structure

view this post on Zulip Johan Commelin (Mar 23 2021 at 21:08):

What exactly are you trying to do? Can you abstract punit away? For example by using a subsingleton type?

view this post on Zulip Adrián Doña Mateo (Mar 23 2021 at 21:11):

I was hoping to define

def of_subsingleton (h : subsingleton G) : G ≃* punit :=
λ _, punit.star, λ _, 1, λ x, subsingleton.elim _ _, λ x, subsingleton.elim _ _, λ _ _, rfl

and transfer it to additive notation.

view this post on Zulip Yury G. Kudryashov (Mar 23 2021 at 21:12):

If you want to fix this, then you should define @[to_additive] instance punit.has_mul, @[to_additive] instance punit.has_one, in algebra/punit_instances, then make sure that all instances in that file use mul := (*) etc.

view this post on Zulip Adrián Doña Mateo (Mar 23 2021 at 21:15):

Okay, I'll give that a go.

view this post on Zulip Johan Commelin (Mar 23 2021 at 21:17):

@Adrián Doña Mateo So, what I would suggest is that you show that two groups G and H with [unique G] and [unique H] are isomorphic.

view this post on Zulip Johan Commelin (Mar 23 2021 at 21:18):

Then you can specialise this to H = punit whenever you want.

view this post on Zulip Adrián Doña Mateo (Mar 23 2021 at 21:19):

Oh yeah, that makes sense. What is the difference between unique and subsingleton?

view this post on Zulip Yury G. Kudryashov (Mar 23 2021 at 21:25):

[unique α] gives you [default α]

view this post on Zulip Yury G. Kudryashov (Mar 23 2021 at 21:26):

But for a [monoid], you already have 1.

view this post on Zulip Adrián Doña Mateo (Mar 23 2021 at 21:26):

Right, in this case it wouldn't matter. Thanks a lot!

view this post on Zulip Johan Commelin (Mar 23 2021 at 21:33):

subsingletons can be empty


Last updated: May 06 2021 at 22:13 UTC