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 #

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]
def triv_sq_zero_ext.inhabited {R : Type u} {M : Type v} [inhabited R] [inhabited M] :
Equations
@[protected, instance]
def triv_sq_zero_ext.has_zero {R : Type u} {M : Type v} [has_zero R] [has_zero M] :
Equations
@[protected, instance]
def triv_sq_zero_ext.has_add {R : Type u} {M : Type v} [has_add R] [has_add M] :
Equations
@[protected, instance]
def triv_sq_zero_ext.has_neg {R : Type u} {M : Type v} [has_neg R] [has_neg M] :
Equations
@[protected, instance]
def triv_sq_zero_ext.add_monoid {R : Type u} {M : Type v} [add_monoid R] [add_monoid M] :
Equations
@[protected, instance]
def triv_sq_zero_ext.add_group {R : Type u} {M : Type v} [add_group R] [add_group M] :
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]
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] :
@[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_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
@[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_neg {R : Type u} (M : Type v) [has_neg R] [add_group M] (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) :
@[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_neg (R : Type u) {M : Type v} [add_group R] [has_neg 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.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.

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

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

Multiplicative structure #

@[protected, instance]
def triv_sq_zero_ext.has_one {R : Type u} {M : Type v} [has_one R] [has_zero M] :
Equations
@[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] :
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] (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] (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_one {R : Type u} (M : Type v) [has_one R] [has_zero M] :
@[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) :
@[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) :
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) :
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) :
@[protected, instance]
Equations
@[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) :
def triv_sq_zero_ext.inl_hom (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M] [module R M] :

The canonical inclusion of rings R → triv_sq_zero_ext R M.

Equations
@[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] :
Equations
@[protected, instance]
def triv_sq_zero_ext.algebra (R : Type u) (M : Type v) [comm_semiring R] [add_comm_monoid M] [module R M] :
Equations
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) :
@[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) :
def triv_sq_zero_ext.fst_hom (R : Type u) (M : Type v) [comm_semiring R] [add_comm_monoid M] [module R M] :

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

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] {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] {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] {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] {A : Type u_2} [semiring A] [algebra R A] (f : {f // ∀ (x y : M), f x * f y = 0}) :
@[simp]