# Zulip Chat Archive

## Stream: new members

### Topic: action of subgroup inference issues

#### Anne Baanen (Jan 29 2020 at 15:10):

I have a group and want to talk about the action of a certain subgroup, but run into issues with typeclass inference. The following is the specific example that I want to get working:

import group_theory.group_action -- My plan is to define a `mul_action` instance on any submonoid, then use inference to get it for a specific set. variables {α β : Type} [monoid α] instance subset_has_scalar (s : set α) [has_scalar α β] : has_scalar s β := ⟨λ s b, s.1 • b⟩ instance submonoid_mul_action (s : set α) [mul_action α β] [is_submonoid s] : mul_action s β := ⟨λ x, (one_smul α x : (1 : s).1 • x = x), λ x y, @mul_smul α _ _ _ x.1 y.1⟩ variables {α β} [group α] [mul_action α β] (s : set α) [is_subgroup s] -- these are concrete values in my situation #check mul_action.orbit_rel s β -- error : failed to synthesise instance for `mul_action ↥s β`

The problem seems to be a mismatch between the `monoid`

instances inferred. With `pp.all`

on, the `submonoid_mul_action`

instance looks like:

@mul_action.{0 0} (@coe_sort.{1 2} (set.{0} ?M_1) (@set.has_coe_to_sort.{0} ?M_1) s) ?M_2 (@subtype.monoid.{0} ?M_1 ?M_3 s _inst_3)

and Lean is trying to infer:

@mul_action.{0 0} (@coe_sort.{1 2} (set.{0} α) (@set.has_coe_to_sort.{0} α) s) β (@group.to_monoid.{0} (@coe_sort.{1 2} (set.{0} α) (@set.has_coe_to_sort.{0} α) s) (@subtype.group.{0} α _inst_2 s _inst_4))

How do I convince Lean that `group.to_monoid (subtype.group ...)`

should coincide with `subtype.monoid`

? (It definitely does in the specific example.)

Or is there another way to set it up so that I can write `mul_action.orbit_rel s β`

without an error, without manually writing each instance on `s`

?

#### Yury G. Kudryashov (Jan 29 2020 at 16:39):

Could you please try to redefine `subtype.group`

so that it will use `{.. subtype.monoid}`

?

#### Yury G. Kudryashov (Jan 29 2020 at 16:39):

It's in `group_theory/subgroup`

#### Yury G. Kudryashov (Jan 29 2020 at 16:40):

I'm not sure if this will help

#### Kevin Buzzard (Jan 29 2020 at 16:52):

Just to comment that one of the mul_actions uses `_inst_3`

and the other uses `_inst_2`

and `_inst_4`

so they are almost certainly not defeq. You can probably see in the local context what is going on.

#### Anne Baanen (Jan 29 2020 at 16:54):

Could you please try to redefine

`subtype.group`

so that it will use`{.. subtype.monoid}`

?

That doesn't seem to help, unfortunately: still the same error

#### Anne Baanen (Jan 29 2020 at 16:59):

Adding an extra instance declaration with an explicit `monoid s`

parameter works, but it seems ugly to have two instances with exactly the same definition:

instance subgroup_mul_action {α β} [group α] [mul_action α β] (s : set α) [is_subgroup s] : @mul_action s β (group.to_monoid _):= ⟨one_smul α, λ x y, @mul_smul α _ _ _ x.1 y.1⟩

#### Yury G. Kudryashov (Feb 13 2020 at 05:21):

Redefined `subtype.*`

without using `subtype_instance`

; compiling.

#### Yury G. Kudryashov (Feb 13 2020 at 06:18):

These definitions make it work:

diff --git a/src/group_theory/subgroup.lean b/src/group_theory/subgroup.lean index d54cd8eba..ac0b1dbcb 100644 --- a/src/group_theory/subgroup.lean +++ b/src/group_theory/subgroup.lean @@ -50,11 +50,13 @@ theorem multiplicative.is_subgroup_iff @[to_additive add_group] instance subtype.group {s : set α} [is_subgroup s] : group s := -by subtype_instance +{ inv := λ x, ⟨(x:α)⁻¹, is_subgroup.inv_mem x.2⟩, + mul_left_inv := λ x, subtype.eq $ mul_left_inv x.1, + .. subtype.monoid } @[to_additive add_comm_group] instance subtype.comm_group {α : Type*} [comm_group α] {s : set α} [is_subgroup s] : comm_group s := -by subtype_instance +{ .. subtype.group, .. subtype.comm_monoid } @[simp, to_additive] lemma is_subgroup.coe_inv {s : set α} [is_subgroup s] (a : s) : ((a⁻¹ : s) : α) = a⁻¹ := rfl diff --git a/src/group_theory/submonoid.lean b/src/group_theory/submonoid.lean index e9fa5895e..c644e06d9 100644 --- a/src/group_theory/submonoid.lean +++ b/src/group_theory/submonoid.lean @@ -221,12 +221,17 @@ end is_submonoid /-- Submonoids are themselves monoids. -/ @[to_additive add_monoid "An `add_submonoid` is itself an `add_monoid`."] instance subtype.monoid {s : set α} [is_submonoid s] : monoid s := -by subtype_instance +{ one := ⟨1, is_submonoid.one_mem s⟩, + mul := λ x y, ⟨x * y, is_submonoid.mul_mem x.2 y.2⟩, + mul_one := λ x, subtype.eq $ mul_one x.1, + one_mul := λ x, subtype.eq $ one_mul x.1, + mul_assoc := λ x y z, subtype.eq $ mul_assoc x.1 y.1 z.1 } /-- Submonoids of commutative monoids are themselves commutative monoids. -/ @[to_additive add_comm_monoid "An `add_submonoid` of a commutative `add_monoid` is itself a commutative `add_monoid`. "] instance subtype.comm_monoid {α} [comm_monoid α] {s : set α} [is_submonoid s] : comm_monoid s := -by subtype_instance +{ mul_comm := λ x y, subtype.eq $ mul_comm x.1 y.1, + .. subtype.monoid } /-- Submonoids inherit the 1 of the monoid. -/ @[simp, to_additive "An `add_submonoid` inherits the 0 of the `add_monoid`. "]

#### Yury G. Kudryashov (Feb 13 2020 at 06:24):

See also https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/subtype.2E*.20diamonds

#### Yury G. Kudryashov (Feb 13 2020 at 08:11):

See #1981

Last updated: May 15 2021 at 02:11 UTC