# Transfer algebraic structures across `Equiv`s #

This continues the pattern set in `Mathlib/Algebra/Group/TransferInstance.lean`.

source
@[reducible, inline]
abbrev Equiv.module (R : Type u_1) {α : Type u_2} {β : Type u_3} [Semiring R] (e : α ≃ β) [AddCommMonoid β] :
have x := e.addCommMonoid; [Module R β] → Module R α

Transfer `Module` across an `Equiv`

Equations

- @Equiv.module R α β inst✝¹ e inst✝ = fun [Module R β] => let __src := Equiv.distribMulAction R e; { toDistribMulAction := __src, add_smul := ⋯, zero_smul := ⋯ }

Instances For

source
def Equiv.linearEquiv (R : Type u_1) {α : Type u_2} {β : Type u_3} [Semiring R] (e : α ≃ β) [AddCommMonoid β] [Module R β] :
let addCommMonoid := e.addCommMonoid; have module := Equiv.module R e; α ≃ₗ[R] β

An equivalence `e : α ≃ β` gives a linear equivalence `α ≃ₗ[R] β` where the `R`-module structure on `α` is the one obtained by transporting an `R`-module structure on `β` back along `e`.

Equations

- Equiv.linearEquiv R e = { toFun := e.addEquiv.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := e.addEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[reducible, inline]
abbrev AddEquiv.module {α : Type u_2} {β : Type u_3} (A : Type u_4) [Semiring A] [AddCommMonoid α] [AddCommMonoid β] [Module A β] (e : α ≃+ β) :
Module A α

Transport a module instance via an isomorphism of the underlying abelian groups. This has better definitional properties than `Equiv.module` since here the abelian group structure remains unmodified.

Equations

- AddEquiv.module A e = { toSMul := Equiv.smul A e.toEquiv, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

Instances For

source
theorem LinearEquiv.isScalarTower {R : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring R] (A : Type u_4) [Semiring A] [Module R A] [AddCommMonoid α] [AddCommMonoid β] [Module A β] [Module R α] [Module R β] [IsScalarTower R A β] (e : α ≃ₗ[R] β) :
IsScalarTower R A α

The module instance from `AddEquiv.module` is compatible with the `R`-module structures, if the `AddEquiv` is induced by an `R`-module isomorphism.