mathlib3 documentation

algebra.triv_sq_zero_ext

Trivial Square-Zero Extension #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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] [add_comm_monoid M]
variables [module R M] [module Rᵐᵒᵖ M] [smul_comm_class R Rᵐᵒᵖ M]

If we instead work with a commutative R' acting symmetrically on M, we write

variables {R' M : Type*} [comm_semiring R'] [add_comm_monoid M]
variables [module R' M] [module R'ᵐᵒᵖ M] [is_central_scalar R' M]

noting that in this context is_central_scalar R' M implies smul_comm_class R' R'ᵐᵒᵖ M.

Many of the later results in this file are only stated for the commutative R' for simplicity.

Main definitions #

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
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
def triv_sq_zero_ext.fst {R : Type u} {M : Type v} (x : triv_sq_zero_ext R 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 : triv_sq_zero_ext R 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 : triv_sq_zero_ext R 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) :
@[simp]
theorem triv_sq_zero_ext.snd_inl {R : Type u} (M : Type v) [has_zero M] (r : R) :
@[simp]
theorem triv_sq_zero_ext.fst_inr (R : Type u) {M : Type v} [has_zero R] (m : M) :
@[simp]
theorem triv_sq_zero_ext.snd_inr (R : Type u) {M : Type v} [has_zero R] (m : M) :

Structures inherited from prod #

Additive operators and scalar multiplication operate elementwise.

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def triv_sq_zero_ext.has_smul {S : Type u_2} {R : Type u} {M : Type v} [has_smul S R] [has_smul S 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} [has_smul T R] [has_smul T M] [has_smul S R] [has_smul S M] [has_smul T S] [is_scalar_tower T S R] [is_scalar_tower T S 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} [has_smul T R] [has_smul T M] [has_smul S R] [has_smul S M] [smul_comm_class T S R] [smul_comm_class T S M] :
@[protected, instance]
@[protected, instance]
def triv_sq_zero_ext.mul_action {S : Type u_2} {R : Type u} {M : Type v} [monoid S] [mul_action S R] [mul_action S M] :
Equations
@[protected, instance]
def triv_sq_zero_ext.module {S : Type u_2} {R : Type u} {M : Type v} [semiring S] [add_comm_monoid R] [add_comm_monoid M] [module S R] [module S 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₂ : triv_sq_zero_ext R 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₂ : triv_sq_zero_ext R 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 : triv_sq_zero_ext R 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 : triv_sq_zero_ext R M) :
(-x).snd = -x.snd
@[simp]
theorem triv_sq_zero_ext.fst_sub {R : Type u} {M : Type v} [has_sub R] [has_sub M] (x₁ x₂ : triv_sq_zero_ext R M) :
(x₁ - x₂).fst = x₁.fst - x₂.fst
@[simp]
theorem triv_sq_zero_ext.snd_sub {R : Type u} {M : Type v} [has_sub R] [has_sub M] (x₁ x₂ : triv_sq_zero_ext R M) :
(x₁ - x₂).snd = x₁.snd - x₂.snd
@[simp]
theorem triv_sq_zero_ext.fst_smul {S : Type u_2} {R : Type u} {M : Type v} [has_smul S R] [has_smul S M] (s : S) (x : triv_sq_zero_ext R 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} [has_smul S R] [has_smul S M] (s : S) (x : triv_sq_zero_ext R M) :
(s x).snd = s x.snd
theorem triv_sq_zero_ext.fst_sum {R : Type u} {M : Type v} {ι : Type u_1} [add_comm_monoid R] [add_comm_monoid M] (s : finset ι) (f : ι triv_sq_zero_ext R M) :
(s.sum (λ (i : ι), f i)).fst = s.sum (λ (i : ι), (f i).fst)
theorem triv_sq_zero_ext.snd_sum {R : Type u} {M : Type v} {ι : Type u_1} [add_comm_monoid R] [add_comm_monoid M] (s : finset ι) (f : ι triv_sq_zero_ext R M) :
(s.sum (λ (i : ι), f i)).snd = s.sum (λ (i : ι), (f i).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] [add_zero_class M] (r₁ r₂ : R) :
@[simp]
theorem triv_sq_zero_ext.inl_sub {R : Type u} (M : Type v) [has_sub R] [sub_neg_zero_monoid M] (r₁ 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] [has_smul S R] [distrib_mul_action S M] (s : S) (r : R) :
theorem triv_sq_zero_ext.inl_sum {R : Type u} (M : Type v) {ι : Type u_1} [add_comm_monoid R] [add_comm_monoid M] (s : finset ι) (f : ι R) :
triv_sq_zero_ext.inl (s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), triv_sq_zero_ext.inl (f i))
@[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} [add_zero_class R] [add_zero_class M] (m₁ m₂ : M) :
@[simp]
theorem triv_sq_zero_ext.inr_sub (R : Type u) {M : Type v} [sub_neg_zero_monoid R] [has_sub M] (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] [smul_with_zero S R] [has_smul S M] (r : S) (m : M) :
theorem triv_sq_zero_ext.inr_sum (R : Type u) {M : Type v} {ι : Type u_1} [add_comm_monoid R] [add_comm_monoid M] (s : finset ι) (f : ι M) :
triv_sq_zero_ext.inr (s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), triv_sq_zero_ext.inr (f i))
theorem triv_sq_zero_ext.ind {R : Type u_1} {M : Type u_2} [add_zero_class R] [add_zero_class M] {P : triv_sq_zero_ext R M Prop} (h : (r : R) (m : M), P (triv_sq_zero_ext.inl r + triv_sq_zero_ext.inr m)) (x : triv_sq_zero_ext R 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] [add_comm_monoid R] [add_comm_monoid M] [add_comm_monoid N] [module S R] [module S M] [module S N] ⦃f g : triv_sq_zero_ext R M →ₗ[S] N⦄ (hl : (r : R), f (triv_sq_zero_ext.inl r) = g (triv_sq_zero_ext.inl r)) (hr : (m : M), f (triv_sq_zero_ext.inr m) = g (triv_sq_zero_ext.inr 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.

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

Equations

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

Equations
@[simp]

Multiplicative structure #

@[protected, instance]
Equations
@[protected, instance]
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] [has_smul R M] [has_smul Rᵐᵒᵖ M] (x₁ x₂ : triv_sq_zero_ext R 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] [has_smul R M] [has_smul Rᵐᵒᵖ M] (x₁ x₂ : triv_sq_zero_ext R M) :
(x₁ * x₂).snd = x₁.fst x₂.snd + mul_opposite.op 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]
@[simp]
theorem triv_sq_zero_ext.inr_mul_inr (R : Type u) {M : Type v} [semiring R] [add_comm_monoid M] [module R M] [module Rᵐᵒᵖ M] (m₁ m₂ : M) :
@[simp]
theorem triv_sq_zero_ext.fst_nat_cast {R : Type u} {M : Type v} [add_monoid_with_one R] [add_monoid M] (n : ) :
@[simp]
theorem triv_sq_zero_ext.snd_nat_cast {R : Type u} {M : Type v} [add_monoid_with_one R] [add_monoid M] (n : ) :
n.snd = 0
@[simp]
theorem triv_sq_zero_ext.fst_int_cast {R : Type u} {M : Type v} [add_group_with_one R] [add_group M] (z : ) :
@[simp]
theorem triv_sq_zero_ext.snd_int_cast {R : Type u} {M : Type v} [add_group_with_one R] [add_group M] (z : ) :
z.snd = 0
@[protected, instance]

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
@[simp]
theorem triv_sq_zero_ext.fst_pow {R : Type u} {M : Type v} [monoid R] [add_monoid M] [distrib_mul_action R M] [distrib_mul_action Rᵐᵒᵖ M] (x : triv_sq_zero_ext R M) (n : ) :
(x ^ n).fst = x.fst ^ n
theorem triv_sq_zero_ext.snd_pow_eq_sum {R : Type u} {M : Type v} [monoid R] [add_monoid M] [distrib_mul_action R M] [distrib_mul_action Rᵐᵒᵖ M] (x : triv_sq_zero_ext R M) (n : ) :
(x ^ n).snd = (list.map (λ (i : ), x.fst ^ (n.pred - i) mul_opposite.op (x.fst ^ i) x.snd) (list.range n)).sum
@[simp]

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 → triv_sq_zero_ext R M.

Equations
@[protected, instance]
Equations

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} [comm_semiring R'] [add_comm_monoid M] [module R' M] [module R'ᵐᵒᵖ M] [is_central_scalar R' M] {A : Type u_1} [semiring A] [algebra R' A] ⦃f g : triv_sq_zero_ext R' M →ₐ[R'] A⦄ (h : (m : M), f (triv_sq_zero_ext.inr m) = g (triv_sq_zero_ext.inr m)) :
f = g
@[ext]
def triv_sq_zero_ext.lift_aux {R' : Type u} {M : Type v} [comm_semiring R'] [add_comm_monoid M] [module R' M] [module R'ᵐᵒᵖ M] [is_central_scalar R' M] {A : Type u_2} [semiring A] [algebra R' 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} [comm_semiring R'] [add_comm_monoid M] [module R' M] [module R'ᵐᵒᵖ M] [is_central_scalar R' M] {A : Type u_2} [semiring A] [algebra R' A] (f : M →ₗ[R'] A) (hf : (x y : M), f x * f y = 0) (m : M) :
@[simp]
theorem triv_sq_zero_ext.lift_aux_comp_inr_hom {R' : Type u} {M : Type v} [comm_semiring R'] [add_comm_monoid M] [module R' M] [module R'ᵐᵒᵖ M] [is_central_scalar R' M] {A : Type u_2} [semiring A] [algebra R' A] (f : M →ₗ[R'] A) (hf : (x y : M), f x * f y = 0) :
def triv_sq_zero_ext.lift {R' : Type u} {M : Type v} [comm_semiring R'] [add_comm_monoid M] [module R' M] [module R'ᵐᵒᵖ M] [is_central_scalar R' M] {A : Type u_2} [semiring A] [algebra R' A] :
{f // (x y : M), f x * f y = 0} (triv_sq_zero_ext R' 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} [comm_semiring R'] [add_comm_monoid M] [module R' M] [module R'ᵐᵒᵖ M] [is_central_scalar R' M] {A : Type u_2} [semiring A] [algebra R' A] (f : {f // (x y : M), f x * f y = 0}) :