Theorems · Definition · ring theory

TrivSqZeroExt.liftEquiv

{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] →
                                { fg //
                                    (∀ (x y : M), fg.2 x * fg.2 y = 0) ∧
                                      (∀ (r : R) (x : M), fg.2 (r • x) = fg.1 r * fg.2 x) ∧
                                        ∀ (r : R) (x : M), fg.2 (MulOpposite.op r • x) = fg.2 x * fg.1 r } ≃
                                  (TrivSqZeroExt R M →ₐ[S] A)

A universal property of the trivial square-zero extension, providing a unique TrivSqZeroExt R M →ₐ[R] A for every pair of maps f : R →ₐ[S] A and g : M →ₗ[S] A, where the range of g has no non-zero products, and scaling the input to g on the left or right amounts to a corresponding multiplication by f in the output. This isomorphism is named to match the very similar Complex.lift.

Defined in

Mathlib.Algebra.TrivSqZeroExt.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAddCommMonoidAlgebraModuleModuleModuleSMulCommClassIsScalarTowerIsScalarTowerSemiringAlgebra