Theorems · Definition · ring theory

TrivSqZeroExt.map

{R' : Type u} →
  {M : Type v} →
    [inst : CommSemiring R'] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R' M] →
          [inst_3 : Module R'ᵐᵒᵖ M] →
            [inst_4 : IsCentralScalar R' M] →
              {N : Type u_3} →
                [inst_5 : AddCommMonoid N] →
                  [inst_6 : Module R' N] →
                    [inst_7 : Module R'ᵐᵒᵖ N] →
                      [inst_8 : IsCentralScalar R' N] → (M →ₗ[R'] N) → TrivSqZeroExt R' M →ₐ[R'] TrivSqZeroExt R' N

Functoriality of TrivSqZeroExt when the ring is commutative: a linear map f : M →ₗ[R'] N induces a morphism of R'-algebras from TrivSqZeroExt R' M to TrivSqZeroExt R' N. Note that we cannot neatly state the non-commutative case, as we do not have morphisms of bimodules.

Defined in

Mathlib.Algebra.TrivSqZeroExt.Basic

Cited by

12 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleModuleIsCentralScalarAddCommMonoidModuleModuleIsCentralScalar