Transfer algebraic structures across Equivs

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

@[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 := ⋯ }

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 := ⋯ }

@[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 := ⋯ }

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.