Transfer algebraic structures across Equivs

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

theorem Equiv.noZeroSMulDivisors {α : Type u_2} {β : Type u_3} (e : α ≃ β) (R : Type u_4) [Zero R] [Zero β] [SMul R β] [NoZeroSMulDivisors R β] : have this := e.zero; have this_1 := Equiv.smul R e; NoZeroSMulDivisors R α

Transfer NoZeroSMulDivisors across an Equiv

@[reducible, inline]

abbrev Equiv.module (R : Type u_1) {α : Type u_2} {β : Type u_3} [Semiring R] (e : α ≃ β) [AddCommMonoid β] [Module R β] : Module R α

Transfer Module across an Equiv

def Equiv.linearEquiv (R : Type u_1) {α : Type u_2} {β : Type u_3} [Semiring R] (e : α ≃ β) [AddCommMonoid β] [Module R β] : α ≃ₗ[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.

theorem Equiv.moduleIsTorsionFree (R : Type u_1) {α : Type u_2} {β : Type u_3} [Semiring R] (e : α ≃ β) [AddCommMonoid β] [Module R β] [Module.IsTorsionFree R β] : let this := e.addCommMonoid; have this_1 := Equiv.module R e; Module.IsTorsionFree R α

Transfer Module.IsTorsionFree across an Equiv

@[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.

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.

def AddEquiv.linearEquiv {α : Type u_2} {β : Type u_3} (A : Type u_4) [Semiring A] [AddCommMonoid α] [AddCommMonoid β] [Module A β] (e : α ≃+ β) : α ≃ₗ[A] β

When α is equipped with the A-module structure transferred via e : α ≃+ β, this isomorphism is A-linear.

@[simp]

theorem AddEquiv.linearEquiv_apply {α : Type u_2} {β : Type u_3} (A : Type u_4) [Semiring A] [AddCommMonoid α] [AddCommMonoid β] [Module A β] (e : α ≃+ β) (a✝ : α) : (linearEquiv A e) a✝ = e.toFun a✝

@[simp]

theorem AddEquiv.linearEquiv_symm_apply {α : Type u_2} {β : Type u_3} (A : Type u_4) [Semiring A] [AddCommMonoid α] [AddCommMonoid β] [Module A β] (e : α ≃+ β) (a✝ : β) : (linearEquiv A e).symm a✝ = e.invFun a✝