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