Documentation

TauCeti.Algebra.Module.Opposite

Modules over opposite algebras #

For an R-algebra A, a module over Aᵐᵒᵖ is a right A-module. Inverse right multiplication gives a homomorphism from Aˣ to its R-linear endomorphisms. This turns the right action into a left action of units, as used in balanced tensor constructions.

A left A-module is also a module over the double opposite Aᵐᵒᵖᵐᵒᵖ, by TauCeti.opOpModule. This is the form in which results about right modules, applied with Aᵐᵒᵖ in place of A, reach left A-modules. It is not a global instance, and TauCeti.opOpSemilinearEquiv transports module properties along the identity map.

source
def TauCeti.inverseRightAction (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] :
Aˣ →* Module.End R M

Units of an algebra act on a right module by inverse right multiplication.

Instances For
    source
    @[simp]
    theorem TauCeti.inverseRightAction_apply (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] (d : Aˣ) (m : M) :
    ((inverseRightAction R A M) d) m = MulOpposite.op ↑d⁻¹ • m

    The left action of a unit is right multiplication by its inverse.

    source
    @[reducible, inline]
    abbrev TauCeti.opOpModule (A : Type u_4) (N : Type u_5) [Semiring A] [AddCommMonoid N] [Module A N] :
    Module Aᵐᵒᵖᵐᵒᵖ N

    A left A-module, seen as a module over the double opposite Aᵐᵒᵖᵐᵒᵖ.

    Instances For
      source
      theorem TauCeti.isScalarTower_opOpModule {R : Type u_4} {A : Type u_5} {N : Type u_6} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid N] [Module R N] [Module A N] [IsScalarTower R A N] :
      IsScalarTower R Aᵐᵒᵖᵐᵒᵖ N

      The action of Aᵐᵒᵖᵐᵒᵖ on a left A-module is compatible with the action of the base.

      source
      def TauCeti.opOpSemilinearEquiv {A : Type u_4} {N : Type u_5} [Semiring A] [AddCommMonoid N] [Module A N] :
      N ≃ₛₗ[↑(RingEquiv.opOp A)] N

      A left A-module is semilinearly identified with itself over the double opposite Aᵐᵒᵖᵐᵒᵖ.

      Instances For
        source
        @[simp]
        theorem TauCeti.opOpSemilinearEquiv_apply {A : Type u_4} {N : Type u_5} [Semiring A] [AddCommMonoid N] [Module A N] (x : N) :
        opOpSemilinearEquiv x = x
        source
        @[simp]
        theorem TauCeti.opOpSemilinearEquiv_symm_apply {A : Type u_4} {N : Type u_5} [Semiring A] [AddCommMonoid N] [Module A N] (x : N) :
        opOpSemilinearEquiv.symm x = x