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 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 →ₐ[S] A
are uniquely defined by an algebra morphismf : R →ₐ[S] A
onR
and a linear mapg : M →ₗ[S] A
onM
such that:g x * g y = 0
: the elements ofM
continue to square to zero.g (r •> x) = f r * g x
andg (x <• r) = g x * f r
: left and right actions are preserved byg
.
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
.
Equations
- TrivSqZeroExt R M = (R × M)
Instances For
Equations
- TrivSqZeroExt.inhabited = instInhabitedProd
Equations
- TrivSqZeroExt.zero = Prod.instZero
Equations
- TrivSqZeroExt.add = Prod.instAdd
Equations
- TrivSqZeroExt.sub = Prod.instSub
Equations
- TrivSqZeroExt.neg = Prod.instNeg
Equations
- TrivSqZeroExt.addSemigroup = Prod.instAddSemigroup
Equations
- TrivSqZeroExt.addZeroClass = Prod.instAddZeroClass
Equations
- TrivSqZeroExt.addMonoid = Prod.instAddMonoid
Equations
- TrivSqZeroExt.addGroup = Prod.instAddGroup
Equations
- TrivSqZeroExt.addCommSemigroup = Prod.instAddCommSemigroup
Equations
- TrivSqZeroExt.addCommMonoid = Prod.instAddCommMonoid
Equations
- TrivSqZeroExt.addCommGroup = Prod.instAddCommGroup
Equations
- TrivSqZeroExt.smul = Prod.smul
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- TrivSqZeroExt.distribMulAction = Prod.distribMulAction
Equations
- TrivSqZeroExt.module = Prod.instModule
The trivial square-zero extension is nontrivial if it is over a nontrivial ring.
Equations
- ⋯ = ⋯
The trivial square-zero extension is nontrivial if it is over a nontrivial module.
Equations
- ⋯ = ⋯
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 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
.
Equations
- TrivSqZeroExt.inrHom R M = { toFun := TrivSqZeroExt.inr, map_add' := ⋯, map_smul' := ⋯ }
Instances For
The canonical R
-linear projection TrivSqZeroExt R M → M
.
Equations
- TrivSqZeroExt.sndHom R M = { toFun := TrivSqZeroExt.snd, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Multiplicative structure #
Equations
- TrivSqZeroExt.one = { one := (1, 0) }
Equations
- TrivSqZeroExt.mul = { mul := fun (x y : TrivSqZeroExt R M) => (x.1 * y.1, x.1 • y.2 + MulOpposite.op y.1 • x.2) }
Equations
- TrivSqZeroExt.mulOneClass = MulOneClass.mk ⋯ ⋯
Equations
- TrivSqZeroExt.addMonoidWithOne = AddMonoidWithOne.mk ⋯ ⋯
Alias of TrivSqZeroExt.fst_natCast
.
Alias of TrivSqZeroExt.snd_natCast
.
Alias of TrivSqZeroExt.inl_natCast
.
Equations
- TrivSqZeroExt.addGroupWithOne = AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Alias of TrivSqZeroExt.fst_intCast
.
Alias of TrivSqZeroExt.snd_intCast
.
Alias of TrivSqZeroExt.inl_intCast
.
Equations
- TrivSqZeroExt.nonAssocSemiring = NonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯
Equations
- TrivSqZeroExt.nonAssocRing = 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.
Equations
- TrivSqZeroExt.monoid = Monoid.mk ⋯ ⋯ (fun (n : ℕ) (x : TrivSqZeroExt R M) => x ^ n) ⋯ ⋯
Equations
- TrivSqZeroExt.semiring = 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$.
Equations
- TrivSqZeroExt.commMonoid = CommMonoid.mk ⋯
Equations
- TrivSqZeroExt.commSemiring = CommSemiring.mk ⋯
Equations
- TrivSqZeroExt.commRing = CommRing.mk ⋯
The canonical inclusion of rings R → TrivSqZeroExt R M
.
Equations
- TrivSqZeroExt.inlHom R M = { toFun := TrivSqZeroExt.inl, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Inversion of the trivial-square-zero extension, sending $r + m$ to $r^{-1} - r^{-1}mr^{-1}$.
Strictly this is only a two-sided inverse when the left and right actions associate.
Equations
- TrivSqZeroExt.instInv = { inv := fun (b : TrivSqZeroExt R M) => (b.1⁻¹, -(MulOpposite.op b.1⁻¹ • b.1⁻¹ • b.2)) }
This section is heavily inspired by analogous results about matrices.
x.fst : R
is invertible when x : tzre R M
is.
Equations
Instances For
x : tzre R M
is invertible when x.fst : R
is.
Equations
Instances For
Together TrivSqZeroExt.detInvertibleOfInvertible
and TrivSqZeroExt.invertibleOfDetInvertible
form an equivalence, although both sides of the equiv are subsingleton anyway.
Equations
- One or more equations did not get rendered due to their size.
Instances For
When lowered to a prop, Matrix.invertibleEquivInvertibleFst
forms an iff
.
Equations
- TrivSqZeroExt.algebra' S R M = Algebra.mk ((TrivSqZeroExt.inlHom R M).comp (algebraMap S R)) ⋯ ⋯
Equations
- TrivSqZeroExt.instAlgebra R' M = TrivSqZeroExt.algebra' R' R' M
The canonical S
-algebra projection TrivSqZeroExt R M → R
.
Equations
- TrivSqZeroExt.fstHom S R M = { toFun := TrivSqZeroExt.fst, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
The canonical S
-algebra inclusion R → TrivSqZeroExt R M
.
Equations
- TrivSqZeroExt.inlAlgHom S R M = { toFun := TrivSqZeroExt.inl, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
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 ofM
continue to square to zero.g (r •> x) = f r * g x
andg (x <• r) = g x * f r
: scalar multiplication on the left and right is sent to left- and right- multiplication by the image underf
.
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
- TrivSqZeroExt.lift f g hg hfg hgf = AlgHom.ofLinearMap ((f.comp (TrivSqZeroExt.fstHom S R M)).toLinearMap + g ∘ₗ ↑S (TrivSqZeroExt.sndHom R M)) ⋯ ⋯
Instances For
When applied to inr
and inl
themselves, lift
is the identity.
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
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
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.map f = TrivSqZeroExt.liftEquivOfComm ⟨TrivSqZeroExt.inrHom R' N ∘ₗ f, ⋯⟩