# Zulip Chat Archive

## Stream: new members

### Topic: Can't find instance

#### Antoine Chambert-Loir (Feb 07 2022 at 14:02):

Hi. Could anyone please explain why instance resolution works in the first case (`stabilizer.submonoid`

) but not in the second one (`stabilizer`

) ? (The strange thing is that the same lines in a bigger file compile without any error, but the problem appeared when I tried to incorporate them in `group_theory.group_action.sub_mul_action.lean`

)

```
-- Stabilizer of sub_mul_action
import tactic
import group_theory.group_action.sub_mul_action
universes u u' u'' v
variables {S : Type u'} {T : Type u''} {R : Type u} {M : Type v}
open mul_action
variables [monoid R] [mul_action R M]
variables [monoid S] [has_scalar S R] [mul_action S M] [is_scalar_tower S R M]
variable {p : sub_mul_action R M}
/-- Stabilizers in monoid sub_mul_action coincide with stabilizer -/
lemma stabilizer_of_sub_mul.submonoid (m : p) :
stabilizer.submonoid R m = stabilizer.submonoid R (m : M) :=
begin
ext,
simp only [mul_action.mem_stabilizer_submonoid_iff,
← sub_mul_action.coe_smul, set_like.coe_eq_coe]
end
variable [group R]
lemma stabilizer_of_sub_mul (m : p) :
stabilizer R m = stabilizer R (m : M) :=
begin
rw ← subgroup.to_submonoid_eq,
have this : (stabilizer G y).to_submonoid = stabilizer.submonoid G y := rfl,
rw this,
have this : (stabilizer G (y : X)).to_submonoid = stabilizer.submonoid G (y : X) := rfl,
rw this,
exact stabilizer_of_sub_mul.submonoid y,
end
```

#### Johan Commelin (Feb 07 2022 at 14:04):

Can you find out what the instance is that is found in the bigger file? (By clicking around in the info-view, drilling down the widgets.)

#### Johan Commelin (Feb 07 2022 at 14:04):

Because it sounds like you might just need an extra `import`

.

#### Kevin Buzzard (Feb 07 2022 at 14:16):

It doesn't work on master with `import all`

#### Kevin Buzzard (Feb 07 2022 at 14:17):

What is the bigger file, and does it have any instances or local instances in it?

#### Kevin Buzzard (Feb 07 2022 at 14:20):

waitwaitwait, your problem is that R is both a group and a monoid; your tactic state has `_inst_1 : monoid R`

and also `_inst_7 : group R`

so you have two unrelated multiplications on R. If you want to prove lemmas about monoids and then later on lemmas about groups then either use a different letter or use sections.

#### Kevin Buzzard (Feb 07 2022 at 14:22):

Yeah, the lemma statement compiles if you change `[monoid R]`

to `[group R]`

right at the top so you might have to put the first lemma in a section and then restate all the variables in a second section but with R being a group not a monoid.

#### Kevin Buzzard (Feb 07 2022 at 14:23):

```
-- Stabilizer of sub_mul_action
import tactic
import group_theory.group_action.sub_mul_action
import all
universes u u' u'' v
variables {S : Type u'} {T : Type u''} {R : Type u} {M : Type v}
open mul_action
section monoidy_stuff
variables [monoid R] [mul_action R M]
variables [monoid S] [has_scalar S R] [mul_action S M] [is_scalar_tower S R M]
variable {p : sub_mul_action R M}
/-- Stabilizers in monoid sub_mul_action coincide with stabilizer -/
lemma stabilizer_of_sub_mul.submonoid (m : p) :
stabilizer.submonoid R m = stabilizer.submonoid R (m : M) :=
begin
ext,
simp only [mul_action.mem_stabilizer_submonoid_iff,
← sub_mul_action.coe_smul, set_like.coe_eq_coe]
end
end monoidy_stuff
section groupy_stuff
variables [group R] [mul_action R M]
variables [monoid S] [has_scalar S R] [mul_action S M] [is_scalar_tower S R M]
variable {p : sub_mul_action R M}
lemma stabilizer_of_sub_mul (m : p) :
stabilizer R m = stabilizer R (m : M) :=
begin
rw ← subgroup.to_submonoid_eq,
have this : (stabilizer G y).to_submonoid = stabilizer.submonoid G y := rfl,
rw this,
have this : (stabilizer G (y : X)).to_submonoid = stabilizer.submonoid G (y : X) := rfl,
rw this,
exact stabilizer_of_sub_mul.submonoid y,
end
end groupy_stuff
```

#### Antoine Chambert-Loir (Feb 07 2022 at 14:24):

Kevin Buzzard said:

Yeah, the lemma statement compiles if you change

`[monoid R]`

to`[group R]`

right at the top so you might have to put the first lemma in a section and then restate all the variables in a second section but with R being a group not a monoid.

It seems that you're right : the file that worked had sections :

```
import tactic
import group_theory.group_action.sub_mul_action
section sub_mul_action
open mul_action
section monoid
variables {G : Type*} [monoid G] {X : Type*} [mul_action G X]
/-- Stabilizers in monoid sub_mul_action coincide with stabilizer -/
lemma stabilizer_of_sub_mul.submonoid { Y : sub_mul_action G X } (y : Y) :
stabilizer.submonoid G y = stabilizer.submonoid G (y : X) :=
begin
ext g,
simp only [mem_stabilizer_submonoid_iff,
← sub_mul_action.coe_smul, set_like.coe_eq_coe]
end
/-- Orbits in sub_mul_action coincide with orbits -/
-- useful ?
lemma orbit_of_sub_mul {Y : sub_mul_action G X} (y : Y) :
(orbit G y : set X) = orbit G (y : X) := rfl
end monoid
section group
open mul_action
variables {G : Type*} [group G] {X : Type*} [mul_action G X]
/-- Stabilizers in sub_mul_action coincide with stabilizer -/
lemma stabilizer_of_sub_mul {Y : sub_mul_action G X} (y : Y) :
stabilizer G y = stabilizer G (y : X) :=
begin
rw ← subgroup.to_submonoid_eq,
exact stabilizer_of_sub_mul.submonoid y,
end
end group
end sub_mul_action
```

#### Antoine Chambert-Loir (Feb 07 2022 at 14:24):

So: what is the impact of those sections?

#### Kevin Buzzard (Feb 07 2022 at 14:24):

`variable [monoid R] [group R]`

is always bad. But variables defined within a section disappear at the end of the section.

#### Kevin Buzzard (Feb 07 2022 at 14:25):

Something I do personally is that I always make my section names not equal to namespace names, because then when I see `end groupy_stuff`

I know that this is the end of a section and not a namespace.

#### Antoine Chambert-Loir (Feb 07 2022 at 14:25):

I just saw that you had explained it already !

There should be a way to say — up to now, `R`

was a monoid, but from now on we assume that it is a group.

#### Kevin Buzzard (Feb 07 2022 at 14:26):

The problem in your case is that `mul_action R M`

and `is_scalar_tower S R M`

already all used `_inst_1`

so you have to restate them to use `_inst_7`

.

#### Johan Commelin (Feb 07 2022 at 14:28):

Antoine Chambert-Loir said:

I just saw that you had explained it already !

There should be a way to say — up to now,`R`

was a monoid, but from now on we assume that it is a group.

I agree, it would be pretty cool to have `unvariables [monoid R]`

.

#### Kevin Buzzard (Feb 07 2022 at 14:28):

We think of group as a propositional extension of a monoid but Lean doesn't because it wants to know the inverse function; we know one exists uniquely but my guess is that this would be a can of worms for Lean. Similarly we think of fields as being a predicate on rings but Lean doesn't.

#### Kevin Buzzard (Feb 07 2022 at 14:29):

I worked out an example of this with a student recently; he had a ring which he wanted to promote to a field at some point so we used `is_field`

and it's a bit of a minefield; in the end we went with `[fact (is_field R)]`

and made the (noncomputable) field instance using type class inference, which worked.

#### Antoine Chambert-Loir (Feb 07 2022 at 14:44):

We can make a similar remark from model theory : the language of Rings has 0, 1, +, - and * — it has subtraction as an elementary law — and the language of Fields is the same : division is not put in. So that basic formulas, even written in fields, have no division. This is not necessarily annoying because you can emulate them with existential quantifiers. But when one proves quantifier elimination in (algebraically closed, say) fields, this implies that you can really remove all division signs.

#### Antoine Chambert-Loir (Feb 07 2022 at 14:45):

Johan Commelin said:

Antoine Chambert-Loir said:

I just saw that you had explained it already !

There should be a way to say — up to now,`R`

was a monoid, but from now on we assume that it is a group.I agree, it would be pretty cool to have

`unvariables [monoid R]`

.

I would rather have `upgrade [group R] from [monoid R]`

so that we are not forced to rewrite all the intermediate variables (from types such as `mul_action R M`

) that already depended on `R `

.

#### Johan Commelin (Feb 07 2022 at 14:47):

Yeah, that's certainly better.

#### Johan Commelin (Feb 07 2022 at 14:47):

No idea how feasible it would be to do that Lean-wise. But I suppose it can easily be done in Lean 4.

#### Antoine Chambert-Loir (Feb 07 2022 at 14:49):

Anyway, the PR is now done ! #11899

#### Johan Commelin (Feb 07 2022 at 14:59):

@Antoine Chambert-Loir I left two comments about the docstrings (and renamed the PR)

#### Antoine Chambert-Loir (Feb 08 2022 at 12:50):

Thanks, and I committed them at once ! Eric made an important comment as well. And Rob removed the *easy* tag!

Last updated: Dec 20 2023 at 11:08 UTC