equiv module

Stream: general

[Hoang Le Truong]

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]

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

[Kevin Buzzard]

The computer scientists are working on it

[Chris Hughes]

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]

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

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

[Chris Hughes]

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 anadd_equiv

[Hoang Le Truong]

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]

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]

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.