Zulip Chat Archive

Stream: general

Topic: subtype.* diamonds


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

With current definitions Lean fails to unify group.to_monoid subtype.group with subtype.monoid group.to_monoid. This diff makes 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`. "]

However I understand that a proper fix should modify the subtype_instance tactic, and I fail to understand how it works.

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

Motivated by https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/action.20of.20subgroup.20inference.20issues

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

Header says that subtype_instance was written by @Simon Hudon . Simon, could you please explain how it works (or even better fix it)?

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

E.g., I see that subtype.monoid has some rewrite on a rfl in the definition of one and I can't understand where it comes from.

view this post on Zulip Simon Hudon (Feb 13 2020 at 07:15):

I don't know that there's a simple solution to make those instances commute. You maybe have to prove that they are equal

view this post on Zulip Johan Commelin (Feb 13 2020 at 07:19):

But Yury gave a diff that makes them defeq, right?

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

The following code works with definition from the diff:

import group_theory.group_action

variables {M G α : Type} [monoid M] [group G]
instance subset_has_scalar [has_scalar M α] (s : set M) : has_scalar s α := ⟨λ s b, s.1  b
instance submonoid_mul_action [mul_action M α] (s : set M) [is_submonoid s] : mul_action s α :=
⟨λ x, (one_smul M x : (1 : s).1  x = x), λ x y, @mul_smul M _ _ _ x.1 y.1

variables [mul_action G α] (s : set G) [is_subgroup s]
#check mul_action.orbit_rel s α

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

It fails with current definitions, and proving equality wouldn't help.

view this post on Zulip Simon Hudon (Feb 13 2020 at 07:38):

Sorry, it's not straightforward and I won't have time to look into it in the near future

view this post on Zulip Simon Hudon (Feb 13 2020 at 07:38):

You may have to go with your version until someone can adapt the tactics

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

OK.

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

#1981


Last updated: May 11 2021 at 13:22 UTC