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