mathlib documentation

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.

@[nolint]
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
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
@[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) :

@[instance]
def triv_sq_zero_ext.has_zero (R : Type u) (M : Type v) [has_zero R] [has_zero 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.inl_zero (R : Type u) (M : Type v) [has_zero R] [has_zero M] :

@[simp]
theorem triv_sq_zero_ext.inr_zero (R : Type u) (M : Type v) [has_zero R] [has_zero M] :

@[instance]
def triv_sq_zero_ext.has_add (R : Type u) (M : Type v) [has_add R] [has_add M] :

Equations
@[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

@[instance]
def triv_sq_zero_ext.has_neg (R : Type u) (M : Type v) [has_neg R] [has_neg M] :

Equations
@[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

@[instance]
def triv_sq_zero_ext.add_monoid (R : Type u) (M : Type v) [add_monoid R] [add_monoid M] :

Equations
@[simp]
theorem triv_sq_zero_ext.inl_add (R : Type u) (M : Type v) [has_add R] [add_monoid M] (r₁ r₂ : R) :

@[simp]
theorem triv_sq_zero_ext.inr_add (R : Type u) (M : Type v) [add_monoid R] [has_add M] (m₁ m₂ : M) :

@[instance]
def triv_sq_zero_ext.add_group (R : Type u) (M : Type v) [add_group R] [add_group M] :

Equations
@[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.inr_neg (R : Type u) (M : Type v) [add_group R] [has_neg M] (m : M) :

@[instance]
def triv_sq_zero_ext.has_scalar (R : Type u) (M : Type v) [has_mul R] [has_scalar R M] :

Equations
@[simp]
theorem triv_sq_zero_ext.fst_smul (R : Type u) (M : Type v) [has_mul R] [has_scalar R M] (r : R) (x : triv_sq_zero_ext R M) :
(r x).fst = r * x.fst

@[simp]
theorem triv_sq_zero_ext.snd_smul (R : Type u) (M : Type v) [has_mul R] [has_scalar R M] (r : R) (x : triv_sq_zero_ext R M) :
(r x).snd = r x.snd

@[simp]
theorem triv_sq_zero_ext.inr_smul (R : Type u) (M : Type v) [mul_zero_class R] [has_scalar R M] (r : R) (m : M) :

def triv_sq_zero_ext.inr_hom (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semimodule 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] [add_comm_monoid M] [semimodule R M] (m : M) :

@[instance]
def triv_sq_zero_ext.has_one (R : Type u) (M : Type v) [has_one R] [has_zero 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.inl_one (R : Type u) (M : Type v) [has_one R] [has_zero M] :

@[instance]
def triv_sq_zero_ext.has_mul (R : Type u) (M : Type v) [has_mul R] [has_add M] [has_scalar R M] :

Equations
@[simp]
theorem triv_sq_zero_ext.fst_mul (R : Type u) (M : Type v) [has_mul R] [has_add M] [has_scalar 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_scalar R M] (x₁ x₂ : triv_sq_zero_ext R M) :
(x₁ * x₂).snd = x₁.fst x₂.snd + x₂.fst x₁.snd

@[simp]
theorem triv_sq_zero_ext.inl_mul (R : Type u) (M : Type v) [monoid R] [add_monoid M] [distrib_mul_action R M] (r₁ r₂ : R) :

theorem triv_sq_zero_ext.inl_mul_inl (R : Type u) (M : Type v) [monoid R] [add_monoid M] [distrib_mul_action R M] (r₁ r₂ : R) :

theorem triv_sq_zero_ext.inl_mul_inr (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semimodule R M] (r : R) (m : M) :

theorem triv_sq_zero_ext.inr_mul_inl (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semimodule R M] (r : R) (m : M) :

@[simp]
theorem triv_sq_zero_ext.inr_mul_inr (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semimodule R M] (m₁ m₂ : M) :

@[instance]
def triv_sq_zero_ext.monoid (R : Type u) (M : Type v) [comm_monoid R] [add_monoid M] [distrib_mul_action R M] :

Equations
@[simp]

def triv_sq_zero_ext.inl_hom (R : Type u) (M : Type v) [comm_semiring R] [add_comm_monoid M] [semimodule R M] :

The canonical inclusion of rings R → triv_sq_zero_ext R M.

Equations
def triv_sq_zero_ext.fst_hom (R : Type u) (M : Type v) [comm_semiring R] [add_comm_monoid M] [semimodule R M] :

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

Equations
def triv_sq_zero_ext.snd_hom (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [semimodule R M] :

The canonical R-module 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] [add_comm_monoid M] [semimodule R M] (x : triv_sq_zero_ext R M) :