Can't find instance

Stream: new members

[Antoine Chambert-Loir]

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]

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]

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

[Kevin Buzzard]

It doesn't work on master with import all

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

-- 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]

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]

So: what is the impact of those sections?

[Kevin Buzzard]

variable [monoid R] [group R] is always bad. But variables defined within a section disappear at the end of the section.

[Kevin Buzzard]

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]

I just saw that you had explained it already !
There should be a way to say — up to now, Rwas a monoid, but from now on we assume that it is a group.

[Kevin Buzzard]

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]

Antoine Chambert-Loir said:

I just saw that you had explained it already !
There should be a way to say — up to now, Rwas 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]

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]

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]

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]

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, Rwas 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]

Yeah, that's certainly better.

[Johan Commelin]

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]

Anyway, the PR is now done ! #11899

[Johan Commelin]

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

[Antoine Chambert-Loir]

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