algebra.triv_sq_zero_ext

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

triv_sq_zero_ext R M = (R × M)

source

def triv_sq_zero_ext.inl {R : Type u} {M : Type v} [has_zero M] (r : R) :

triv_sq_zero_ext R M

The canonical inclusion R → triv_sq_zero_ext R M.

Equations

triv_sq_zero_ext.inl r = (r, 0)

source

def triv_sq_zero_ext.inr {R : Type u} {M : Type v} [has_zero R] (m : M) :

triv_sq_zero_ext R M

The canonical inclusion M → triv_sq_zero_ext R M.

Equations

triv_sq_zero_ext.inr m = (0, m)

source

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

x.fst = x.fst

source

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

x.snd = x.snd

source

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

source

@[simp]

theorem triv_sq_zero_ext.fst_inl {R : Type u} {M : Type v} [has_zero M] (r : R) :

(triv_sq_zero_ext.inl r).fst = r

source

@[simp]

theorem triv_sq_zero_ext.snd_inl {R : Type u} {M : Type v} [has_zero M] (r : R) :

(triv_sq_zero_ext.inl r).snd = 0

source

@[simp]

theorem triv_sq_zero_ext.fst_inr {R : Type u} {M : Type v} [has_zero R] (m : M) :

(triv_sq_zero_ext.inr m).fst = 0

source

@[simp]

theorem triv_sq_zero_ext.snd_inr {R : Type u} {M : Type v} [has_zero R] (m : M) :

(triv_sq_zero_ext.inr m).snd = m

source

theorem triv_sq_zero_ext.inl_injective {R : Type u} {M : Type v} [has_zero M] :

function.injective triv_sq_zero_ext.inl

source

theorem triv_sq_zero_ext.inr_injective {R : Type u} {M : Type v} [has_zero R] :

function.injective triv_sq_zero_ext.inr

source

@[instance]

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

has_zero (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.has_zero R M = prod.has_zero

source

@[simp]

theorem triv_sq_zero_ext.fst_zero (R : Type u) (M : Type v) [has_zero R] [has_zero M] :

0.fst = 0

source

@[simp]

theorem triv_sq_zero_ext.snd_zero (R : Type u) (M : Type v) [has_zero R] [has_zero M] :

0.snd = 0

source

@[simp]

theorem triv_sq_zero_ext.inl_zero (R : Type u) (M : Type v) [has_zero R] [has_zero M] :

triv_sq_zero_ext.inl 0 = 0

source

@[simp]

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

triv_sq_zero_ext.inr 0 = 0

source

@[instance]

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

has_add (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.has_add R M = prod.has_add

source

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

source

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

source

@[instance]

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

has_neg (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.has_neg R M = prod.has_neg

source

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

source

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

source

@[instance]

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

add_semigroup (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.add_semigroup R M = prod.add_semigroup

source

@[instance]

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

add_monoid (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.add_monoid R M = prod.add_monoid

source

@[simp]

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

triv_sq_zero_ext.inl (r₁ + r₂) = triv_sq_zero_ext.inl r₁ + triv_sq_zero_ext.inl r₂

source

@[simp]

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

triv_sq_zero_ext.inr (m₁ + m₂) = triv_sq_zero_ext.inr m₁ + triv_sq_zero_ext.inr m₂

source

theorem triv_sq_zero_ext.inl_fst_add_inr_snd_eq (R : Type u) (M : Type v) [add_monoid R] [add_monoid M] (x : triv_sq_zero_ext R M) :

triv_sq_zero_ext.inl x.fst + triv_sq_zero_ext.inr x.snd = x

source

@[instance]

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

add_group (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.add_group R M = prod.add_group

source

@[simp]

theorem triv_sq_zero_ext.inl_neg (R : Type u) (M : Type v) [has_neg R] [add_group M] (r : R) :

triv_sq_zero_ext.inl (-r) = -triv_sq_zero_ext.inl r

source

@[simp]

theorem triv_sq_zero_ext.inr_neg (R : Type u) (M : Type v) [add_group R] [has_neg M] (m : M) :

triv_sq_zero_ext.inr (-m) = -triv_sq_zero_ext.inr m

source

@[instance]

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

add_comm_semigroup (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.add_comm_semigroup R M = prod.add_comm_semigroup

source

@[instance]

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

add_comm_monoid (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.add_comm_monoid R M = prod.add_comm_monoid

source

@[instance]

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

add_comm_group (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.add_comm_group R M = prod.add_comm_group

source

@[instance]

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

has_scalar R (triv_sq_zero_ext R M)

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)}

source

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

source

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

source

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

triv_sq_zero_ext.inr (r • m) = r • triv_sq_zero_ext.inr m

source

@[instance]

def triv_sq_zero_ext.mul_action (R : Type u) (M : Type v) [monoid R] [mul_action R M] :

mul_action R (triv_sq_zero_ext R M)

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 := _}

source

@[instance]

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

distrib_mul_action R (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.distrib_mul_action R M = {to_mul_action := triv_sq_zero_ext.mul_action R M distrib_mul_action.to_mul_action, smul_add := _, smul_zero := _}

source

@[instance]

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

module R (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.module R M = {to_distrib_mul_action := triv_sq_zero_ext.distrib_mul_action R M module.to_distrib_mul_action, add_smul := _, zero_smul := _}

source

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

M →ₗ[R] triv_sq_zero_ext 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' := _}

source

@[simp]

theorem triv_sq_zero_ext.inr_hom_apply (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [module R M] (m : M) :

⇑(triv_sq_zero_ext.inr_hom R M) m = triv_sq_zero_ext.inr m

source

@[instance]

def triv_sq_zero_ext.has_one (R : Type u) (M : Type v) [has_one R] [has_zero M] :

has_one (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.has_one R M = {one := (1, 0)}

source

@[simp]

theorem triv_sq_zero_ext.fst_one (R : Type u) (M : Type v) [has_one R] [has_zero M] :

1.fst = 1

source

@[simp]

theorem triv_sq_zero_ext.snd_one (R : Type u) (M : Type v) [has_one R] [has_zero M] :

1.snd = 0

source

@[simp]

theorem triv_sq_zero_ext.inl_one (R : Type u) (M : Type v) [has_one R] [has_zero M] :

triv_sq_zero_ext.inl 1 = 1

source

@[instance]

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

has_mul (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.has_mul R M = {mul := λ (x y : triv_sq_zero_ext R M), ((x.fst) * y.fst, x.fst • y.snd + y.fst • x.snd)}

source

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

source

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

source

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

triv_sq_zero_ext.inl (r₁ * r₂) = (triv_sq_zero_ext.inl r₁) * triv_sq_zero_ext.inl r₂

source

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) :

(triv_sq_zero_ext.inl r₁) * triv_sq_zero_ext.inl r₂ = triv_sq_zero_ext.inl (r₁ * r₂)

source

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

(triv_sq_zero_ext.inl r) * triv_sq_zero_ext.inr m = triv_sq_zero_ext.inr (r • m)

source

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

(triv_sq_zero_ext.inr m) * triv_sq_zero_ext.inl r = triv_sq_zero_ext.inr (r • m)

source

@[simp]

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

(triv_sq_zero_ext.inr m₁) * triv_sq_zero_ext.inr m₂ = 0

source

@[instance]

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

monoid (triv_sq_zero_ext R M)

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 := _, npow := npow_rec (mul_one_class.to_has_mul (triv_sq_zero_ext R M)), npow_zero' := _, npow_succ' := _}

source

@[instance]

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

comm_semiring (triv_sq_zero_ext R M)

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 := _, nsmul := add_comm_monoid.nsmul (triv_sq_zero_ext.add_comm_monoid R M), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := monoid.mul (triv_sq_zero_ext.monoid R M), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := monoid.one (triv_sq_zero_ext.monoid R M), one_mul := _, mul_one := _, npow := npow (triv_sq_zero_ext.monoid R M), npow_zero' := _, npow_succ' := _, mul_comm := _}

source

@[simp]

theorem triv_sq_zero_ext.inl_hom_apply (R : Type u) (M : Type v) [comm_semiring R] [add_comm_monoid M] [module R M] (r : R) :

⇑(triv_sq_zero_ext.inl_hom R M) r = triv_sq_zero_ext.inl r

source

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

R →+* triv_sq_zero_ext R M

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' := _}

source

@[instance]

def triv_sq_zero_ext.algebra (R : Type u) (M : Type v) [comm_semiring R] [add_comm_monoid M] [module R M] :

algebra R (triv_sq_zero_ext R M)

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' := _}

source

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

triv_sq_zero_ext R M →ₐ[R] R

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' := _}

source

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

triv_sq_zero_ext R M →ₗ[R] M

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' := _}

source

@[simp]

theorem triv_sq_zero_ext.snd_hom_apply (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [module R M] (x : triv_sq_zero_ext R M) :

⇑(triv_sq_zero_ext.snd_hom R M) x = x.snd

mathlib documentation

Trivial Square-Zero Extension #