algebra.triv_sq_zero_ext

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)

Instances for triv_sq_zero_ext

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

@[simp]

theorem triv_sq_zero_ext.fst_mk {R : Type u} {M : Type v} (r : R) (m : M) :

triv_sq_zero_ext.fst (r, m) = r

source

@[simp]

theorem triv_sq_zero_ext.snd_mk {R : Type u} {M : Type v} (r : R) (m : M) :

triv_sq_zero_ext.snd (r, m) = m

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_comp_inl {R : Type u} (M : Type v) [has_zero M] :

triv_sq_zero_ext.fst ∘ triv_sq_zero_ext.inl = id

source

@[simp]

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

triv_sq_zero_ext.snd ∘ triv_sq_zero_ext.inl = 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

@[simp]

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

triv_sq_zero_ext.fst ∘ triv_sq_zero_ext.inr = 0

source

@[simp]

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

triv_sq_zero_ext.snd ∘ triv_sq_zero_ext.inr = id

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

@[protected, instance]

def triv_sq_zero_ext.inhabited {R : Type u} {M : Type v} [inhabited R] [inhabited M] :

inhabited (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.inhabited = prod.inhabited

source

@[protected, 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 = prod.has_zero

source

@[protected, 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 = prod.has_add

source

@[protected, instance]

def triv_sq_zero_ext.has_sub {R : Type u} {M : Type v} [has_sub R] [has_sub M] :

has_sub (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.has_sub = prod.has_sub

source

@[protected, 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 = prod.has_neg

source

@[protected, 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 = prod.add_semigroup

source

@[protected, instance]

def triv_sq_zero_ext.add_zero_class {R : Type u} {M : Type v} [add_zero_class R] [add_zero_class M] :

add_zero_class (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.add_zero_class = prod.add_zero_class

source

@[protected, 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 = prod.add_monoid

source

@[protected, 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 = prod.add_group

source

@[protected, 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 = prod.add_comm_semigroup

source

@[protected, 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 = prod.add_comm_monoid

source

@[protected, 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 = prod.add_comm_group

source

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

has_smul S (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.has_smul = prod.has_smul

source

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

is_scalar_tower T S (triv_sq_zero_ext R M)

source

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

smul_comm_class T S (triv_sq_zero_ext R M)

source

@[protected, instance]

def triv_sq_zero_ext.is_central_scalar {S : Type u_2} {R : Type u} {M : Type v} [has_smul S R] [has_smul S M] [has_smul Sᵐᵒᵖ R] [has_smul Sᵐᵒᵖ M] [is_central_scalar S R] [is_central_scalar S M] :

is_central_scalar S (triv_sq_zero_ext R M)

source

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

mul_action S (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.mul_action = prod.mul_action

source

@[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] [distrib_mul_action S R] [distrib_mul_action S M] :

distrib_mul_action S (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.distrib_mul_action = prod.distrib_mul_action

source

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

module S (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.module = prod.module

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.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

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

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

source

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

source

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

source

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

source

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)

source

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)

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.inl_add {R : Type u} (M : Type v) [has_add R] [add_zero_class 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.inl_neg {R : Type u} (M : Type v) [has_neg R] [sub_neg_zero_monoid M] (r : R) :

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

source

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

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

triv_sq_zero_ext.inl (s • r) = s • triv_sq_zero_ext.inl r

source

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

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

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

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

source

@[simp]

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

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

source

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

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

source

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

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

source

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

source

theorem triv_sq_zero_ext.inl_fst_add_inr_snd_eq {R : Type u} {M : Type v} [add_zero_class R] [add_zero_class M] (x : triv_sq_zero_ext R M) :

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

source

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.

source

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.

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

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

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

source

@[protected, 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 = {one := (1, 0)}

source

@[protected, instance]

def triv_sq_zero_ext.has_mul {R : Type u} {M : Type v} [has_mul R] [has_add M] [has_smul R M] [has_smul Rᵐᵒᵖ M] :

has_mul (triv_sq_zero_ext R M)

Equations

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

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.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

source

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

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

@[simp]

theorem triv_sq_zero_ext.inl_mul {R : Type u} (M : Type v) [monoid R] [add_monoid M] [distrib_mul_action R 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] [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

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

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

source

theorem triv_sq_zero_ext.inl_mul_inr {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R 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] [module Rᵐᵒᵖ M] (r : R) (m : M) :

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

source

@[protected, instance]

def triv_sq_zero_ext.mul_one_class {R : Type u} {M : Type v} [monoid R] [add_monoid M] [distrib_mul_action R M] [distrib_mul_action Rᵐᵒᵖ M] :

mul_one_class (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.mul_one_class = {one := 1, mul := has_mul.mul triv_sq_zero_ext.has_mul, one_mul := _, mul_one := _}

source

@[protected, instance]

def triv_sq_zero_ext.add_monoid_with_one {R : Type u} {M : Type v} [add_monoid_with_one R] [add_monoid M] :

add_monoid_with_one (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.add_monoid_with_one = {nat_cast := λ (n : ℕ), triv_sq_zero_ext.inl ↑n, 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 := _}

source

@[simp]

theorem triv_sq_zero_ext.fst_nat_cast {R : Type u} {M : Type v} [add_monoid_with_one R] [add_monoid M] (n : ℕ) :

↑n.fst = ↑n

source

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

source

@[simp]

theorem triv_sq_zero_ext.inl_nat_cast {R : Type u} {M : Type v} [add_monoid_with_one R] [add_monoid M] (n : ℕ) :

triv_sq_zero_ext.inl ↑n = ↑n

source

@[protected, instance]

def triv_sq_zero_ext.add_group_with_one {R : Type u} {M : Type v} [add_group_with_one R] [add_group M] :

add_group_with_one (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.add_group_with_one = {int_cast := λ (z : ℤ), triv_sq_zero_ext.inl ↑z, add := add_group.add triv_sq_zero_ext.add_group, add_assoc := _, zero := add_group.zero triv_sq_zero_ext.add_group, zero_add := _, add_zero := _, nsmul := add_group.nsmul triv_sq_zero_ext.add_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg triv_sq_zero_ext.add_group, sub := add_group.sub triv_sq_zero_ext.add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul triv_sq_zero_ext.add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, nat_cast := add_monoid_with_one.nat_cast triv_sq_zero_ext.add_monoid_with_one, one := add_monoid_with_one.one triv_sq_zero_ext.add_monoid_with_one, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}

source

@[simp]

theorem triv_sq_zero_ext.fst_int_cast {R : Type u} {M : Type v} [add_group_with_one R] [add_group M] (z : ℤ) :

↑z.fst = ↑z

source

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

source

@[simp]

theorem triv_sq_zero_ext.inl_int_cast {R : Type u} {M : Type v} [add_group_with_one R] [add_group M] (z : ℤ) :

triv_sq_zero_ext.inl ↑z = ↑z

source

@[protected, instance]

def triv_sq_zero_ext.non_assoc_semiring {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] [module Rᵐᵒᵖ M] :

non_assoc_semiring (triv_sq_zero_ext R M)

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

source

@[protected, instance]

def triv_sq_zero_ext.non_assoc_ring {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] [module Rᵐᵒᵖ M] :

non_assoc_ring (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.non_assoc_ring = {add := add_group_with_one.add triv_sq_zero_ext.add_group_with_one, add_assoc := _, zero := add_group_with_one.zero triv_sq_zero_ext.add_group_with_one, zero_add := _, add_zero := _, nsmul := add_group_with_one.nsmul triv_sq_zero_ext.add_group_with_one, nsmul_zero' := _, nsmul_succ' := _, neg := add_group_with_one.neg triv_sq_zero_ext.add_group_with_one, sub := add_group_with_one.sub triv_sq_zero_ext.add_group_with_one, sub_eq_add_neg := _, zsmul := add_group_with_one.zsmul triv_sq_zero_ext.add_group_with_one, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := non_assoc_semiring.mul triv_sq_zero_ext.non_assoc_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := add_group_with_one.one triv_sq_zero_ext.add_group_with_one, one_mul := _, mul_one := _, nat_cast := add_group_with_one.nat_cast triv_sq_zero_ext.add_group_with_one, nat_cast_zero := _, nat_cast_succ := _, int_cast := add_group_with_one.int_cast triv_sq_zero_ext.add_group_with_one, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}

source

@[protected, instance]

def triv_sq_zero_ext.nat.has_pow {R : Type u} {M : Type v} [monoid R] [add_monoid M] [distrib_mul_action R M] [distrib_mul_action Rᵐᵒᵖ M] :

has_pow (triv_sq_zero_ext R M) ℕ

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

triv_sq_zero_ext.nat.has_pow = {pow := λ (x : triv_sq_zero_ext R M) (n : ℕ), (x.fst ^ n, (list.map (λ (i : ℕ), x.fst ^ (n.pred - i) • mul_opposite.op (x.fst ^ i) • x.snd) (list.range n)).sum)}

source

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

source

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

source

theorem triv_sq_zero_ext.snd_pow_of_smul_comm {R : Type u} {M : Type v} [monoid R] [add_monoid M] [distrib_mul_action R M] [distrib_mul_action Rᵐᵒᵖ M] [smul_comm_class R Rᵐᵒᵖ M] (x : triv_sq_zero_ext R M) (n : ℕ) (h : mul_opposite.op x.fst • x.snd = x.fst • x.snd) :

(x ^ n).snd = n • x.fst ^ n.pred • x.snd

source

@[simp]

theorem triv_sq_zero_ext.snd_pow {R : Type u} {M : Type v} [comm_monoid R] [add_monoid M] [distrib_mul_action R M] [distrib_mul_action Rᵐᵒᵖ M] [is_central_scalar R M] (x : triv_sq_zero_ext R M) (n : ℕ) :

(x ^ n).snd = n • x.fst ^ n.pred • x.snd

source

@[simp]

theorem triv_sq_zero_ext.inl_pow {R : Type u} {M : Type v} [monoid R] [add_monoid M] [distrib_mul_action R M] [distrib_mul_action Rᵐᵒᵖ M] (r : R) (n : ℕ) :

triv_sq_zero_ext.inl r ^ n = triv_sq_zero_ext.inl (r ^ n)

source

@[protected, instance]

def triv_sq_zero_ext.monoid {R : Type u} {M : Type v} [monoid R] [add_monoid M] [distrib_mul_action R M] [distrib_mul_action Rᵐᵒᵖ M] [smul_comm_class R Rᵐᵒᵖ M] :

monoid (triv_sq_zero_ext R M)

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 := λ (n : ℕ) (x : triv_sq_zero_ext R M), x ^ n, npow_zero' := _, npow_succ' := _}

source

theorem triv_sq_zero_ext.fst_list_prod {R : Type u} {M : Type v} [monoid R] [add_monoid M] [distrib_mul_action R M] [distrib_mul_action Rᵐᵒᵖ M] [smul_comm_class R Rᵐᵒᵖ M] (l : list (triv_sq_zero_ext R M)) :

l.prod.fst = (list.map triv_sq_zero_ext.fst l).prod

source

@[protected, instance]

def triv_sq_zero_ext.semiring {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] [module Rᵐᵒᵖ M] [smul_comm_class R Rᵐᵒᵖ M] :

semiring (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.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 := monoid.mul triv_sq_zero_ext.monoid, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := monoid.one triv_sq_zero_ext.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 := monoid.npow triv_sq_zero_ext.monoid, npow_zero' := _, npow_succ' := _}

source

theorem triv_sq_zero_ext.snd_list_prod {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M] [module Rᵐᵒᵖ M] [smul_comm_class R Rᵐᵒᵖ M] (l : list (triv_sq_zero_ext R M)) :

l.prod.snd = (list.map (λ (x : ℕ × triv_sq_zero_ext R M), (list.take x.fst (list.map triv_sq_zero_ext.fst l)).prod • mul_opposite.op (list.drop x.fst.succ (list.map triv_sq_zero_ext.fst l)).prod • x.snd.snd) l.enum).sum

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$.

source

@[protected, instance]

def triv_sq_zero_ext.ring {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] [module Rᵐᵒᵖ M] [smul_comm_class R Rᵐᵒᵖ M] :

ring (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.ring = {add := semiring.add triv_sq_zero_ext.semiring, add_assoc := _, zero := semiring.zero triv_sq_zero_ext.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul triv_sq_zero_ext.semiring, nsmul_zero' := _, nsmul_succ' := _, neg := non_assoc_ring.neg triv_sq_zero_ext.non_assoc_ring, sub := non_assoc_ring.sub triv_sq_zero_ext.non_assoc_ring, sub_eq_add_neg := _, zsmul := non_assoc_ring.zsmul triv_sq_zero_ext.non_assoc_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := non_assoc_ring.int_cast triv_sq_zero_ext.non_assoc_ring, nat_cast := semiring.nat_cast triv_sq_zero_ext.semiring, one := semiring.one triv_sq_zero_ext.semiring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := semiring.mul triv_sq_zero_ext.semiring, mul_assoc := _, one_mul := _, mul_one := _, npow := semiring.npow triv_sq_zero_ext.semiring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}

source

@[protected, instance]

def triv_sq_zero_ext.comm_monoid {R : Type u} {M : Type v} [comm_monoid R] [add_comm_monoid M] [distrib_mul_action R M] [distrib_mul_action Rᵐᵒᵖ M] [is_central_scalar R M] :

comm_monoid (triv_sq_zero_ext R M)

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

source

@[protected, instance]

def triv_sq_zero_ext.comm_semiring {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] [module Rᵐᵒᵖ M] [is_central_scalar R M] :

comm_semiring (triv_sq_zero_ext R M)

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

source

@[protected, instance]

def triv_sq_zero_ext.comm_ring {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] [module Rᵐᵒᵖ M] [is_central_scalar R M] :

comm_ring (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.comm_ring = {add := non_assoc_ring.add triv_sq_zero_ext.non_assoc_ring, add_assoc := _, zero := non_assoc_ring.zero triv_sq_zero_ext.non_assoc_ring, zero_add := _, add_zero := _, nsmul := non_assoc_ring.nsmul triv_sq_zero_ext.non_assoc_ring, nsmul_zero' := _, nsmul_succ' := _, neg := non_assoc_ring.neg triv_sq_zero_ext.non_assoc_ring, sub := non_assoc_ring.sub triv_sq_zero_ext.non_assoc_ring, sub_eq_add_neg := _, zsmul := non_assoc_ring.zsmul triv_sq_zero_ext.non_assoc_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := non_assoc_ring.int_cast triv_sq_zero_ext.non_assoc_ring, nat_cast := non_assoc_ring.nat_cast triv_sq_zero_ext.non_assoc_ring, one := non_assoc_ring.one triv_sq_zero_ext.non_assoc_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := non_assoc_ring.mul triv_sq_zero_ext.non_assoc_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := comm_semiring.npow triv_sq_zero_ext.comm_semiring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

source

@[simp]

theorem triv_sq_zero_ext.inl_hom_apply (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [module R 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) [semiring R] [add_comm_monoid M] [module R 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

@[protected, instance]

def triv_sq_zero_ext.algebra' (S : Type u_1) (R : Type u) (M : Type v) [comm_semiring S] [semiring R] [add_comm_monoid M] [algebra S R] [module S M] [module R M] [module Rᵐᵒᵖ M] [smul_comm_class R Rᵐᵒᵖ M] [is_scalar_tower S R M] [is_scalar_tower S Rᵐᵒᵖ M] :

algebra S (triv_sq_zero_ext R M)

Equations

triv_sq_zero_ext.algebra' S R M = {to_has_smul := {smul := has_smul.smul triv_sq_zero_ext.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' := _}

source

@[protected, instance]

def triv_sq_zero_ext.algebra (R' : Type u) (M : Type v) [comm_semiring R'] [add_comm_monoid M] [module R' M] [module R'ᵐᵒᵖ M] [is_central_scalar R' M] :

algebra R' (triv_sq_zero_ext R' M)

Equations

triv_sq_zero_ext.algebra R' M = triv_sq_zero_ext.algebra' R' R' M

source

theorem triv_sq_zero_ext.algebra_map_eq_inl (R' : Type u) (M : Type v) [comm_semiring R'] [add_comm_monoid M] [module R' M] [module R'ᵐᵒᵖ M] [is_central_scalar R' M] :

⇑(algebra_map R' (triv_sq_zero_ext R' M)) = triv_sq_zero_ext.inl

source

theorem triv_sq_zero_ext.algebra_map_eq_inl_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] :

algebra_map R' (triv_sq_zero_ext R' M) = triv_sq_zero_ext.inl_hom R' M

source

theorem triv_sq_zero_ext.algebra_map_eq_inl' (S : Type u_1) (R : Type u) (M : Type v) [comm_semiring S] [semiring R] [add_comm_monoid M] [algebra S R] [module S M] [module R M] [module Rᵐᵒᵖ M] [smul_comm_class R Rᵐᵒᵖ M] [is_scalar_tower S R M] [is_scalar_tower S Rᵐᵒᵖ M] (s : S) :

⇑(algebra_map S (triv_sq_zero_ext R M)) s = triv_sq_zero_ext.inl (⇑(algebra_map S R) s)

source

@[simp]

theorem triv_sq_zero_ext.fst_hom_apply (S : Type u_1) (R : Type u) (M : Type v) [comm_semiring S] [semiring R] [add_comm_monoid M] [algebra S R] [module S M] [module R M] [module Rᵐᵒᵖ M] [smul_comm_class R Rᵐᵒᵖ M] [is_scalar_tower S R M] [is_scalar_tower S Rᵐᵒᵖ M] (x : triv_sq_zero_ext R M) :

⇑(triv_sq_zero_ext.fst_hom S R M) x = x.fst

source

def triv_sq_zero_ext.fst_hom (S : Type u_1) (R : Type u) (M : Type v) [comm_semiring S] [semiring R] [add_comm_monoid M] [algebra S R] [module S M] [module R M] [module Rᵐᵒᵖ M] [smul_comm_class R Rᵐᵒᵖ M] [is_scalar_tower S R M] [is_scalar_tower S Rᵐᵒᵖ M] :

triv_sq_zero_ext R M →ₐ[S] R

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

Equations

triv_sq_zero_ext.fst_hom S R M = {to_fun := triv_sq_zero_ext.fst M, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

source

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

source

@[ext]

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 : f.to_linear_map.comp (triv_sq_zero_ext.inr_hom R' M) = g.to_linear_map.comp (triv_sq_zero_ext.inr_hom R' M)) :

f = g

source

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

triv_sq_zero_ext R' M →ₐ[R'] A

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' R' M).to_linear_map + f.comp (triv_sq_zero_ext.snd_hom R' M)) _ _

source

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

⇑(triv_sq_zero_ext.lift_aux f hf) (triv_sq_zero_ext.inr m) = ⇑f m

source

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

(triv_sq_zero_ext.lift_aux f hf).to_linear_map.comp (triv_sq_zero_ext.inr_hom R' M) = f

source

@[simp]

theorem triv_sq_zero_ext.lift_aux_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] :

triv_sq_zero_ext.lift_aux (triv_sq_zero_ext.inr_hom R' M) _ = alg_hom.id R' (triv_sq_zero_ext R' M)

source

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