# 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 #

• TrivSqZeroExt.inl, TrivSqZeroExt.inr: the canonical inclusions into TrivSqZeroExt R M.
• TrivSqZeroExt.fst, TrivSqZeroExt.snd: the canonical projections from TrivSqZeroExt R M.
• triv_sq_zero_ext.algebra: the associated R-algebra structure.
• TrivSqZeroExt.lift: the universal property of the trivial square-zero extension; algebra morphisms TrivSqZeroExt R M →ₐ[S] A are uniquely defined by an algebra morphism f : R →ₐ[S] A on R and a linear map g : M →ₗ[S] A on M such that:
• 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: left and right actions are preserved by g.
• TrivSqZeroExt.lift: the universal property of the trivial square-zero extension; algebra morphisms TrivSqZeroExt R M →ₐ[R] A are uniquely defined by linear maps M →ₗ[R] A for which the product of any two elements in the range is zero.
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
• = (r, 0)
Instances For
def TrivSqZeroExt.inr {R : Type u} {M : Type v} [Zero R] (m : M) :

The canonical inclusion M → TrivSqZeroExt R M.

Equations
• = (0, m)
Instances For
def TrivSqZeroExt.fst {R : Type u} {M : Type v} (x : ) :
R

The canonical projection TrivSqZeroExt R M → R.

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

The canonical projection TrivSqZeroExt R M → M.

Equations
• x.snd = x.2
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) :
theorem TrivSqZeroExt.ext {R : Type u} {M : Type v} {x : } {y : } (h1 : x.fst = y.fst) (h2 : x.snd = y.snd) :
x = y
@[simp]
theorem TrivSqZeroExt.fst_inl {R : Type u} (M : Type v) [Zero M] (r : R) :
.fst = r
@[simp]
theorem TrivSqZeroExt.snd_inl {R : Type u} (M : Type v) [Zero M] (r : R) :
.snd = 0
@[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) :
.fst = 0
@[simp]
theorem TrivSqZeroExt.snd_inr (R : Type u) {M : Type v} [Zero R] (m : M) :
.snd = 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.

instance TrivSqZeroExt.inhabited {R : Type u} {M : Type v} [] [] :
Equations
• TrivSqZeroExt.inhabited = instInhabitedProd
instance TrivSqZeroExt.zero {R : Type u} {M : Type v} [Zero R] [Zero M] :
Zero ()
Equations
• TrivSqZeroExt.zero = Prod.instZero
instance TrivSqZeroExt.add {R : Type u} {M : Type v} [Add R] [Add M] :
Equations
instance TrivSqZeroExt.sub {R : Type u} {M : Type v} [Sub R] [Sub M] :
Sub ()
Equations
• TrivSqZeroExt.sub = Prod.instSub
instance TrivSqZeroExt.neg {R : Type u} {M : Type v} [Neg R] [Neg M] :
Neg ()
Equations
• TrivSqZeroExt.neg = Prod.instNeg
instance TrivSqZeroExt.addSemigroup {R : Type u} {M : Type v} [] [] :
Equations
instance TrivSqZeroExt.addZeroClass {R : Type u} {M : Type v} [] [] :
Equations
instance TrivSqZeroExt.addMonoid {R : Type u} {M : Type v} [] [] :
Equations
instance TrivSqZeroExt.addGroup {R : Type u} {M : Type v} [] [] :
Equations
instance TrivSqZeroExt.addCommSemigroup {R : Type u} {M : Type v} [] [] :
Equations
instance TrivSqZeroExt.addCommMonoid {R : Type u} {M : Type v} [] [] :
Equations
instance TrivSqZeroExt.addCommGroup {R : Type u} {M : Type v} [] [] :
Equations
instance TrivSqZeroExt.smul {S : Type u_2} {R : Type u} {M : Type v} [SMul S R] [SMul S M] :
SMul S ()
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] [] [] :
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] [] [] :
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] [] [] :
Equations
• =
instance TrivSqZeroExt.mulAction {S : Type u_2} {R : Type u} {M : Type v} [] [] [] :
Equations
• TrivSqZeroExt.mulAction = Prod.mulAction
instance TrivSqZeroExt.distribMulAction {S : Type u_2} {R : Type u} {M : Type v} [] [] [] [] [] :
Equations
• TrivSqZeroExt.distribMulAction = Prod.distribMulAction
instance TrivSqZeroExt.module {S : Type u_2} {R : Type u} {M : Type v} [] [] [] [Module S R] [Module S M] :
Module S ()
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₁ : ) (x₂ : ) :
(x₁ + x₂).fst = x₁.fst + x₂.fst
@[simp]
theorem TrivSqZeroExt.snd_add {R : Type u} {M : Type v} [Add R] [Add M] (x₁ : ) (x₂ : ) :
(x₁ + x₂).snd = x₁.snd + x₂.snd
@[simp]
theorem TrivSqZeroExt.fst_neg {R : Type u} {M : Type v} [Neg R] [Neg M] (x : ) :
(-x).fst = -x.fst
@[simp]
theorem TrivSqZeroExt.snd_neg {R : Type u} {M : Type v} [Neg R] [Neg M] (x : ) :
(-x).snd = -x.snd
@[simp]
theorem TrivSqZeroExt.fst_sub {R : Type u} {M : Type v} [Sub R] [Sub M] (x₁ : ) (x₂ : ) :
(x₁ - x₂).fst = x₁.fst - x₂.fst
@[simp]
theorem TrivSqZeroExt.snd_sub {R : Type u} {M : Type v} [Sub R] [Sub M] (x₁ : ) (x₂ : ) :
(x₁ - x₂).snd = x₁.snd - x₂.snd
@[simp]
theorem TrivSqZeroExt.fst_smul {S : Type u_2} {R : Type u} {M : Type v} [SMul S R] [SMul S M] (s : S) (x : ) :
(s x).fst = s x.fst
@[simp]
theorem TrivSqZeroExt.snd_smul {S : Type u_2} {R : Type u} {M : Type v} [SMul S R] [SMul S M] (s : S) (x : ) :
(s x).snd = s x.snd
theorem TrivSqZeroExt.fst_sum {R : Type u} {M : Type v} {ι : Type u_3} [] [] (s : ) (f : ι) :
(is, f i).fst = is, (f i).fst
theorem TrivSqZeroExt.snd_sum {R : Type u} {M : Type v} {ι : Type u_3} [] [] (s : ) (f : ι) :
(is, f i).snd = is, (f i).snd
@[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] [] (r₁ : R) (r₂ : R) :
TrivSqZeroExt.inl (r₁ + r₂) =
@[simp]
theorem TrivSqZeroExt.inl_neg {R : Type u} (M : Type v) [Neg R] [] (r : R) :
@[simp]
theorem TrivSqZeroExt.inl_sub {R : Type u} (M : Type v) [Sub R] [] (r₁ : R) (r₂ : R) :
TrivSqZeroExt.inl (r₁ - r₂) =
@[simp]
theorem TrivSqZeroExt.inl_smul {S : Type u_2} {R : Type u} (M : Type v) [] [] [SMul S R] [] (s : S) (r : R) :
theorem TrivSqZeroExt.inl_sum {R : Type u} (M : Type v) {ι : Type u_3} [] [] (s : ) (f : ιR) :
TrivSqZeroExt.inl (is, f i) = is, 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} [] [] (m₁ : M) (m₂ : M) :
TrivSqZeroExt.inr (m₁ + m₂) =
@[simp]
theorem TrivSqZeroExt.inr_neg (R : Type u) {M : Type v} [] [Neg M] (m : M) :
@[simp]
theorem TrivSqZeroExt.inr_sub (R : Type u) {M : Type v} [] [Sub M] (m₁ : M) (m₂ : M) :
TrivSqZeroExt.inr (m₁ - m₂) =
@[simp]
theorem TrivSqZeroExt.inr_smul {S : Type u_2} (R : Type u) {M : Type v} [Zero R] [Zero S] [] [SMul S M] (r : S) (m : M) :
theorem TrivSqZeroExt.inr_sum (R : Type u) {M : Type v} {ι : Type u_3} [] [] (s : ) (f : ιM) :
TrivSqZeroExt.inr (is, f i) = is, TrivSqZeroExt.inr (f i)
theorem TrivSqZeroExt.inl_fst_add_inr_snd_eq {R : Type u} {M : Type v} [] [] (x : ) :
theorem TrivSqZeroExt.ind {R : Type u_3} {M : Type u_4} [] [] {P : Prop} (inl_add_inr : ∀ (r : R) (m : M), P ) (x : ) :
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.

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

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

@[simp]
theorem TrivSqZeroExt.inrHom_apply (R : Type u) (M : Type v) [] [] [Module R M] (m : M) :
() m =
def TrivSqZeroExt.inrHom (R : Type u) (M : Type v) [] [] [Module R M] :

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

Equations
• = let __src := ; { toFun := TrivSqZeroExt.inr, map_add' := , map_smul' := }
Instances For
@[simp]
theorem TrivSqZeroExt.sndHom_apply (R : Type u) (M : Type v) [] [] [Module R M] (x : ) :
() x = x.snd
def TrivSqZeroExt.sndHom (R : Type u) (M : Type v) [] [] [Module R M] :

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

Equations
• = let __src := ; { toFun := TrivSqZeroExt.snd, map_add' := , map_smul' := }
Instances For

### Multiplicative structure #

instance TrivSqZeroExt.one {R : Type u} {M : Type v} [One R] [Zero M] :
One ()
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] :
Mul ()
Equations
• TrivSqZeroExt.mul = { mul := fun (x y : ) => (x.1 * y.1, x.1 y.2 + x.2) }
@[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₁ : ) (x₂ : ) :
(x₁ * x₂).fst = x₁.fst * x₂.fst
@[simp]
theorem TrivSqZeroExt.snd_mul {R : Type u} {M : Type v} [Mul R] [Add M] [SMul R M] [SMul Rᵐᵒᵖ M] (x₁ : ) (x₂ : ) :
(x₁ * x₂).snd = x₁.fst x₂.snd + MulOpposite.op x₂.fst x₁.snd
@[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) [] [] [] [] (r₁ : R) (r₂ : R) :
TrivSqZeroExt.inl (r₁ * r₂) =
theorem TrivSqZeroExt.inl_mul_inl {R : Type u} (M : Type v) [] [] [] [] (r₁ : R) (r₂ : R) :
= TrivSqZeroExt.inl (r₁ * r₂)
@[simp]
theorem TrivSqZeroExt.inr_mul_inr (R : Type u) {M : Type v} [] [] [Module R M] [] (m₁ : M) (m₂ : M) :
= 0
theorem TrivSqZeroExt.inl_mul_inr {R : Type u} {M : Type v} [] [] [Module R M] [] (r : R) (m : M) :
theorem TrivSqZeroExt.inr_mul_inl {R : Type u} {M : Type v} [] [] [Module R M] [] (r : R) (m : M) :
theorem TrivSqZeroExt.inl_mul_eq_smul {R : Type u} {M : Type v} [] [] [Module R M] [] (r : R) (x : ) :
= r x
theorem TrivSqZeroExt.mul_inl_eq_op_smul {R : Type u} {M : Type v} [] [] [Module R M] [] (x : ) (r : R) :
=
instance TrivSqZeroExt.mulOneClass {R : Type u} {M : Type v} [] [] [] [] :
Equations
• TrivSqZeroExt.mulOneClass = let __src := TrivSqZeroExt.one; let __src_1 := TrivSqZeroExt.mul;
instance TrivSqZeroExt.addMonoidWithOne {R : Type u} {M : Type v} [] [] :
Equations
• TrivSqZeroExt.addMonoidWithOne = let __src := TrivSqZeroExt.addMonoid; let __src_1 := TrivSqZeroExt.one;
@[simp]
theorem TrivSqZeroExt.fst_natCast {R : Type u} {M : Type v} [] [] (n : ) :
(n).fst = n
@[deprecated TrivSqZeroExt.fst_natCast]
theorem TrivSqZeroExt.fst_nat_cast {R : Type u} {M : Type v} [] [] (n : ) :
(n).fst = n

Alias of TrivSqZeroExt.fst_natCast.

@[simp]
theorem TrivSqZeroExt.snd_natCast {R : Type u} {M : Type v} [] [] (n : ) :
(n).snd = 0
@[deprecated TrivSqZeroExt.snd_natCast]
theorem TrivSqZeroExt.snd_nat_cast {R : Type u} {M : Type v} [] [] (n : ) :
(n).snd = 0

Alias of TrivSqZeroExt.snd_natCast.

@[simp]
theorem TrivSqZeroExt.inl_natCast {R : Type u} {M : Type v} [] [] (n : ) :
= n
@[deprecated TrivSqZeroExt.inl_natCast]
theorem TrivSqZeroExt.inl_nat_cast {R : Type u} {M : Type v} [] [] (n : ) :
= n

Alias of TrivSqZeroExt.inl_natCast.

instance TrivSqZeroExt.addGroupWithOne {R : Type u} {M : Type v} [] [] :
Equations
@[simp]
theorem TrivSqZeroExt.fst_intCast {R : Type u} {M : Type v} [] [] (z : ) :
(z).fst = z
@[deprecated TrivSqZeroExt.fst_intCast]
theorem TrivSqZeroExt.fst_int_cast {R : Type u} {M : Type v} [] [] (z : ) :
(z).fst = z

Alias of TrivSqZeroExt.fst_intCast.

@[simp]
theorem TrivSqZeroExt.snd_intCast {R : Type u} {M : Type v} [] [] (z : ) :
(z).snd = 0
@[deprecated TrivSqZeroExt.snd_intCast]
theorem TrivSqZeroExt.snd_int_cast {R : Type u} {M : Type v} [] [] (z : ) :
(z).snd = 0

Alias of TrivSqZeroExt.snd_intCast.

@[simp]
theorem TrivSqZeroExt.inl_intCast {R : Type u} {M : Type v} [] [] (z : ) :
= z
@[deprecated TrivSqZeroExt.inl_intCast]
theorem TrivSqZeroExt.inl_int_cast {R : Type u} {M : Type v} [] [] (z : ) :
= z

Alias of TrivSqZeroExt.inl_intCast.

instance TrivSqZeroExt.nonAssocSemiring {R : Type u} {M : Type v} [] [] [Module R M] [] :
Equations
• TrivSqZeroExt.nonAssocSemiring = let __src := TrivSqZeroExt.addMonoidWithOne; let __src_1 := TrivSqZeroExt.mulOneClass; let __src_2 := TrivSqZeroExt.addCommMonoid;
instance TrivSqZeroExt.nonAssocRing {R : Type u} {M : Type v} [Ring R] [] [Module R M] [] :
Equations
• TrivSqZeroExt.nonAssocRing = let __src := TrivSqZeroExt.addGroupWithOne; let __src_1 := TrivSqZeroExt.nonAssocSemiring; NonAssocRing.mk
instance TrivSqZeroExt.instPowNatOfDistribMulActionMulOpposite {R : Type u} {M : Type v} [] [] [] [] :
Pow ()

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]
theorem TrivSqZeroExt.fst_pow {R : Type u} {M : Type v} [] [] [] [] (x : ) (n : ) :
(x ^ n).fst = x.fst ^ n
theorem TrivSqZeroExt.snd_pow_eq_sum {R : Type u} {M : Type v} [] [] [] [] (x : ) (n : ) :
(x ^ n).snd = (List.map (fun (i : ) => MulOpposite.op (x.fst ^ i) x.fst ^ (n.pred - i) x.snd) ()).sum
theorem TrivSqZeroExt.snd_pow_of_smul_comm {R : Type u} {M : Type v} [] [] [] [] [] (x : ) (n : ) (h : MulOpposite.op x.fst x.snd = x.fst x.snd) :
(x ^ n).snd = n x.fst ^ n.pred x.snd
theorem TrivSqZeroExt.snd_pow_of_smul_comm.aux {R : Type u} {M : Type v} [] [] [] [] [] (x : ) (h : MulOpposite.op x.fst x.snd = x.fst x.snd) (n : ) :
MulOpposite.op (x.fst ^ n) x.snd = x.fst ^ n x.snd
theorem TrivSqZeroExt.snd_pow_of_smul_comm' {R : Type u} {M : Type v} [] [] [] [] [] (x : ) (n : ) (h : MulOpposite.op x.fst x.snd = x.fst x.snd) :
(x ^ n).snd = n MulOpposite.op (x.fst ^ n.pred) x.snd
@[simp]
theorem TrivSqZeroExt.snd_pow {R : Type u} {M : Type v} [] [] [] [] [] (x : ) (n : ) :
(x ^ n).snd = n x.fst ^ n.pred x.snd
@[simp]
theorem TrivSqZeroExt.inl_pow {R : Type u} {M : Type v} [] [] [] [] (r : R) (n : ) :
instance TrivSqZeroExt.monoid {R : Type u} {M : Type v} [] [] [] [] [] :
Equations
• TrivSqZeroExt.monoid = let __src := TrivSqZeroExt.mulOneClass; Monoid.mk (fun (n : ) (x : ) => x ^ n)
theorem TrivSqZeroExt.fst_list_prod {R : Type u} {M : Type v} [] [] [] [] [] (l : List ()) :
l.prod.fst = (List.map TrivSqZeroExt.fst l).prod
instance TrivSqZeroExt.semiring {R : Type u} {M : Type v} [] [] [Module R M] [] [] :
Equations
• TrivSqZeroExt.semiring = let __src := TrivSqZeroExt.monoid; let __src_1 := TrivSqZeroExt.nonAssocSemiring; Semiring.mk Monoid.npow
theorem TrivSqZeroExt.snd_list_prod {R : Type u} {M : Type v} [] [] [Module R M] [] [] (l : List ()) :
l.prod.snd = (List.map (fun (x : × ) => MulOpposite.op (List.drop x.1.succ (List.map TrivSqZeroExt.fst l)).prod (List.take x.1 (List.map TrivSqZeroExt.fst l)).prod x.2.snd) l.enum).sum

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] [] [Module R M] [] [] :
Ring ()
Equations
• TrivSqZeroExt.ring = let __src := TrivSqZeroExt.semiring; let __src_1 := TrivSqZeroExt.nonAssocRing; Ring.mk SubNegMonoid.zsmul
instance TrivSqZeroExt.commMonoid {R : Type u} {M : Type v} [] [] [] [] [] :
Equations
• TrivSqZeroExt.commMonoid = let __src := TrivSqZeroExt.monoid;
instance TrivSqZeroExt.commSemiring {R : Type u} {M : Type v} [] [] [Module R M] [] [] :
Equations
• TrivSqZeroExt.commSemiring = let __src := TrivSqZeroExt.commMonoid; let __src_1 := TrivSqZeroExt.nonAssocSemiring;
instance TrivSqZeroExt.commRing {R : Type u} {M : Type v} [] [] [Module R M] [] [] :
Equations
• TrivSqZeroExt.commRing = let __src := TrivSqZeroExt.nonAssocRing; let __src_1 := TrivSqZeroExt.commSemiring;
@[simp]
theorem TrivSqZeroExt.inlHom_apply (R : Type u) (M : Type v) [] [] [Module R M] [] (r : R) :
() r =
def TrivSqZeroExt.inlHom (R : Type u) (M : Type v) [] [] [Module R M] [] :

The canonical inclusion of rings R → TrivSqZeroExt R M.

Equations
• = { toFun := TrivSqZeroExt.inl, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
instance TrivSqZeroExt.instInv {R : Type u} {M : Type v} [Neg M] [Inv R] [SMul Rᵐᵒᵖ M] [SMul R M] :
Inv ()

Inversion of the trivial-square-zero extension, sending $r + m$ to $r^{-1} - r^{-1}mr^{-1}$.

Equations
@[simp]
theorem TrivSqZeroExt.fst_inv {R : Type u} {M : Type v} [Neg M] [Inv R] [SMul Rᵐᵒᵖ M] [SMul R M] (x : ) :
x⁻¹.fst = x.fst⁻¹
@[simp]
theorem TrivSqZeroExt.snd_inv {R : Type u} {M : Type v} [Neg M] [Inv R] [SMul Rᵐᵒᵖ M] [SMul R M] (x : ) :
x⁻¹.snd = -(MulOpposite.op x.fst⁻¹ x.fst⁻¹ x.snd)
theorem TrivSqZeroExt.inv_inl {R : Type u} {M : Type v} [] [] [] [Module R M] (r : R) :
@[simp]
theorem TrivSqZeroExt.inv_inr {R : Type u} {M : Type v} [] [] [] [Module R M] (m : M) :
= 0
@[simp]
theorem TrivSqZeroExt.inv_zero {R : Type u} {M : Type v} [] [] [] [Module R M] :
0⁻¹ = 0
@[simp]
theorem TrivSqZeroExt.inv_one {R : Type u} {M : Type v} [] [] [] [Module R M] :
1⁻¹ = 1
theorem TrivSqZeroExt.mul_inv_cancel {R : Type u} {M : Type v} [] [] [] [Module R M] [] {x : } (hx : x.fst 0) :
x * x⁻¹ = 1
theorem TrivSqZeroExt.inv_mul_cancel {R : Type u} {M : Type v} [] [] [] [Module R M] {x : } (hx : x.fst 0) :
x⁻¹ * x = 1
theorem TrivSqZeroExt.mul_inv_rev {R : Type u} {M : Type v} [] [] [] [Module R M] [] (a : ) (b : ) :
(a * b)⁻¹ = b⁻¹ * a⁻¹
theorem TrivSqZeroExt.inv_inv {R : Type u} {M : Type v} [] [] [] [Module R M] [] {x : } (hx : x.fst 0) :
theorem TrivSqZeroExt.inv_neg {R : Type u} {M : Type v} [] [] [] [Module R M] {x : } :
instance TrivSqZeroExt.algebra' (S : Type u_1) (R : Type u) (M : Type v) [] [] [] [Algebra S R] [Module S M] [Module R M] [] [] [] [] :
Algebra S ()
Equations
instance TrivSqZeroExt.instAlgebra (R' : Type u) (M : Type v) [] [] [Module R' M] [Module R'ᵐᵒᵖ M] [] :
Algebra R' ()
Equations
theorem TrivSqZeroExt.algebraMap_eq_inl (R' : Type u) (M : Type v) [] [] [Module R' M] [Module R'ᵐᵒᵖ M] [] :
(algebraMap R' ()) = TrivSqZeroExt.inl
theorem TrivSqZeroExt.algebraMap_eq_inlHom (R' : Type u) (M : Type v) [] [] [Module R' M] [Module R'ᵐᵒᵖ M] [] :
algebraMap R' () =
theorem TrivSqZeroExt.algebraMap_eq_inl' (S : Type u_1) (R : Type u) (M : Type v) [] [] [] [Algebra S R] [Module S M] [Module R M] [] [] [] [] (s : S) :
@[simp]
theorem TrivSqZeroExt.fstHom_apply (S : Type u_1) (R : Type u) (M : Type v) [] [] [] [Algebra S R] [Module S M] [Module R M] [] [] [] [] (x : ) :
() x = x.fst
def TrivSqZeroExt.fstHom (S : Type u_1) (R : Type u) (M : Type v) [] [] [] [Algebra S R] [Module S M] [Module R M] [] [] [] [] :

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

Equations
• = { toFun := TrivSqZeroExt.fst, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem TrivSqZeroExt.inlAlgHom_apply (S : Type u_1) (R : Type u) (M : Type v) [] [] [] [Algebra S R] [Module S M] [Module R M] [] [] [] [] (r : R) :
() r =
def TrivSqZeroExt.inlAlgHom (S : Type u_1) (R : Type u) (M : Type v) [] [] [] [Algebra S R] [Module S M] [Module R M] [] [] [] [] :

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

Equations
• = { toFun := TrivSqZeroExt.inl, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
theorem TrivSqZeroExt.algHom_ext {R' : Type u} {M : Type v} [] [] [Module R' M] [Module R'ᵐᵒᵖ M] [] {A : Type u_2} [] [Algebra R' A] ⦃f : →ₐ[R'] A ⦃g : →ₐ[R'] A (h : ∀ (m : M), f = g ) :
f = g
theorem TrivSqZeroExt.algHom_ext' {S : Type u_1} {R : Type u} {M : Type v} [] [] [] [Algebra S R] [Module S M] [Module R M] [] [] [] [] {A : Type u_2} [] [Algebra S A] ⦃f : →ₐ[S] A ⦃g : →ₐ[S] A (hinl : f.comp () = g.comp ()) (hinr : f.toLinearMap ∘ₗ S () = g.toLinearMap ∘ₗ S ()) :
f = g
def TrivSqZeroExt.lift {S : Type u_1} {R : Type u} {M : Type v} [] [] [] [Algebra S R] [Module S M] [Module R M] [] [] [] [] {A : Type u_2} [] [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 () = 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} [] [] [] [Algebra S R] [Module S M] [Module R M] [] [] [] [] {A : Type u_2} [] [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 () = g x * f r) (x : ) :
(TrivSqZeroExt.lift f g hg hfg hgf) x = f x.fst + g x.snd
@[simp]
theorem TrivSqZeroExt.lift_apply_inl {S : Type u_1} {R : Type u} {M : Type v} [] [] [] [Algebra S R] [Module S M] [Module R M] [] [] [] [] {A : Type u_2} [] [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 () = g x * f r) (r : R) :
(TrivSqZeroExt.lift f g hg hfg hgf) = f r
@[simp]
theorem TrivSqZeroExt.lift_apply_inr {S : Type u_1} {R : Type u} {M : Type v} [] [] [] [Algebra S R] [Module S M] [Module R M] [] [] [] [] {A : Type u_2} [] [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 () = g x * f r) (m : M) :
(TrivSqZeroExt.lift f g hg hfg hgf) = g m
@[simp]
theorem TrivSqZeroExt.lift_comp_inlHom {S : Type u_1} {R : Type u} {M : Type v} [] [] [] [Algebra S R] [Module S M] [Module R M] [] [] [] [] {A : Type u_2} [] [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 () = g x * f r) :
(TrivSqZeroExt.lift f g hg hfg hgf).comp () = f
@[simp]
theorem TrivSqZeroExt.lift_comp_inrHom {S : Type u_1} {R : Type u} {M : Type v} [] [] [] [Algebra S R] [Module S M] [Module R M] [] [] [] [] {A : Type u_2} [] [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 () = g x * f r) :
(TrivSqZeroExt.lift f g hg hfg hgf).toLinearMap ∘ₗ S () = g
@[simp]
theorem TrivSqZeroExt.lift_inlAlgHom_inrHom {S : Type u_1} {R : Type u} {M : Type v} [] [] [] [Algebra S R] [Module S M] [Module R M] [] [] [] [] :
TrivSqZeroExt.lift () (S ()) = AlgHom.id S ()

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

@[simp]
theorem TrivSqZeroExt.liftEquiv_apply {S : Type u_1} {R : Type u} {M : Type v} [] [] [] [Algebra S R] [Module S M] [Module R M] [] [] [] [] {A : Type u_2} [] [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 () = fg.2 x * fg.1 r }) :
TrivSqZeroExt.liftEquiv fg = TrivSqZeroExt.lift (fg).1 (fg).2
@[simp]
theorem TrivSqZeroExt.liftEquiv_symm_apply_coe {S : Type u_1} {R : Type u} {M : Type v} [] [] [] [Algebra S R] [Module S M] [Module R M] [] [] [] [] {A : Type u_2} [] [Algebra S A] (F : →ₐ[S] A) :
(TrivSqZeroExt.liftEquiv.symm F) = (F.comp (), F.toLinearMap ∘ₗ S ())
def TrivSqZeroExt.liftEquiv {S : Type u_1} {R : Type u} {M : Type v} [] [] [] [Algebra S R] [Module S M] [Module R M] [] [] [] [] {A : Type u_2} [] [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 () = fg.2 x * fg.1 r } ( →ₐ[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_apply {R' : Type u} {M : Type v} [] [] [Module R' M] [Module R'ᵐᵒᵖ M] [] {A : Type u_2} [] [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
@[simp]
theorem TrivSqZeroExt.liftEquivOfComm_symm_apply_coe {R' : Type u} {M : Type v} [] [] [Module R' M] [Module R'ᵐᵒᵖ M] [] {A : Type u_2} [] [Algebra R' A] :
∀ (a : →ₐ[R'] A), (TrivSqZeroExt.liftEquivOfComm.symm a) = a.toLinearMap ∘ₗ R' ()
def TrivSqZeroExt.liftEquivOfComm {R' : Type u} {M : Type v} [] [] [Module R' M] [Module R'ᵐᵒᵖ M] [] {A : Type u_2} [] [Algebra R' A] :
{ f : M →ₗ[R'] A // ∀ (x y : M), f x * f y = 0 } ( →ₐ[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} [] [] [Module R' M] [Module R'ᵐᵒᵖ M] [] {N : Type u_3} [] [Module R' N] [Module 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
• = TrivSqZeroExt.liftEquivOfComm ∘ₗ f,
Instances For
@[simp]
theorem TrivSqZeroExt.map_inl {R' : Type u} {M : Type v} [] [] [Module R' M] [Module R'ᵐᵒᵖ M] [] {N : Type u_3} [] [Module R' N] [Module R'ᵐᵒᵖ N] [] (f : M →ₗ[R'] N) (r : R') :
@[simp]
theorem TrivSqZeroExt.map_inr {R' : Type u} {M : Type v} [] [] [Module R' M] [Module R'ᵐᵒᵖ M] [] {N : Type u_3} [] [Module R' N] [Module R'ᵐᵒᵖ N] [] (f : M →ₗ[R'] N) (x : M) :
@[simp]
theorem TrivSqZeroExt.fst_map {R' : Type u} {M : Type v} [] [] [Module R' M] [Module R'ᵐᵒᵖ M] [] {N : Type u_3} [] [Module R' N] [Module R'ᵐᵒᵖ N] [] (f : M →ₗ[R'] N) (x : ) :
( x).fst = x.fst
@[simp]
theorem TrivSqZeroExt.snd_map {R' : Type u} {M : Type v} [] [] [Module R' M] [Module R'ᵐᵒᵖ M] [] {N : Type u_3} [] [Module R' N] [Module R'ᵐᵒᵖ N] [] (f : M →ₗ[R'] N) (x : ) :
( x).snd = f x.snd
@[simp]
theorem TrivSqZeroExt.map_comp_inlAlgHom {R' : Type u} {M : Type v} [] [] [Module R' M] [Module R'ᵐᵒᵖ M] [] {N : Type u_3} [] [Module R' N] [Module R'ᵐᵒᵖ N] [] (f : M →ₗ[R'] N) :
.comp () =
@[simp]
theorem TrivSqZeroExt.map_comp_inrHom {R' : Type u} {M : Type v} [] [] [Module R' M] [Module R'ᵐᵒᵖ M] [] {N : Type u_3} [] [Module R' N] [Module R'ᵐᵒᵖ N] [] (f : M →ₗ[R'] N) :
.toLinearMap ∘ₗ = ∘ₗ f
@[simp]
theorem TrivSqZeroExt.fstHom_comp_map {R' : Type u} {M : Type v} [] [] [Module R' M] [Module R'ᵐᵒᵖ M] [] {N : Type u_3} [] [Module R' N] [Module R'ᵐᵒᵖ N] [] (f : M →ₗ[R'] N) :
@[simp]
theorem TrivSqZeroExt.sndHom_comp_map {R' : Type u} {M : Type v} [] [] [Module R' M] [Module R'ᵐᵒᵖ M] [] {N : Type u_3} [] [Module R' N] [Module R'ᵐᵒᵖ N] [] (f : M →ₗ[R'] N) :
∘ₗ .toLinearMap = f ∘ₗ
@[simp]
theorem TrivSqZeroExt.map_id {R' : Type u} {M : Type v} [] [] [Module R' M] [Module R'ᵐᵒᵖ M] [] :
TrivSqZeroExt.map LinearMap.id = AlgHom.id R' ()
theorem TrivSqZeroExt.map_comp_map {R' : Type u} {M : Type v} [] [] [Module R' M] [Module R'ᵐᵒᵖ M] [] {N : Type u_3} {P : Type u_4} [] [Module R' N] [Module R'ᵐᵒᵖ N] [] [] [Module R' P] [Module R'ᵐᵒᵖ P] [] (f : M →ₗ[R'] N) (g : N →ₗ[R'] P) :
TrivSqZeroExt.map (g ∘ₗ f) = .comp