Isomorphism of Representations

Stream: mathlib4

[Chengyan Hu]

How do I state that two Representations are isomorphic?

[Kim Morrison]

docs#Representation

[Kim Morrison]

I guess X.asModule ≃+* Y.asModule?

[Aaron Liu]

Kim Morrison said:

I guess X.asModule ≃+* Y.asModule?

Those aren't rings so you can't use a ring equiv

[Kim Morrison]

Oops, wrong equiv symbol indeed. But asModule was the actual suggestion. :-)

[Chengyan Hu]

I wrote one with Kenny yesterday

[Chengyan Hu]

variable {G M : Type*} [Group G] [AddCommGroup M]

structure Representation.Equiv {R : Type*} [CommSemiring R] {G : Type*} [Group G]
    {M₁ M₂ : Type*} [_root_.AddCommMonoid M₁] [_root_.AddCommMonoid M₂] [Module R M₁] [Module R M₂]
    (ρ₁ : Representation R G M₁) (ρ₂ : Representation R G M₂)
     extends M₁ ≃ₗ[R] M₂ where
     exchange : ∀(g : G), ∀(m : M₁), toFun (ρ₁ g m) = (ρ₂ g (toFun m))