How do I make a LinearEquiv using a ring equiv?

Stream: mathlib4

[Scott Carnahan]

I have an isomorphism of rings, and modules over those rings, but I am having trouble defining a semilinear equivalence between the modules. The problem seems to be one of generating the appropriate RingHomInvPair instances from the isomorphism.

import Mathlib

def MySemilinearEquiv {R S M N : Type*} [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M]
    [AddCommMonoid N] [Module S N] (f : R ≃+* S) :
    @LinearEquiv R S _ _ f f.symm (RingHomInvPair.of_ringEquiv f) (RingHomInvPair.of_ringEquiv f).symm M N _ _ _ _ where
  toFun := sorry

I've tried a few ways to fill in the right instance, but I couldn't get anything to work reliably. Ideally, I would like way to construct a semilinear equivalence without bothering with RingHomInvPair.

[Yaël Dillies]

There you go:

import Mathlib

variable {R S M N : Type*} [Semiring R] [Semiring S]
  [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module S N] {σ : R ≃+* S}

instance : RingHomInvPair σ.toRingHom σ.symm.toRingHom where
  comp_eq := by simp
  comp_eq₂ := by simp

def MySemilinearEquiv : M ≃ₛₗ[σ.toRingHom] N := sorry

[Yaël Dillies]

Alternatively, here's a notation I just made up to specify σ' too in docs#LinearEquiv:

/-- `M ≃ₛₗ[σ, σ'] M₂` denotes the type of linear equivalences between `M` and `M₂` over a
ring homomorphisms `σ` and `σ'`. -/
notation:50 M " ≃ₛₗ[" σ ", " sigma' "] " M₂ => LinearEquiv (σ' := sigma') σ M M₂

[Scott Carnahan]

Thank you, that works well.