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 #
triv_sq_zero_ext.inl,triv_sq_zero_ext.inr: the canonical inclusions intotriv_sq_zero_ext R M.triv_sq_zero_ext.fst,triv_sq_zero_ext.snd: the canonical projections fromtriv_sq_zero_ext R M.triv_sq_zero_ext.algebra: the associatedR-algebra structure.triv_sq_zero_ext.lift: the universal property of the trivial square-zero extension; algebra morphismstriv_sq_zero_ext R M →ₐ[R] Aare uniquely defined by linear mapsM →ₗ[R] Afor which the product of any two elements in the range is zero.
"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)
The canonical inclusion R → triv_sq_zero_ext R M.
Equations
- triv_sq_zero_ext.inl r = (r, 0)
The canonical inclusion M → triv_sq_zero_ext R M.
Equations
- triv_sq_zero_ext.inr m = (0, m)
The canonical projection triv_sq_zero_ext R M → R.
The canonical projection triv_sq_zero_ext 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) :
(triv_sq_zero_ext.inl r).fst = r
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[protected, instance]
@[protected, instance]
def
triv_sq_zero_ext.add_zero_class
{R : Type u}
{M : Type v}
[add_zero_class R]
[add_zero_class M] :
@[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
@[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
@[protected, instance]
def
triv_sq_zero_ext.add_comm_semigroup
{R : Type u}
{M : Type v}
[add_comm_semigroup R]
[add_comm_semigroup M] :
@[protected, instance]
def
triv_sq_zero_ext.add_comm_monoid
{R : Type u}
{M : Type v}
[add_comm_monoid R]
[add_comm_monoid M] :
@[protected, instance]
def
triv_sq_zero_ext.add_comm_group
{R : Type u}
{M : Type v}
[add_comm_group R]
[add_comm_group M] :
@[protected, instance]
def
triv_sq_zero_ext.has_scalar
{S : Type u_2}
{R : Type u}
{M : Type v}
[has_scalar S R]
[has_scalar S M] :
has_scalar S (triv_sq_zero_ext R 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_scalar T R]
[has_scalar T M]
[has_scalar S R]
[has_scalar S M]
[has_scalar 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)
@[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_scalar T R]
[has_scalar T M]
[has_scalar S R]
[has_scalar 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)
@[protected, instance]
def
triv_sq_zero_ext.is_central_scalar
{S : Type u_2}
{R : Type u}
{M : Type v}
[has_scalar S R]
[has_scalar S M]
[has_scalar Sᵐᵒᵖ R]
[has_scalar Sᵐᵒᵖ M]
[is_central_scalar S R]
[is_central_scalar S M] :
is_central_scalar S (triv_sq_zero_ext R 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] :
mul_action S (triv_sq_zero_ext R M)
Equations
@[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)
@[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
@[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) :
@[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) :
@[simp]
theorem
triv_sq_zero_ext.fst_smul
{S : Type u_2}
{R : Type u}
{M : Type v}
[has_scalar S R]
[has_scalar S M]
(s : S)
(x : triv_sq_zero_ext R M) :
@[simp]
theorem
triv_sq_zero_ext.snd_smul
{S : Type u_2}
{R : Type u}
{M : Type v}
[has_scalar S R]
[has_scalar S M]
(s : S)
(x : triv_sq_zero_ext R M) :
@[simp]
@[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₂
@[simp]
@[simp]
theorem
triv_sq_zero_ext.inl_smul
{S : Type u_2}
{R : Type u}
(M : Type v)
[monoid S]
[add_monoid M]
[has_scalar 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
@[simp]
@[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₂
@[simp]
@[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_scalar S M]
(r : S)
(m : M) :
triv_sq_zero_ext.inr (r • m) = r • triv_sq_zero_ext.inr m
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) :
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] :
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' := _}
@[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
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' := _}
@[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 #
@[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)}
@[protected, 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)
@[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) :
@[simp]
@[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₂
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₂)
@[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
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)
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)
@[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] :
Equations
- triv_sq_zero_ext.mul_one_class = {one := 1, mul := has_mul.mul triv_sq_zero_ext.has_mul, one_mul := _, mul_one := _}
@[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] :
Equations
- triv_sq_zero_ext.non_assoc_semiring = {add := add_comm_monoid.add triv_sq_zero_ext.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero triv_sq_zero_ext.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul triv_sq_zero_ext.add_comm_monoid, 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 := mul_one_class.one triv_sq_zero_ext.mul_one_class, one_mul := _, mul_one := _}
@[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
- 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 := npow_rec (mul_one_class.to_has_mul (triv_sq_zero_ext R M)), npow_zero' := _, npow_succ' := _}
@[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
- 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 := _}
@[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] :
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 := _, npow := comm_monoid.npow triv_sq_zero_ext.comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}
@[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
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
- 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' := _}
@[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
- triv_sq_zero_ext.algebra' S R M = {to_has_scalar := triv_sq_zero_ext.has_scalar smul_with_zero.to_has_scalar, 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' := _}
@[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
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
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
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)
@[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
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' := _}
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) :
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 M).to_linear_map + f.comp (triv_sq_zero_ext.snd_hom R M)) _ _
@[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
@[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
@[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)
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] :
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
- triv_sq_zero_ext.lift = {to_fun := λ (f : {f // ∀ (x y : M), (⇑f x) * ⇑f y = 0}), triv_sq_zero_ext.lift_aux ↑f _, inv_fun := λ (F : triv_sq_zero_ext R M →ₐ[R] A), ⟨F.to_linear_map.comp (triv_sq_zero_ext.inr_hom R M), _⟩, left_inv := _, right_inv := _}
@[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]
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)