# mathlibdocumentation

algebra.triv_sq_zero_ext

# 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 into triv_sq_zero_ext R M.
• triv_sq_zero_ext.fst, triv_sq_zero_ext.snd: the canonical projections from triv_sq_zero_ext R M.
• triv_sq_zero_ext.algebra: the associated R-algebra structure.
• triv_sq_zero_ext.lift: the universal property of the trivial square-zero extension; algebra morphisms triv_sq_zero_ext 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 triv_sq_zero_ext (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 triv_sq_zero_ext
def triv_sq_zero_ext.inl {R : Type u} {M : Type v} [has_zero M] (r : R) :

The canonical inclusion R → triv_sq_zero_ext R M.

Equations
• = (r, 0)
def triv_sq_zero_ext.inr {R : Type u} {M : Type v} [has_zero R] (m : M) :

The canonical inclusion M → triv_sq_zero_ext R M.

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

The canonical projection triv_sq_zero_ext R M → R.

Equations
def triv_sq_zero_ext.snd {R : Type u} {M : Type v} (x : M) :
M

The canonical projection triv_sq_zero_ext R M → M.

Equations
@[simp]
theorem triv_sq_zero_ext.fst_mk {R : Type u} {M : Type v} (r : R) (m : M) :
@[simp]
theorem triv_sq_zero_ext.snd_mk {R : Type u} {M : Type v} (r : R) (m : M) :
@[ext]
theorem triv_sq_zero_ext.ext {R : Type u} {M : Type v} {x y : M} (h1 : x.fst = y.fst) (h2 : x.snd = y.snd) :
x = y
@[simp]
theorem triv_sq_zero_ext.fst_inl {R : Type u} (M : Type v) [has_zero M] (r : R) :
= r
@[simp]
theorem triv_sq_zero_ext.snd_inl {R : Type u} (M : Type v) [has_zero M] (r : R) :
= 0
@[simp]
theorem triv_sq_zero_ext.fst_inr (R : Type u) {M : Type v} [has_zero R] (m : M) :
= 0
@[simp]
theorem triv_sq_zero_ext.snd_inr (R : Type u) {M : Type v} [has_zero R] (m : M) :
= m
theorem triv_sq_zero_ext.inl_injective {R : Type u} {M : Type v} [has_zero M] :
theorem triv_sq_zero_ext.inr_injective {R : Type u} {M : Type v} [has_zero R] :

### Structures inherited from prod#

Additive operators and scalar multiplication operate elementwise.

@[protected, instance]
def triv_sq_zero_ext.inhabited {R : Type u} {M : Type v} [inhabited R] [inhabited M] :
Equations
@[protected, instance]
def triv_sq_zero_ext.has_zero {R : Type u} {M : Type v} [has_zero R] [has_zero M] :
Equations
@[protected, instance]
def triv_sq_zero_ext.has_add {R : Type u} {M : Type v} [has_add R] [has_add M] :
Equations
@[protected, instance]
def triv_sq_zero_ext.has_neg {R : Type u} {M : Type v} [has_neg R] [has_neg M] :
Equations
@[protected, instance]
def triv_sq_zero_ext.add_semigroup {R : Type u} {M : Type v}  :
Equations
@[protected, instance]
def triv_sq_zero_ext.add_zero_class {R : Type u} {M : Type v}  :
Equations
@[protected, instance]
def triv_sq_zero_ext.add_monoid {R : Type u} {M : Type v} [add_monoid R] [add_monoid M] :
Equations
@[protected, instance]
def triv_sq_zero_ext.add_group {R : Type u} {M : Type v} [add_group R] [add_group M] :
Equations
@[protected, instance]
def triv_sq_zero_ext.add_comm_semigroup {R : Type u} {M : Type v}  :
Equations
@[protected, instance]
def triv_sq_zero_ext.add_comm_monoid {R : Type u} {M : Type v}  :
Equations
@[protected, instance]
def triv_sq_zero_ext.add_comm_group {R : Type u} {M : Type v}  :
Equations
@[protected, instance]
def triv_sq_zero_ext.has_smul {S : Type u_2} {R : Type u} {M : Type v} [ R] [ M] :
M)
Equations
@[protected, instance]
def triv_sq_zero_ext.is_scalar_tower {T : Type u_1} {S : Type u_2} {R : Type u} {M : Type v} [ R] [ M] [ R] [ M] [ S] [ R] [ M] :
M)
@[protected, instance]
def triv_sq_zero_ext.smul_comm_class {T : Type u_1} {S : Type u_2} {R : Type u} {M : Type v} [ R] [ M] [ R] [ M] [ R] [ M] :
M)
@[protected, instance]
def triv_sq_zero_ext.is_central_scalar {S : Type u_2} {R : Type u} {M : Type v} [ R] [ M] [ R] [ M] [ R] [ M] :
@[protected, instance]
def triv_sq_zero_ext.mul_action {S : Type u_2} {R : Type u} {M : Type v} [monoid S] [ R] [ M] :
M)
Equations
@[protected, instance]
def triv_sq_zero_ext.distrib_mul_action {S : Type u_2} {R : Type u} {M : Type v} [monoid S] [add_monoid R] [add_monoid M] [ R] [ M] :
Equations
@[protected, instance]
def triv_sq_zero_ext.module {S : Type u_2} {R : Type u} {M : Type v} [semiring S] [ R] [ M] :
M)
Equations
@[simp]
theorem triv_sq_zero_ext.fst_zero {R : Type u} {M : Type v} [has_zero R] [has_zero M] :
0.fst = 0
@[simp]
theorem triv_sq_zero_ext.snd_zero {R : Type u} {M : Type v} [has_zero R] [has_zero M] :
0.snd = 0
@[simp]
theorem triv_sq_zero_ext.fst_add {R : Type u} {M : Type v} [has_add R] [has_add M] (x₁ x₂ : M) :
(x₁ + x₂).fst = x₁.fst + x₂.fst
@[simp]
theorem triv_sq_zero_ext.snd_add {R : Type u} {M : Type v} [has_add R] [has_add M] (x₁ x₂ : M) :
(x₁ + x₂).snd = x₁.snd + x₂.snd
@[simp]
theorem triv_sq_zero_ext.fst_neg {R : Type u} {M : Type v} [has_neg R] [has_neg M] (x : M) :
(-x).fst = -x.fst
@[simp]
theorem triv_sq_zero_ext.snd_neg {R : Type u} {M : Type v} [has_neg R] [has_neg M] (x : M) :
(-x).snd = -x.snd
@[simp]
theorem triv_sq_zero_ext.fst_smul {S : Type u_2} {R : Type u} {M : Type v} [ R] [ M] (s : S) (x : M) :
(s x).fst = s x.fst
@[simp]
theorem triv_sq_zero_ext.snd_smul {S : Type u_2} {R : Type u} {M : Type v} [ R] [ M] (s : S) (x : M) :
(s x).snd = s x.snd
@[simp]
theorem triv_sq_zero_ext.inl_zero {R : Type u} (M : Type v) [has_zero R] [has_zero M] :
@[simp]
theorem triv_sq_zero_ext.inl_add {R : Type u} (M : Type v) [has_add R] (r₁ r₂ : R) :
triv_sq_zero_ext.inl (r₁ + r₂) =
@[simp]
theorem triv_sq_zero_ext.inl_neg {R : Type u} (M : Type v) [has_neg R] [add_group M] (r : R) :
@[simp]
theorem triv_sq_zero_ext.inl_smul {S : Type u_2} {R : Type u} (M : Type v) [monoid S] [add_monoid M] [ R] [ M] (s : S) (r : R) :
@[simp]
theorem triv_sq_zero_ext.inr_zero (R : Type u) {M : Type v} [has_zero R] [has_zero M] :
@[simp]
theorem triv_sq_zero_ext.inr_add (R : Type u) {M : Type v} (m₁ m₂ : M) :
triv_sq_zero_ext.inr (m₁ + m₂) =
@[simp]
theorem triv_sq_zero_ext.inr_neg (R : Type u) {M : Type v} [add_group R] [has_neg M] (m : M) :
@[simp]
theorem triv_sq_zero_ext.inr_smul {S : Type u_2} (R : Type u) {M : Type v} [has_zero R] [has_zero S] [ R] [ M] (r : S) (m : M) :
theorem triv_sq_zero_ext.inl_fst_add_inr_snd_eq {R : Type u} {M : Type v} (x : M) :
theorem triv_sq_zero_ext.ind {R : Type u_1} {M : Type u_2} {P : → Prop} (h : ∀ (r : R) (m : M), ) (x : M) :
P x

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.

theorem triv_sq_zero_ext.linear_map_ext {S : Type u_2} {R : Type u} {M : Type v} {N : Type u_1} [semiring S] [ R] [ M] [ N] ⦃f g : →ₗ[S] N⦄ (hl : ∀ (r : R), = ) (hr : ∀ (m : M), = ) :
f = g

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

def triv_sq_zero_ext.inr_hom (R : Type u) (M : Type v) [semiring R] [ M] :

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

Equations
@[simp]
theorem triv_sq_zero_ext.inr_hom_apply (R : Type u) (M : Type v) [semiring R] [ M] (m : M) :
def triv_sq_zero_ext.snd_hom (R : Type u) (M : Type v) [semiring R] [ M] :

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

Equations
@[simp]
theorem triv_sq_zero_ext.snd_hom_apply (R : Type u) (M : Type v) [semiring R] [ M] (x : M) :
x = x.snd

### Multiplicative structure #

@[protected, instance]
def triv_sq_zero_ext.has_one {R : Type u} {M : Type v} [has_one R] [has_zero M] :
Equations
@[protected, instance]
def triv_sq_zero_ext.has_mul {R : Type u} {M : Type v} [has_mul R] [has_add M] [ M] :
Equations
@[simp]
theorem triv_sq_zero_ext.fst_one {R : Type u} {M : Type v} [has_one R] [has_zero M] :
1.fst = 1
@[simp]
theorem triv_sq_zero_ext.snd_one {R : Type u} {M : Type v} [has_one R] [has_zero M] :
1.snd = 0
@[simp]
theorem triv_sq_zero_ext.fst_mul {R : Type u} {M : Type v} [has_mul R] [has_add M] [ M] (x₁ x₂ : M) :
(x₁ * x₂).fst = x₁.fst * x₂.fst
@[simp]
theorem triv_sq_zero_ext.snd_mul {R : Type u} {M : Type v} [has_mul R] [has_add M] [ M] (x₁ x₂ : M) :
(x₁ * x₂).snd = x₁.fst x₂.snd + x₂.fst x₁.snd
@[simp]
theorem triv_sq_zero_ext.inl_one {R : Type u} (M : Type v) [has_one R] [has_zero M] :
@[simp]
theorem triv_sq_zero_ext.inl_mul {R : Type u} (M : Type v) [monoid R] [add_monoid M] [ M] (r₁ r₂ : R) :
triv_sq_zero_ext.inl (r₁ * r₂) =
theorem triv_sq_zero_ext.inl_mul_inl {R : Type u} (M : Type v) [monoid R] [add_monoid M] [ M] (r₁ r₂ : R) :
= triv_sq_zero_ext.inl (r₁ * r₂)
@[simp]
theorem triv_sq_zero_ext.inr_mul_inr (R : Type u) {M : Type v} [semiring R] [ M] (m₁ m₂ : M) :
theorem triv_sq_zero_ext.inl_mul_inr {R : Type u} {M : Type v} [semiring R] [ M] (r : R) (m : M) :
theorem triv_sq_zero_ext.inr_mul_inl {R : Type u} {M : Type v} [semiring R] [ M] (r : R) (m : M) :
@[protected, instance]
def triv_sq_zero_ext.mul_one_class {R : Type u} {M : Type v} [monoid R] [add_monoid M] [ M] :
Equations
@[protected, instance]
def triv_sq_zero_ext.add_monoid_with_one {R : Type u} {M : Type v} [add_monoid M] :
Equations
@[protected, instance]
def triv_sq_zero_ext.non_assoc_semiring {R : Type u} {M : Type v} [semiring R] [ M] :
Equations
@[protected, instance]
def triv_sq_zero_ext.monoid {R : Type u} {M : Type v} [comm_monoid R] [add_monoid M] [ M] :
Equations
@[protected, instance]
def triv_sq_zero_ext.comm_monoid {R : Type u} {M : Type v} [comm_monoid R] [ M] :
Equations
@[protected, instance]
def triv_sq_zero_ext.comm_semiring {R : Type u} {M : Type v} [ M] :
Equations
@[simp]
theorem triv_sq_zero_ext.inl_hom_apply (R : Type u) (M : Type v) [semiring R] [ M] (r : R) :
def triv_sq_zero_ext.inl_hom (R : Type u) (M : Type v) [semiring R] [ M] :

The canonical inclusion of rings R → triv_sq_zero_ext R M.

Equations
@[protected, instance]
def triv_sq_zero_ext.algebra' (S : Type u_1) (R : Type u) (M : Type v) [ R] [ M] [ M] [ M] :
M)
Equations
@[protected, instance]
def triv_sq_zero_ext.algebra (R : Type u) (M : Type v) [ M] :
M)
Equations
theorem triv_sq_zero_ext.algebra_map_eq_inl (R : Type u) (M : Type v) [ M] :
theorem triv_sq_zero_ext.algebra_map_eq_inl_hom (R : Type u) (M : Type v) [ M] :
M) =
theorem triv_sq_zero_ext.algebra_map_eq_inl' (S : Type u_1) (R : Type u) (M : Type v) [ R] [ M] [ M] [ M] (s : S) :
@[simp]
theorem triv_sq_zero_ext.fst_hom_apply (R : Type u) (M : Type v) [ M] (x : M) :
x = x.fst
def triv_sq_zero_ext.fst_hom (R : Type u) (M : Type v) [ M] :

The canonical R-algebra projection triv_sq_zero_ext R M → R.

Equations
theorem triv_sq_zero_ext.alg_hom_ext {R : Type u} {M : Type v} [ M] {A : Type u_1} [semiring A] [ A] ⦃f g : →ₐ[R] A⦄ (h : ∀ (m : M), = ) :
f = g
@[ext]
theorem triv_sq_zero_ext.alg_hom_ext' {R : Type u} {M : Type v} [ M] {A : Type u_1} [semiring A] [ A] ⦃f g : →ₐ[R] A⦄ (h : = ) :
f = g
def triv_sq_zero_ext.lift_aux {R : Type u} {M : Type v} [ M] {A : Type u_2} [semiring A] [ A] (f : M →ₗ[R] A) (hf : ∀ (x y : M), f x * f y = 0) :

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
@[simp]
theorem triv_sq_zero_ext.lift_aux_apply_inr {R : Type u} {M : Type v} [ M] {A : Type u_2} [semiring A] [ A] (f : M →ₗ[R] A) (hf : ∀ (x y : M), f x * f y = 0) (m : M) :
= f m
@[simp]
theorem triv_sq_zero_ext.lift_aux_comp_inr_hom {R : Type u} {M : Type v} [ M] {A : Type u_2} [semiring A] [ A] (f : M →ₗ[R] A) (hf : ∀ (x y : M), f x * f y = 0) :
= f
@[simp]
theorem triv_sq_zero_ext.lift_aux_inr_hom {R : Type u} {M : Type v} [ M] :
def triv_sq_zero_ext.lift {R : Type u} {M : Type v} [ M] {A : Type u_2} [semiring A] [ A] :
{f // ∀ (x y : M), f x * f y = 0} M →ₐ[R] A)

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
@[simp]
theorem triv_sq_zero_ext.lift_apply {R : Type u} {M : Type v} [ M] {A : Type u_2} [semiring A] [ A] (f : {f // ∀ (x y : M), f x * f y = 0}) :
@[simp]
theorem triv_sq_zero_ext.lift_symm_apply_coe {R : Type u} {M : Type v} [ M] {A : Type u_2} [semiring A] [ A] (F : →ₐ[R] A) :