# Zulip Chat Archive

## 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, ..equiv.add_monoid e } end instances end equiv

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

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 α := equiv.add_monoid e

Depending on your application, it might just be better to make `add_monoid α`

an assumption, and stipulate that `e`

is an`add_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