Theorems · Definition · commutative algebra

Algebra.lsmul

(R : Type u) →
  {A : Type w} →
    (B : Type u₁) →
      (M : Type v₁) →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] →
                  [inst_5 : AddCommMonoid M] →
                    [inst_6 : Module R M] →
                      [inst_7 : Module A M] →
                        [inst_8 : Module B M] →
                          [IsScalarTower R A M] →
                            [inst_10 : IsScalarTower R B M] → [SMulCommClass A B M] → A →ₐ[R] Module.End B M

The R-algebra morphism A → End (M) corresponding to the representation of the algebra A on the B-module M. This is a stronger version of DistribSMul.toLinearMap, and could also have been called Algebra.toModuleEnd. The typeclasses correspond to the situation where the types act on each other as `` R -→ B | ⟍ | | ⟍ | ↓ ↘ ↓ A -→ M ` where the diagram commutes, the action by R commutes with everything, and the action by A and B on M commute. Typically this is most useful with B = R as Algebra.lsmul R R A : A →ₐ[R] Module.End R M. However this can be used to get the fact that left-multiplication by A is right A-linear, and vice versa, as `lean example : A →ₐ[R] Module.End Aᵐᵒᵖ A := Algebra.lsmul R Aᵐᵒᵖ A example : Aᵐᵒᵖ →ₐ[R] Module.End A A := Algebra.lsmul R A A ` respectively; though LinearMap.mulLeft and LinearMap.mulRight` can also be used here.

Defined in

Mathlib.Algebra.Algebra.Tower

Cited by

24 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringSemiringSemiringAlgebraAlgebraAddCommMonoidModuleModuleModuleIsScalarTowerIsScalarTowerSMulCommClass