Theorems · Definition · ring theory

TrivSqZeroExt.lift

{S : Type u_1} →
  {R : Type u} →
    {M : Type v} →
      [inst : CommSemiring S] →
        [inst_1 : Semiring R] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra S R] →
              [inst_4 : Module S M] →
                [inst_5 : Module R M] →
                  [inst_6 : Module Rᵐᵒᵖ M] →
                    [inst_7 : SMulCommClass R Rᵐᵒᵖ M] →
                      [inst_8 : IsScalarTower S R M] →
                        [inst_9 : IsScalarTower S Rᵐᵒᵖ M] →
                          {A : Type u_2} →
                            [inst_10 : Semiring A] →
                              [inst_11 : Algebra S A] →
                                (f : R →ₐ[S] A) →
                                  (g : M →ₗ[S] A) →
                                    (∀ (x y : M), g x * g y = 0) →
                                      (∀ (r : R) (x : M), g (r • x) = f r * g x) →
                                        (∀ (r : R) (x : M), g (MulOpposite.op r • x) = g x * f r) →
                                          TrivSqZeroExt R M →ₐ[S] A

Assemble an algebra morphism TrivSqZeroExt R M →ₐ[S] A from separate morphisms on R and M. Namely, we require that for an algebra morphism f : R →ₐ[S] A and a linear map g : M →ₗ[S] A, we have: * g x * g y = 0: the elements of M continue to square to zero. * g (r •> x) = f r * g x and g (x <• r) = g x * f r: scalar multiplication on the left and right is sent to left- and right- multiplication by the image under f. See TrivSqZeroExt.liftEquiv for this as an equiv; namely that any such algebra morphism can be factored in this way. When R is commutative, this can be invoked with f = Algebra.ofId R A, which satisfies hfg and hgf. This version is captured as an equiv by TrivSqZeroExt.liftEquivOfComm.

Defined in

Mathlib.Algebra.TrivSqZeroExt.Basic

Cited by

10 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAddCommMonoidAlgebraModuleModuleModuleSMulCommClassIsScalarTowerIsScalarTowerSemiringAlgebra