## Stream: general

### Topic: equiv module

#### Hoang Le Truong (Apr 28 2019 at 10:21):

I want to construct the following theorem:

if α has a  γ - module structure and α ≃ β then β has  γ - module structure
I have a problem.

import data.equiv.algebra  algebra.module
universes u v w
variables {α : Type u} {β : Type v} {γ : Type w}
open equiv

namespace equiv
section instances
variables (e : α ≃ β)
protected def has_scalar [has_scalar γ β] : has_scalar γ α := ⟨λ (a:γ)  x, e.symm ( a • e x)⟩

lemma smul_def [has_scalar γ β] (a: γ) (x : α) :
@has_scalar.smul _ _ (equiv.has_scalar e) a x = e.symm ( a • e x) := rfl

protected def mul_action [monoid γ][mul_action γ  β] : mul_action γ  α :=
{ one_smul := by simp [smul_def],
mul_smul := by simp [smul_def, mul_action.mul_smul],
..equiv.has_scalar e  }

protected def distrib_mul_action [monoid γ] [add_monoid β]  [distrib_mul_action γ  β] : distrib_mul_action γ α  :=
{ smul_add  := by simp [smul_def],
smul_zero := by simp [zero_def, smul_def, distrib_mul_action],
..equiv.mul_action e,
}

end instances
end equiv

failed to synthesize type class instance for
α : Type u,
β : Type v,
γ : Type w,
e : α ≃ β,
_inst_1 : monoid γ,
_inst_3 : distrib_mul_action γ β


How can fix it?

#### Kevin Buzzard (Apr 28 2019 at 10:28):

Yeah, you're not the only one with this sort of problem

#### Kevin Buzzard (Apr 28 2019 at 10:29):

The computer scientists are working on it

#### Chris Hughes (Apr 28 2019 at 10:29):

If you go into data.equiv.algebra, there are a bunch of definitions that will let you transfer the ring structure from alpha to beta.

#### Hoang Le Truong (Apr 28 2019 at 10:37):

@ Chris Hughes I read data.equiv.algebra but I don't understand how to fix it. What is hidden in this error?

#### Hoang Le Truong (Apr 28 2019 at 10:42):

@Kevin Buzzard Yes, I need the computer scientist to explain this error.

#### Chris Hughes (Apr 28 2019 at 10:47):

The error is that Lean doesn't know what the add_monoid structure is on α. You can fix this by putting an add_monoid structure on α like this.

import data.equiv.algebra

variables {α : Type*} {β : Type*} [add_monoid β] (e : α ≃ β)

instance foo : add_monoid α :=


Depending on your application, it might just be better to make add_monoid α an assumption, and stipulate that e is anadd_equiv

#### Hoang Le Truong (Apr 28 2019 at 11:14):

I used instance but it is error

 maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')


#### Hoang Le Truong (Apr 28 2019 at 11:15):

we knew that equiv.add_monoid e give add_monoid α from hypothesis add_monoid β
If you add H:add_monoid α monoid structure of α from H and monoid structure of α from add_monoid β can difference
If you add add_equiv you have a problem with has_scalar and has_add

#### Chris Hughes (Apr 28 2019 at 11:23):

Sorry, the instance won't work because it depends on e. I would probably make add_monoid α an assumption to your mul_action definition, and then in any application, you'll have to make it an instance yourself, using the equiv you have available.

Last updated: May 10 2021 at 00:31 UTC