coe_is_monoid_hom transitivity

Stream: Is there code for X?

[Vasily Nesterov]

I have 3 monoids A B C and there are coercions A → B, B → C, which are monoid homomorphisms. It would be convenient if Lean inferred coe_is_monoid_hom A Cby transitivity on its own. So I need something like that:

variables (A B C : Type*) [mul_one_class A] [mul_one_class B] [mul_one_class C]

instance trans [has_lift_t A B] [has_lift_t B C]
  [coe_is_monoid_hom A B] [coe_is_monoid_hom B C] : coe_is_monoid_hom A C := sorry

Is there a reason why it's not in mathlib? If no, I can do it and make a PR. If yes, how can I work around the problem?

[Jireh Loreaux]

The class coe_is_monoid_hom is very new, so it's possible there is API missing, but in this case I think the problem is that B becomes a metavariable in type class search.

[Jireh Loreaux]

If you #lint right after this instance you get a dangerous_instance warning right?

[Jireh Loreaux]

@Anne Baanen will know the plan for this type class.

[Eric Wieser]

Normally the way to express this would be

variables (A B C : Type*) [monoid A] [monoid B] [monoid C]
variables [mul_action A B] [mul_action B C] [is_scalar_tower A B C]

[Eric Wieser]

but in this case I think the problem is that B becomes a metavariable in type class search, so we can't actually have this instance. You could make it a def though.

I think the instance is safe because B is encoded as an implicit argument of coe_is_monoid_hom

[Anne Baanen]

I haven't been able to get around to implementing this but the plan is indeed to have this as an instance (and I designed the classes so that it can be an instance without issues)

[Vasily Nesterov]

@Anne Baanen It's nice. If you don't mind, I could implement this (transitivity of coercions preserving various algebraic structures presented in algebra.hom.group and algebra.hom.group_action).

Actually I've already tried to do this, because it's necessary for my other project. But I ran into an annoying problem: we can't just imitate lift_trans in which we have has_lift_t B C and only has_lift A B (instead has_lift_t), because chain of coercions may contain non-monoid types. So we need to use has_lift_t in both cases. But then Lean can't infer lifting from A to C by lift_trans. The best thing I came up with is explicitly specify the coercion:

instance coe_is_monoid_hom_trans [AB_lift : has_lift_t A B] [BC_lift : has_lift_t B C]
  [AB_hom : coe_is_monoid_hom A B] [BC_hom : coe_is_monoid_hom B C] :
  @coe_is_monoid_hom A C ⟨BC_lift.lift ∘ AB_lift.lift⟩ _ _ := sorry

What do you think?

[Jireh Loreaux]

Please don't, see: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Please.20stop.20adding.20generalized.20API.20around.20coercions