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

Equations

• Equiv.module R e = { toDistribMulAction := Equiv.distribMulAction R e, add_smul := ⋯, zero_smul := ⋯ }

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.

Equations

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

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.

Equations

• AddEquiv.module A e = { toSMul := Equiv.smul A e.toEquiv, mul_smul := ⋯, one_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.

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.

Equations

• AddEquiv.linearEquiv A e = { toFun := e.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ }

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

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