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
.
"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
- triv_sq_zero_ext R M = (R × M)
The canonical inclusion R → triv_sq_zero_ext R M
.
Equations
- triv_sq_zero_ext.inl r = (r, 0)
The canonical inclusion M → triv_sq_zero_ext R M
.
Equations
- triv_sq_zero_ext.inr m = (0, m)
The canonical projection triv_sq_zero_ext R M → R
.
The canonical projection triv_sq_zero_ext R M → M
.
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
- triv_sq_zero_ext.has_scalar R M = {smul := λ (r : R) (x : triv_sq_zero_ext R M), (r * x.fst, r • x.snd)}
Equations
- triv_sq_zero_ext.mul_action R M = {to_has_scalar := triv_sq_zero_ext.has_scalar R M mul_action.to_has_scalar, one_smul := _, mul_smul := _}
Equations
Equations
Equations
- triv_sq_zero_ext.module R M = {to_distrib_mul_action := semimodule.to_distrib_mul_action (triv_sq_zero_ext.semimodule R M), add_smul := _, zero_smul := _}
The canonical R
-linear inclusion M → triv_sq_zero_ext R M
.
Equations
- triv_sq_zero_ext.inr_hom R M = {to_fun := triv_sq_zero_ext.inr (mul_zero_class.to_has_zero R), map_add' := _, map_smul' := _}
Equations
- triv_sq_zero_ext.has_one R M = {one := (1, 0)}
Equations
- triv_sq_zero_ext.monoid R M = {mul := has_mul.mul (triv_sq_zero_ext.has_mul R M), mul_assoc := _, one := 1, one_mul := _, mul_one := _}
Equations
- triv_sq_zero_ext.comm_semiring R M = {add := add_comm_monoid.add (triv_sq_zero_ext.add_comm_monoid R M), add_assoc := _, zero := add_comm_monoid.zero (triv_sq_zero_ext.add_comm_monoid R M), zero_add := _, add_zero := _, add_comm := _, mul := monoid.mul (triv_sq_zero_ext.monoid R M), mul_assoc := _, one := monoid.one (triv_sq_zero_ext.monoid R M), one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}
The canonical inclusion of rings R → triv_sq_zero_ext R M
.
Equations
- triv_sq_zero_ext.inl_hom R M = {to_fun := triv_sq_zero_ext.inl (add_monoid.to_has_zero M), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
Equations
- triv_sq_zero_ext.algebra R M = {to_has_scalar := mul_action.to_has_scalar distrib_mul_action.to_mul_action, to_ring_hom := {to_fun := (triv_sq_zero_ext.inl_hom R M).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
The canonical R
-algebra projection triv_sq_zero_ext R M → R
.
Equations
- triv_sq_zero_ext.fst_hom R M = {to_fun := triv_sq_zero_ext.fst M, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}
The canonical R
-module projection triv_sq_zero_ext R M → M
.
Equations
- triv_sq_zero_ext.snd_hom R M = {to_fun := triv_sq_zero_ext.snd M, map_add' := _, map_smul' := _}