Documentation

Mathlib.Algebra.TrivSqZeroExt

Trivial Square-Zero Extension #

Given a ring R together with an (R, R)-bimodule M, the trivial square-zero extension of M over R is defined to be the R-algebra R ⊕ M with multiplication given by (r₁ + m₁) * (r₂ + m₂) = r₁ r₂ + r₁ m₂ + m₁ r₂.

It is a square-zero extension because M^2 = 0.

Note that expressing this requires bimodules; we write these in general for a not-necessarily-commutative R as:

variable {R M : Type*} [Semiring R] [AddCommMonoid M]
variable [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M]

If we instead work with a commutative R' acting symmetrically on M, we write

variable {R' M : Type*} [CommSemiring R'] [AddCommMonoid M]
variable [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M]

noting that in this context IsCentralScalar R' M implies SMulCommClass R' R'ᵐᵒᵖ M.

Many of the later results in this file are only stated for the commutative R' for simplicity.

Main definitions #

def TrivSqZeroExt (R : Type u) (M : Type v) :
Type (max u v)

"Trivial Square-Zero Extension".

Given a module M over a ring R, the trivial square-zero extension of M over R is defined to be the R-algebra R × M with multiplication given by (r₁ + m₁) * (r₂ + m₂) = r₁ r₂ + r₁ m₂ + r₂ m₁.

It is a square-zero extension because M^2 = 0.

Equations
Instances For
    def TrivSqZeroExt.inl {R : Type u} {M : Type v} [Zero M] (r : R) :

    The canonical inclusion R → TrivSqZeroExt R M.

    Equations
    Instances For
      def TrivSqZeroExt.inr {R : Type u} {M : Type v} [Zero R] (m : M) :

      The canonical inclusion M → TrivSqZeroExt R M.

      Equations
      Instances For
        def TrivSqZeroExt.fst {R : Type u} {M : Type v} (x : TrivSqZeroExt R M) :
        R

        The canonical projection TrivSqZeroExt R M → R.

        Equations
        Instances For
          def TrivSqZeroExt.snd {R : Type u} {M : Type v} (x : TrivSqZeroExt R M) :
          M

          The canonical projection TrivSqZeroExt R M → M.

          Equations
          Instances For
            @[simp]
            theorem TrivSqZeroExt.fst_mk {R : Type u} {M : Type v} (r : R) (m : M) :
            @[simp]
            theorem TrivSqZeroExt.snd_mk {R : Type u} {M : Type v} (r : R) (m : M) :
            @[simp]
            theorem TrivSqZeroExt.fst_inl {R : Type u} (M : Type v) [Zero M] (r : R) :
            @[simp]
            theorem TrivSqZeroExt.snd_inl {R : Type u} (M : Type v) [Zero M] (r : R) :
            @[simp]
            theorem TrivSqZeroExt.fst_comp_inl {R : Type u} (M : Type v) [Zero M] :
            TrivSqZeroExt.fst TrivSqZeroExt.inl = id
            @[simp]
            theorem TrivSqZeroExt.snd_comp_inl {R : Type u} (M : Type v) [Zero M] :
            TrivSqZeroExt.snd TrivSqZeroExt.inl = 0
            @[simp]
            theorem TrivSqZeroExt.fst_inr (R : Type u) {M : Type v} [Zero R] (m : M) :
            @[simp]
            theorem TrivSqZeroExt.snd_inr (R : Type u) {M : Type v} [Zero R] (m : M) :
            @[simp]
            theorem TrivSqZeroExt.fst_comp_inr (R : Type u) {M : Type v} [Zero R] :
            TrivSqZeroExt.fst TrivSqZeroExt.inr = 0
            @[simp]
            theorem TrivSqZeroExt.snd_comp_inr (R : Type u) {M : Type v} [Zero R] :
            TrivSqZeroExt.snd TrivSqZeroExt.inr = id
            theorem TrivSqZeroExt.inl_injective {R : Type u} {M : Type v} [Zero M] :
            Function.Injective TrivSqZeroExt.inl
            theorem TrivSqZeroExt.inr_injective {R : Type u} {M : Type v} [Zero R] :
            Function.Injective TrivSqZeroExt.inr

            Structures inherited from Prod #

            Additive operators and scalar multiplication operate elementwise.

            Equations
            • TrivSqZeroExt.inhabited = instInhabitedProd
            instance TrivSqZeroExt.zero {R : Type u} {M : Type v} [Zero R] [Zero M] :
            Equations
            • TrivSqZeroExt.zero = Prod.instZero
            instance TrivSqZeroExt.add {R : Type u} {M : Type v} [Add R] [Add M] :
            Equations
            • TrivSqZeroExt.add = Prod.instAdd
            instance TrivSqZeroExt.sub {R : Type u} {M : Type v} [Sub R] [Sub M] :
            Equations
            • TrivSqZeroExt.sub = Prod.instSub
            instance TrivSqZeroExt.neg {R : Type u} {M : Type v} [Neg R] [Neg M] :
            Equations
            • TrivSqZeroExt.neg = Prod.instNeg
            Equations
            • TrivSqZeroExt.addSemigroup = Prod.instAddSemigroup
            Equations
            • TrivSqZeroExt.addZeroClass = Prod.instAddZeroClass
            Equations
            • TrivSqZeroExt.addMonoid = Prod.instAddMonoid
            instance TrivSqZeroExt.addGroup {R : Type u} {M : Type v} [AddGroup R] [AddGroup M] :
            Equations
            • TrivSqZeroExt.addGroup = Prod.instAddGroup
            Equations
            • TrivSqZeroExt.addCommSemigroup = Prod.instAddCommSemigroup
            Equations
            • TrivSqZeroExt.addCommMonoid = Prod.instAddCommMonoid
            Equations
            • TrivSqZeroExt.addCommGroup = Prod.instAddCommGroup
            instance TrivSqZeroExt.smul {S : Type u_2} {R : Type u} {M : Type v} [SMul S R] [SMul S M] :
            Equations
            • TrivSqZeroExt.smul = Prod.smul
            instance TrivSqZeroExt.isScalarTower {T : Type u_1} {S : Type u_2} {R : Type u} {M : Type v} [SMul T R] [SMul T M] [SMul S R] [SMul S M] [SMul T S] [IsScalarTower T S R] [IsScalarTower T S M] :
            Equations
            • =
            instance TrivSqZeroExt.smulCommClass {T : Type u_1} {S : Type u_2} {R : Type u} {M : Type v} [SMul T R] [SMul T M] [SMul S R] [SMul S M] [SMulCommClass T S R] [SMulCommClass T S M] :
            Equations
            • =
            instance TrivSqZeroExt.isCentralScalar {S : Type u_2} {R : Type u} {M : Type v} [SMul S R] [SMul S M] [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [IsCentralScalar S R] [IsCentralScalar S M] :
            Equations
            • =
            instance TrivSqZeroExt.mulAction {S : Type u_2} {R : Type u} {M : Type v} [Monoid S] [MulAction S R] [MulAction S M] :
            Equations
            • TrivSqZeroExt.mulAction = Prod.mulAction
            Equations
            • TrivSqZeroExt.distribMulAction = Prod.distribMulAction
            instance TrivSqZeroExt.module {S : Type u_2} {R : Type u} {M : Type v} [Semiring S] [AddCommMonoid R] [AddCommMonoid M] [Module S R] [Module S M] :
            Equations
            • TrivSqZeroExt.module = Prod.instModule
            @[simp]
            theorem TrivSqZeroExt.fst_zero {R : Type u} {M : Type v} [Zero R] [Zero M] :
            @[simp]
            theorem TrivSqZeroExt.snd_zero {R : Type u} {M : Type v} [Zero R] [Zero M] :
            @[simp]
            theorem TrivSqZeroExt.fst_add {R : Type u} {M : Type v} [Add R] [Add M] (x₁ : TrivSqZeroExt R M) (x₂ : TrivSqZeroExt R M) :
            @[simp]
            theorem TrivSqZeroExt.snd_add {R : Type u} {M : Type v} [Add R] [Add M] (x₁ : TrivSqZeroExt R M) (x₂ : TrivSqZeroExt R M) :
            @[simp]
            theorem TrivSqZeroExt.fst_neg {R : Type u} {M : Type v} [Neg R] [Neg M] (x : TrivSqZeroExt R M) :
            @[simp]
            theorem TrivSqZeroExt.snd_neg {R : Type u} {M : Type v} [Neg R] [Neg M] (x : TrivSqZeroExt R M) :
            @[simp]
            theorem TrivSqZeroExt.fst_sub {R : Type u} {M : Type v} [Sub R] [Sub M] (x₁ : TrivSqZeroExt R M) (x₂ : TrivSqZeroExt R M) :
            @[simp]
            theorem TrivSqZeroExt.snd_sub {R : Type u} {M : Type v} [Sub R] [Sub M] (x₁ : TrivSqZeroExt R M) (x₂ : TrivSqZeroExt R M) :
            @[simp]
            theorem TrivSqZeroExt.fst_smul {S : Type u_2} {R : Type u} {M : Type v} [SMul S R] [SMul S M] (s : S) (x : TrivSqZeroExt R M) :
            @[simp]
            theorem TrivSqZeroExt.snd_smul {S : Type u_2} {R : Type u} {M : Type v} [SMul S R] [SMul S M] (s : S) (x : TrivSqZeroExt R M) :
            theorem TrivSqZeroExt.fst_sum {R : Type u} {M : Type v} {ι : Type u_3} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ιTrivSqZeroExt R M) :
            TrivSqZeroExt.fst (Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => TrivSqZeroExt.fst (f i)
            theorem TrivSqZeroExt.snd_sum {R : Type u} {M : Type v} {ι : Type u_3} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ιTrivSqZeroExt R M) :
            TrivSqZeroExt.snd (Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => TrivSqZeroExt.snd (f i)
            @[simp]
            theorem TrivSqZeroExt.inl_zero {R : Type u} (M : Type v) [Zero R] [Zero M] :
            @[simp]
            theorem TrivSqZeroExt.inl_add {R : Type u} (M : Type v) [Add R] [AddZeroClass M] (r₁ : R) (r₂ : R) :
            @[simp]
            @[simp]
            theorem TrivSqZeroExt.inl_sub {R : Type u} (M : Type v) [Sub R] [SubNegZeroMonoid M] (r₁ : R) (r₂ : R) :
            @[simp]
            theorem TrivSqZeroExt.inl_smul {S : Type u_2} {R : Type u} (M : Type v) [Monoid S] [AddMonoid M] [SMul S R] [DistribMulAction S M] (s : S) (r : R) :
            theorem TrivSqZeroExt.inl_sum {R : Type u} (M : Type v) {ι : Type u_3} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ιR) :
            TrivSqZeroExt.inl (Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => TrivSqZeroExt.inl (f i)
            @[simp]
            theorem TrivSqZeroExt.inr_zero (R : Type u) {M : Type v} [Zero R] [Zero M] :
            @[simp]
            theorem TrivSqZeroExt.inr_add (R : Type u) {M : Type v} [AddZeroClass R] [AddZeroClass M] (m₁ : M) (m₂ : M) :
            @[simp]
            @[simp]
            theorem TrivSqZeroExt.inr_sub (R : Type u) {M : Type v} [SubNegZeroMonoid R] [Sub M] (m₁ : M) (m₂ : M) :
            @[simp]
            theorem TrivSqZeroExt.inr_smul {S : Type u_2} (R : Type u) {M : Type v} [Zero R] [Zero S] [SMulWithZero S R] [SMul S M] (r : S) (m : M) :
            theorem TrivSqZeroExt.inr_sum (R : Type u) {M : Type v} {ι : Type u_3} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ιM) :
            TrivSqZeroExt.inr (Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => TrivSqZeroExt.inr (f i)
            theorem TrivSqZeroExt.ind {R : Type u_3} {M : Type u_4} [AddZeroClass R] [AddZeroClass M] {P : TrivSqZeroExt R MProp} (h : ∀ (r : R) (m : M), P (TrivSqZeroExt.inl r + TrivSqZeroExt.inr m)) (x : TrivSqZeroExt R M) :
            P x

            To show a property hold on all TrivSqZeroExt R M it suffices to show it holds on terms of the form inl r + inr m.

            This can be used as induction x using TrivSqZeroExt.ind.

            theorem TrivSqZeroExt.linearMap_ext {S : Type u_2} {R : Type u} {M : Type v} {N : Type u_3} [Semiring S] [AddCommMonoid R] [AddCommMonoid M] [AddCommMonoid N] [Module S R] [Module S M] [Module S N] ⦃f : TrivSqZeroExt R M →ₗ[S] N ⦃g : TrivSqZeroExt R M →ₗ[S] N (hl : ∀ (r : R), f (TrivSqZeroExt.inl r) = g (TrivSqZeroExt.inl r)) (hr : ∀ (m : M), f (TrivSqZeroExt.inr m) = g (TrivSqZeroExt.inr m)) :
            f = g

            This cannot be marked @[ext] as it ends up being used instead of LinearMap.prod_ext when working with R × M.

            @[simp]

            The canonical R-linear inclusion M → TrivSqZeroExt R M.

            Equations
            Instances For

              The canonical R-linear projection TrivSqZeroExt R M → M.

              Equations
              Instances For

                Multiplicative structure #

                instance TrivSqZeroExt.one {R : Type u} {M : Type v} [One R] [Zero M] :
                Equations
                • TrivSqZeroExt.one = { one := (1, 0) }
                instance TrivSqZeroExt.mul {R : Type u} {M : Type v} [Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] :
                Equations
                @[simp]
                theorem TrivSqZeroExt.fst_one {R : Type u} {M : Type v} [One R] [Zero M] :
                @[simp]
                theorem TrivSqZeroExt.snd_one {R : Type u} {M : Type v} [One R] [Zero M] :
                @[simp]
                theorem TrivSqZeroExt.fst_mul {R : Type u} {M : Type v} [Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] (x₁ : TrivSqZeroExt R M) (x₂ : TrivSqZeroExt R M) :
                @[simp]
                theorem TrivSqZeroExt.snd_mul {R : Type u} {M : Type v} [Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] (x₁ : TrivSqZeroExt R M) (x₂ : TrivSqZeroExt R M) :
                @[simp]
                theorem TrivSqZeroExt.inl_one {R : Type u} (M : Type v) [One R] [Zero M] :
                @[simp]
                theorem TrivSqZeroExt.inl_mul {R : Type u} (M : Type v) [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (r₁ : R) (r₂ : R) :
                theorem TrivSqZeroExt.inl_mul_inl {R : Type u} (M : Type v) [Monoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] (r₁ : R) (r₂ : R) :
                @[simp]
                theorem TrivSqZeroExt.inr_mul_inr (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] (m₁ : M) (m₂ : M) :
                theorem TrivSqZeroExt.inl_mul_eq_smul {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] (r : R) (x : TrivSqZeroExt R M) :
                Equations
                • TrivSqZeroExt.mulOneClass = let __src := TrivSqZeroExt.one; let __src_1 := TrivSqZeroExt.mul; MulOneClass.mk
                Equations
                • TrivSqZeroExt.addMonoidWithOne = let __src := TrivSqZeroExt.addMonoid; let __src_1 := TrivSqZeroExt.one; AddMonoidWithOne.mk
                @[simp]
                theorem TrivSqZeroExt.fst_nat_cast {R : Type u} {M : Type v} [AddMonoidWithOne R] [AddMonoid M] (n : ) :
                @[simp]
                @[simp]
                theorem TrivSqZeroExt.inl_nat_cast {R : Type u} {M : Type v} [AddMonoidWithOne R] [AddMonoid M] (n : ) :
                Equations
                • TrivSqZeroExt.addGroupWithOne = let __src := TrivSqZeroExt.addGroup; let __src_1 := TrivSqZeroExt.addMonoidWithOne; AddGroupWithOne.mk SubNegMonoid.zsmul
                @[simp]
                theorem TrivSqZeroExt.fst_int_cast {R : Type u} {M : Type v} [AddGroupWithOne R] [AddGroup M] (z : ) :
                @[simp]
                theorem TrivSqZeroExt.snd_int_cast {R : Type u} {M : Type v} [AddGroupWithOne R] [AddGroup M] (z : ) :
                @[simp]
                theorem TrivSqZeroExt.inl_int_cast {R : Type u} {M : Type v} [AddGroupWithOne R] [AddGroup M] (z : ) :
                Equations
                • TrivSqZeroExt.nonAssocSemiring = let __src := TrivSqZeroExt.addMonoidWithOne; let __src_1 := TrivSqZeroExt.mulOneClass; let __src_2 := TrivSqZeroExt.addCommMonoid; NonAssocSemiring.mk
                Equations
                • TrivSqZeroExt.nonAssocRing = let __src := TrivSqZeroExt.addGroupWithOne; let __src_1 := TrivSqZeroExt.nonAssocSemiring; NonAssocRing.mk

                In the general non-commutative case, the power operator is

                $$\begin{align} (r + m)^n &= r^n + r^{n-1}m + r^{n-2}mr + \cdots + rmr^{n-2} + mr^{n-1} \ & =r^n + \sum_{i = 0}^{n - 1} r^{(n - 1) - i} m r^{i} \end{align}$$

                In the commutative case this becomes the simpler $(r + m)^n = r^n + nr^{n-1}m$.

                Equations
                • One or more equations did not get rendered due to their size.
                @[simp]
                Equations
                • TrivSqZeroExt.monoid = let __src := TrivSqZeroExt.mulOneClass; Monoid.mk (fun (n : ) (x : TrivSqZeroExt R M) => x ^ n)
                Equations
                • TrivSqZeroExt.semiring = let __src := TrivSqZeroExt.monoid; let __src_1 := TrivSqZeroExt.nonAssocSemiring; Semiring.mk Monoid.npow

                The second element of a product $\prod_{i=0}^n (r_i + m_i)$ is a sum of terms of the form $r_0\cdots r_{i-1}m_ir_{i+1}\cdots r_n$.

                instance TrivSqZeroExt.ring {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] :
                Equations
                • TrivSqZeroExt.ring = let __src := TrivSqZeroExt.semiring; let __src_1 := TrivSqZeroExt.nonAssocRing; Ring.mk SubNegMonoid.zsmul
                Equations
                • TrivSqZeroExt.commMonoid = let __src := TrivSqZeroExt.monoid; CommMonoid.mk
                Equations
                • TrivSqZeroExt.commSemiring = let __src := TrivSqZeroExt.commMonoid; let __src_1 := TrivSqZeroExt.nonAssocSemiring; CommSemiring.mk
                Equations
                • TrivSqZeroExt.commRing = let __src := TrivSqZeroExt.nonAssocRing; let __src_1 := TrivSqZeroExt.commSemiring; CommRing.mk
                @[simp]

                The canonical inclusion of rings R → TrivSqZeroExt R M.

                Equations
                • TrivSqZeroExt.inlHom R M = { toMonoidHom := { toOneHom := { toFun := TrivSqZeroExt.inl, map_one' := }, map_mul' := }, map_zero' := , map_add' := }
                Instances For
                  instance TrivSqZeroExt.algebra' (S : Type u_1) (R : Type u) (M : Type v) [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] :
                  Equations
                  theorem TrivSqZeroExt.algebraMap_eq_inl (R' : Type u) (M : Type v) [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] :
                  (algebraMap R' (TrivSqZeroExt R' M)) = TrivSqZeroExt.inl

                  The canonical S-algebra projection TrivSqZeroExt R M → R.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    The canonical S-algebra inclusion R → TrivSqZeroExt R M.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      theorem TrivSqZeroExt.algHom_ext {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {A : Type u_2} [Semiring A] [Algebra R' A] ⦃f : TrivSqZeroExt R' M →ₐ[R'] A ⦃g : TrivSqZeroExt R' M →ₐ[R'] A (h : ∀ (m : M), f (TrivSqZeroExt.inr m) = g (TrivSqZeroExt.inr m)) :
                      f = g
                      theorem TrivSqZeroExt.algHom_ext' {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] ⦃f : TrivSqZeroExt R M →ₐ[S] A ⦃g : TrivSqZeroExt R M →ₐ[S] A (hinl : AlgHom.comp f (TrivSqZeroExt.inlAlgHom S R M) = AlgHom.comp g (TrivSqZeroExt.inlAlgHom S R M)) (hinr : AlgHom.toLinearMap f ∘ₗ S (TrivSqZeroExt.inrHom R M) = AlgHom.toLinearMap g ∘ₗ S (TrivSqZeroExt.inrHom R M)) :
                      f = g
                      def TrivSqZeroExt.lift {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ (x y : M), g x * g y = 0) (hfg : ∀ (r : R) (x : M), g (r x) = f r * g x) (hgf : ∀ (r : R) (x : M), g (MulOpposite.op r x) = g x * f r) :

                      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.

                      Equations
                      Instances For
                        theorem TrivSqZeroExt.lift_def {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ (x y : M), g x * g y = 0) (hfg : ∀ (r : R) (x : M), g (r x) = f r * g x) (hgf : ∀ (r : R) (x : M), g (MulOpposite.op r x) = g x * f r) (x : TrivSqZeroExt R M) :
                        @[simp]
                        theorem TrivSqZeroExt.lift_apply_inl {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ (x y : M), g x * g y = 0) (hfg : ∀ (r : R) (x : M), g (r x) = f r * g x) (hgf : ∀ (r : R) (x : M), g (MulOpposite.op r x) = g x * f r) (r : R) :
                        (TrivSqZeroExt.lift f g hg hfg hgf) (TrivSqZeroExt.inl r) = f r
                        @[simp]
                        theorem TrivSqZeroExt.lift_apply_inr {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ (x y : M), g x * g y = 0) (hfg : ∀ (r : R) (x : M), g (r x) = f r * g x) (hgf : ∀ (r : R) (x : M), g (MulOpposite.op r x) = g x * f r) (m : M) :
                        (TrivSqZeroExt.lift f g hg hfg hgf) (TrivSqZeroExt.inr m) = g m
                        @[simp]
                        theorem TrivSqZeroExt.lift_comp_inlHom {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ (x y : M), g x * g y = 0) (hfg : ∀ (r : R) (x : M), g (r x) = f r * g x) (hgf : ∀ (r : R) (x : M), g (MulOpposite.op r x) = g x * f r) :
                        @[simp]
                        theorem TrivSqZeroExt.lift_comp_inrHom {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ (x y : M), g x * g y = 0) (hfg : ∀ (r : R) (x : M), g (r x) = f r * g x) (hgf : ∀ (r : R) (x : M), g (MulOpposite.op r x) = g x * f r) :
                        AlgHom.toLinearMap (TrivSqZeroExt.lift f g hg hfg hgf) ∘ₗ S (TrivSqZeroExt.inrHom R M) = g
                        @[simp]

                        When applied to inr and inl themselves, lift is the identity.

                        @[simp]
                        theorem TrivSqZeroExt.liftEquiv_symm_apply_coe {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] (F : TrivSqZeroExt R M →ₐ[S] A) :
                        (TrivSqZeroExt.liftEquiv.symm F) = (AlgHom.comp F (TrivSqZeroExt.inlAlgHom S R M), LinearMap.comp (AlgHom.toLinearMap F) (S (TrivSqZeroExt.inrHom R M)))
                        @[simp]
                        theorem TrivSqZeroExt.liftEquiv_apply {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] (fg : { fg : (R →ₐ[S] A) × (M →ₗ[S] A) // (∀ (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.liftEquiv fg = TrivSqZeroExt.lift (fg).1 (fg).2
                        def TrivSqZeroExt.liftEquiv {S : Type u_1} {R : Type u} {M : Type v} [CommSemiring S] [Semiring R] [AddCommMonoid M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2} [Semiring A] [Algebra S A] :
                        { fg : (R →ₐ[S] A) × (M →ₗ[S] A) // (∀ (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.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem TrivSqZeroExt.liftEquivOfComm_symm_apply_coe {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {A : Type u_2} [Semiring A] [Algebra R' A] :
                          ∀ (a : TrivSqZeroExt R' M →ₐ[R'] A), (TrivSqZeroExt.liftEquivOfComm.symm a) = LinearMap.comp (AlgHom.toLinearMap a) (R' (TrivSqZeroExt.inrHom R' M))
                          @[simp]
                          theorem TrivSqZeroExt.liftEquivOfComm_apply {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {A : Type u_2} [Semiring A] [Algebra R' A] :
                          ∀ (a : { f : M →ₗ[R'] A // ∀ (x y : M), f x * f y = 0 }), TrivSqZeroExt.liftEquivOfComm a = TrivSqZeroExt.lift (Algebra.ofId R' A) a
                          def TrivSqZeroExt.liftEquivOfComm {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {A : Type u_2} [Semiring A] [Algebra R' A] :
                          { f : M →ₗ[R'] A // ∀ (x y : M), f x * f y = 0 } (TrivSqZeroExt R' M →ₐ[R'] A)

                          A simplified version of TrivSqZeroExt.liftEquiv for the commutative case.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def TrivSqZeroExt.map {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {N : Type u_3} [AddCommMonoid N] [Module R' N] [Module R'ᵐᵒᵖ N] [IsCentralScalar R' N] (f : M →ₗ[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.

                            Equations
                            Instances For
                              @[simp]
                              theorem TrivSqZeroExt.map_inl {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {N : Type u_3} [AddCommMonoid N] [Module R' N] [Module R'ᵐᵒᵖ N] [IsCentralScalar R' N] (f : M →ₗ[R'] N) (r : R') :
                              @[simp]
                              theorem TrivSqZeroExt.map_inr {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {N : Type u_3} [AddCommMonoid N] [Module R' N] [Module R'ᵐᵒᵖ N] [IsCentralScalar R' N] (f : M →ₗ[R'] N) (x : M) :
                              @[simp]
                              @[simp]
                              theorem TrivSqZeroExt.snd_map {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {N : Type u_3} [AddCommMonoid N] [Module R' N] [Module R'ᵐᵒᵖ N] [IsCentralScalar R' N] (f : M →ₗ[R'] N) (x : TrivSqZeroExt R' M) :
                              @[simp]
                              theorem TrivSqZeroExt.map_id {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] :
                              theorem TrivSqZeroExt.map_comp_map {R' : Type u} {M : Type v} [CommSemiring R'] [AddCommMonoid M] [Module R' M] [Module R'ᵐᵒᵖ M] [IsCentralScalar R' M] {N : Type u_3} {P : Type u_4} [AddCommMonoid N] [Module R' N] [Module R'ᵐᵒᵖ N] [IsCentralScalar R' N] [AddCommMonoid P] [Module R' P] [Module R'ᵐᵒᵖ P] [IsCentralScalar R' P] (f : M →ₗ[R'] N) (g : N →ₗ[R'] P) :