to_additive and punit

Stream: general

[Adrián Doña Mateo]

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

[Johan Commelin]

What is the error message that it gives?

[Adrián Doña Mateo]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Adrián Doña Mateo]

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.

[Yury G. Kudryashov]

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.

[Adrián Doña Mateo]

Okay, I'll give that a go.

[Johan Commelin]

@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.

[Johan Commelin]

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

[Adrián Doña Mateo]

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

[Yury G. Kudryashov]

[unique α] gives you [default α]

[Yury G. Kudryashov]

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

[Adrián Doña Mateo]

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

[Johan Commelin]

subsingletons can be empty