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
.
Main definitions #
triv_sq_zero_ext.inl
,triv_sq_zero_ext.inr
: the canonical inclusions intotriv_sq_zero_ext R M
.triv_sq_zero_ext.fst
,triv_sq_zero_ext.snd
: the canonical projections fromtriv_sq_zero_ext R M
.triv_sq_zero_ext.algebra
: the associatedR
-algebra structure.triv_sq_zero_ext.lift
: the universal property of the trivial square-zero extension; algebra morphismstriv_sq_zero_ext 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
- triv_sq_zero_ext R M = (R × M)
Instances for triv_sq_zero_ext
- triv_sq_zero_ext.inhabited
- triv_sq_zero_ext.has_zero
- triv_sq_zero_ext.has_add
- triv_sq_zero_ext.has_neg
- triv_sq_zero_ext.add_semigroup
- triv_sq_zero_ext.add_zero_class
- triv_sq_zero_ext.add_monoid
- triv_sq_zero_ext.add_group
- triv_sq_zero_ext.add_comm_semigroup
- triv_sq_zero_ext.add_comm_monoid
- triv_sq_zero_ext.add_comm_group
- triv_sq_zero_ext.has_smul
- triv_sq_zero_ext.is_scalar_tower
- triv_sq_zero_ext.smul_comm_class
- triv_sq_zero_ext.is_central_scalar
- triv_sq_zero_ext.mul_action
- triv_sq_zero_ext.distrib_mul_action
- triv_sq_zero_ext.module
- triv_sq_zero_ext.has_one
- triv_sq_zero_ext.has_mul
- triv_sq_zero_ext.mul_one_class
- triv_sq_zero_ext.add_monoid_with_one
- triv_sq_zero_ext.non_assoc_semiring
- triv_sq_zero_ext.monoid
- triv_sq_zero_ext.comm_monoid
- triv_sq_zero_ext.comm_semiring
- triv_sq_zero_ext.algebra'
- triv_sq_zero_ext.algebra
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
To show a property hold on all triv_sq_zero_ext 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 triv_sq_zero_ext.ind
.
This cannot be marked @[ext]
as it ends up being used instead of linear_map.prod_ext
when
working with R × M
.
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' := _}
The canonical R
-linear 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' := _}
Multiplicative structure #
Equations
- triv_sq_zero_ext.has_one = {one := (1, 0)}
Equations
- triv_sq_zero_ext.mul_one_class = {one := 1, mul := has_mul.mul triv_sq_zero_ext.has_mul, one_mul := _, mul_one := _}
Equations
- triv_sq_zero_ext.add_monoid_with_one = {nat_cast := λ (n : ℕ), (↑n, 0), add := add_monoid.add triv_sq_zero_ext.add_monoid, add_assoc := _, zero := add_monoid.zero triv_sq_zero_ext.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul triv_sq_zero_ext.add_monoid, nsmul_zero' := _, nsmul_succ' := _, one := 1, nat_cast_zero := _, nat_cast_succ := _}
Equations
- triv_sq_zero_ext.non_assoc_semiring = {add := add_monoid_with_one.add triv_sq_zero_ext.add_monoid_with_one, add_assoc := _, zero := add_monoid_with_one.zero triv_sq_zero_ext.add_monoid_with_one, zero_add := _, add_zero := _, nsmul := add_monoid_with_one.nsmul triv_sq_zero_ext.add_monoid_with_one, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := mul_one_class.mul triv_sq_zero_ext.mul_one_class, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := add_monoid_with_one.one triv_sq_zero_ext.add_monoid_with_one, one_mul := _, mul_one := _, nat_cast := add_monoid_with_one.nat_cast triv_sq_zero_ext.add_monoid_with_one, nat_cast_zero := _, nat_cast_succ := _}
Equations
- triv_sq_zero_ext.monoid = {mul := mul_one_class.mul triv_sq_zero_ext.mul_one_class, mul_assoc := _, one := mul_one_class.one triv_sq_zero_ext.mul_one_class, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (triv_sq_zero_ext R M)), npow_zero' := _, npow_succ' := _}
Equations
- triv_sq_zero_ext.comm_monoid = {mul := monoid.mul triv_sq_zero_ext.monoid, mul_assoc := _, one := monoid.one triv_sq_zero_ext.monoid, one_mul := _, mul_one := _, npow := monoid.npow triv_sq_zero_ext.monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}
Equations
- triv_sq_zero_ext.comm_semiring = {add := non_assoc_semiring.add triv_sq_zero_ext.non_assoc_semiring, add_assoc := _, zero := non_assoc_semiring.zero triv_sq_zero_ext.non_assoc_semiring, zero_add := _, add_zero := _, nsmul := non_assoc_semiring.nsmul triv_sq_zero_ext.non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := comm_monoid.mul triv_sq_zero_ext.comm_monoid, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := comm_monoid.one triv_sq_zero_ext.comm_monoid, one_mul := _, mul_one := _, nat_cast := non_assoc_semiring.nat_cast triv_sq_zero_ext.non_assoc_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := comm_monoid.npow triv_sq_zero_ext.comm_monoid, npow_zero' := _, npow_succ' := _, 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_zero_class.to_has_zero M), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
Equations
- triv_sq_zero_ext.algebra' S R M = {to_has_smul := triv_sq_zero_ext.has_smul smul_with_zero.to_has_smul, to_ring_hom := {to_fun := ((triv_sq_zero_ext.inl_hom R M).comp (algebra_map S R)).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
Equations
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' := _}
There is an alg_hom from the trivial square zero extension to any R
-algebra with a submodule
whose products are all zero.
See triv_sq_zero_ext.lift
for this as an equiv.
Equations
- triv_sq_zero_ext.lift_aux f hf = alg_hom.of_linear_map ((algebra.linear_map R A).comp (triv_sq_zero_ext.fst_hom R M).to_linear_map + f.comp (triv_sq_zero_ext.snd_hom R M)) _ _
A universal property of the trivial square-zero extension, providing a unique
triv_sq_zero_ext 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
.
Equations
- triv_sq_zero_ext.lift = {to_fun := λ (f : {f // ∀ (x y : M), ⇑f x * ⇑f y = 0}), triv_sq_zero_ext.lift_aux ↑f _, inv_fun := λ (F : triv_sq_zero_ext R M →ₐ[R] A), ⟨F.to_linear_map.comp (triv_sq_zero_ext.inr_hom R M), _⟩, left_inv := _, right_inv := _}