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.

Main definitions #

source
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
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
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
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
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
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_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

Structures inherited from prod #

Additive operators and scalar multiplication operate elementwise.

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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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_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
@[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] [add_group M] (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
@[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} [add_group 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_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.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
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
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

Multiplicative structure #

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
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_mul (triv_sq_zero_ext R M)
Equations
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] (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] (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_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] (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
@[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
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
@[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] :
mul_one_class (triv_sq_zero_ext R M)
Equations
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
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] :
non_assoc_semiring (triv_sq_zero_ext R M)
Equations
source
@[protected, 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
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] :
comm_monoid (triv_sq_zero_ext R M)
Equations
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] :
comm_semiring (triv_sq_zero_ext R M)
Equations
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] (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] :
R →+* triv_sq_zero_ext R M

The canonical inclusion of rings R → triv_sq_zero_ext R M.

Equations
source
@[protected, instance]
def triv_sq_zero_ext.algebra' (S : Type u_1) (R : Type u) (M : Type v) [comm_semiring S] [comm_semiring R] [add_comm_monoid M] [algebra S R] [module S M] [module R M] [is_scalar_tower S R M] :
algebra S (triv_sq_zero_ext R M)
Equations
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] :
algebra R (triv_sq_zero_ext R M)
Equations
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] :
⇑(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] :
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] [comm_semiring R] [add_comm_monoid M] [algebra S R] [module S M] [module 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 (R : Type u) (M : Type v) [comm_semiring R] [add_comm_monoid M] [module R M] (x : triv_sq_zero_ext R M) :
⇑(triv_sq_zero_ext.fst_hom R M) x = x.fst
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
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] {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] {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] {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
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] {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] {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] :
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] {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
source
@[simp]
theorem triv_sq_zero_ext.lift_apply {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {A : Type u_2} [semiring A] [algebra R A] (f : {f // ∀ (x y : M), ⇑f x * ⇑f y = 0}) :
⇑triv_sq_zero_ext.lift f = triv_sq_zero_ext.lift_aux ↑f _
source
@[simp]
theorem triv_sq_zero_ext.lift_symm_apply_coe {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M] {A : Type u_2} [semiring A] [algebra R A] (F : triv_sq_zero_ext R M →ₐ[R] A) :
↑(⇑(triv_sq_zero_ext.lift.symm) F) = F.to_linear_map.comp (triv_sq_zero_ext.inr_hom R M)