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:
variables {R M : Type*} [Semiring R] [AddCommMonoid M]
variables [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M]
If we instead work with a commutative R'
acting symmetrically on M
, we write
variables {R' M : Type*} [CommSemiring R'] [AddCommMonoid M]
variables [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 intoTrivSqZeroExt R M
.TrivSqZeroExt.fst
,TrivSqZeroExt.snd
: the canonical projections fromTrivSqZeroExt R M
.triv_sq_zero_ext.algebra
: the associatedR
-algebra structure.TrivSqZeroExt.lift
: the universal property of the trivial square-zero extension; algebra morphismsTrivSqZeroExt R M →ₐ[R] A
are uniquely defined by linear mapsM →ₗ[R] A
for which the product of any two elements in the range is zero.
"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
.
Instances For
The canonical inclusion R → TrivSqZeroExt R M
.
Instances For
The canonical inclusion M → TrivSqZeroExt R M
.
Instances For
The canonical projection TrivSqZeroExt R M → R
.
Instances For
The canonical projection TrivSqZeroExt R M → M
.
Instances For
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
.
This cannot be marked @[ext]
as it ends up being used instead of LinearMap.prod_ext
when
working with R × M
.
The canonical R
-linear inclusion M → TrivSqZeroExt R M
.
Instances For
The canonical R
-linear projection TrivSqZeroExt R M → M
.
Instances For
Multiplicative structure #
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$.
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$.
The canonical inclusion of rings R → TrivSqZeroExt R M
.
Instances For
The canonical R
-algebra projection TrivSqZeroExt R M → R
.
Instances For
There is an alg_hom from the trivial square zero extension to any R
-algebra with a submodule
whose products are all zero.
See TrivSqZeroExt.lift
for this as an equiv.
Instances For
A universal property of the trivial square-zero extension, providing a unique
TrivSqZeroExt R M →ₐ[R] A
for every linear map M →ₗ[R] A
whose range has no non-zero
products.
This isomorphism is named to match the very similar Complex.lift
.