Zulip Chat Archive

Stream: new members

Topic: action of subgroup inference issues


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

view this post on Zulip Yury G. Kudryashov (Jan 29 2020 at 16:39):

Could you please try to redefine subtype.group so that it will use {.. subtype.monoid}?

view this post on Zulip Yury G. Kudryashov (Jan 29 2020 at 16:39):

It's in group_theory/subgroup

view this post on Zulip Yury G. Kudryashov (Jan 29 2020 at 16:40):

I'm not sure if this will help

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

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

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

view this post on Zulip Yury G. Kudryashov (Feb 13 2020 at 05:21):

Redefined subtype.* without using subtype_instance; compiling.

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

view this post on Zulip Yury G. Kudryashov (Feb 13 2020 at 06:24):

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

view this post on Zulip Yury G. Kudryashov (Feb 13 2020 at 08:11):

See #1981


Last updated: May 15 2021 at 02:11 UTC