# mathlibdocumentation

algebra.algebra.unitization

# Unitization of a non-unital algebra #

Given a non-unital R-algebra A (given via the type classes [non_unital_ring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A A]) we construct the minimal unital R-algebra containing A as an ideal. This object algebra.unitization R A is a type synonym for R × A on which we place a different multiplicative structure, namely, (r₁, a₁) * (r₂, a₂) = (r₁ * r₂, r₁ • a₂ + r₂ • a₁ + a₁ * a₂) where the multiplicative identity is (1, 0).

Note, when A is a unital R-algebra, then unitization R A constructs a new multiplicative identity different from the old one, and so in general unitization R A and A will not be isomorphic even in the unital case. This approach actually has nice functorial properties.

There is a natural coercion from A to unitization R A given by λ a, (0, a), the image of which is a proper ideal (TODO), and when R is a field this ideal is maximal. Moreover, this ideal is always an essential ideal (it has nontrivial intersection with every other nontrivial ideal).

Every non-unital algebra homomorphism from A into a unital R-algebra B has a unique extension to a (unital) algebra homomorphism from unitization R A to B.

## Main definitions #

• unitization R A: the unitization of a non-unital R-algebra A.
• unitization.algebra: the unitization of A as a (unital) R-algebra.
• unitization.coe_non_unital_alg_hom: coercion as a non-unital algebra homomorphism.
• non_unital_alg_hom.to_alg_hom φ: the extension of a non-unital algebra homomorphism φ : A → B into a unital R-algebra B to an algebra homomorphism unitization R A →ₐ[R] B.

## Main results #

• non_unital_alg_hom.to_alg_hom_unique: the extension is unique

## TODO #

• prove the unitization operation is a functor between the appropriate categories
• prove the image of the coercion is an essential ideal, maximal if scalars are a field.
def unitization (R : Type u_1) (A : Type u_2) :
Type (max u_1 u_2)

The minimal unitization of a non-unital R-algebra A. This is just a type synonym for R × A.

Equations
Instances for unitization
def unitization.inl {R : Type u_1} {A : Type u_2} [has_zero A] (r : R) :
A

The canonical inclusion R → unitization R A.

Equations
• = (r, 0)
@[protected, instance]
def unitization.has_coe_t {R : Type u_1} {A : Type u_2} [has_zero R] :
A)

The canonical inclusion A → unitization R A.

Equations
def unitization.fst {R : Type u_1} {A : Type u_2} (x : A) :
R

The canonical projection unitization R A → R.

Equations
def unitization.snd {R : Type u_1} {A : Type u_2} (x : A) :
A

The canonical projection unitization R A → A.

Equations
@[ext]
theorem unitization.ext {R : Type u_1} {A : Type u_2} {x y : A} (h1 : x.fst = y.fst) (h2 : x.snd = y.snd) :
x = y
@[simp]
theorem unitization.fst_inl {R : Type u_1} (A : Type u_2) [has_zero A] (r : R) :
.fst = r
@[simp]
theorem unitization.snd_inl {R : Type u_1} (A : Type u_2) [has_zero A] (r : R) :
.snd = 0
@[simp]
theorem unitization.fst_coe (R : Type u_1) {A : Type u_2} [has_zero R] (a : A) :
a.fst = 0
@[simp]
theorem unitization.snd_coe (R : Type u_1) {A : Type u_2} [has_zero R] (a : A) :
a.snd = a
theorem unitization.inl_injective {R : Type u_1} {A : Type u_2} [has_zero A] :
theorem unitization.coe_injective {R : Type u_1} {A : Type u_2} [has_zero R] :

### Structures inherited from prod#

Additive operators and scalar multiplication operate elementwise.

@[protected, instance]
def unitization.inhabited {R : Type u_3} {A : Type u_4} [inhabited R] [inhabited A] :
Equations
@[protected, instance]
def unitization.has_zero {R : Type u_3} {A : Type u_4} [has_zero R] [has_zero A] :
Equations
@[protected, instance]
def unitization.has_add {R : Type u_3} {A : Type u_4} [has_add R] [has_add A] :
Equations
@[protected, instance]
def unitization.has_neg {R : Type u_3} {A : Type u_4} [has_neg R] [has_neg A] :
Equations
@[protected, instance]
def unitization.add_semigroup {R : Type u_3} {A : Type u_4}  :
Equations
@[protected, instance]
def unitization.add_zero_class {R : Type u_3} {A : Type u_4}  :
Equations
@[protected, instance]
def unitization.add_monoid {R : Type u_3} {A : Type u_4} [add_monoid R] [add_monoid A] :
Equations
@[protected, instance]
def unitization.add_group {R : Type u_3} {A : Type u_4} [add_group R] [add_group A] :
Equations
@[protected, instance]
def unitization.add_comm_semigroup {R : Type u_3} {A : Type u_4}  :
Equations
@[protected, instance]
def unitization.add_comm_monoid {R : Type u_3} {A : Type u_4}  :
Equations
@[protected, instance]
def unitization.add_comm_group {R : Type u_3} {A : Type u_4}  :
Equations
@[protected, instance]
def unitization.has_smul {S : Type u_2} {R : Type u_3} {A : Type u_4} [ R] [ A] :
A)
Equations
@[protected, instance]
def unitization.is_scalar_tower {T : Type u_1} {S : Type u_2} {R : Type u_3} {A : Type u_4} [ R] [ A] [ R] [ A] [ S] [ R] [ A] :
A)
@[protected, instance]
def unitization.smul_comm_class {T : Type u_1} {S : Type u_2} {R : Type u_3} {A : Type u_4} [ R] [ A] [ R] [ A] [ R] [ A] :
A)
@[protected, instance]
def unitization.is_central_scalar {S : Type u_2} {R : Type u_3} {A : Type u_4} [ R] [ A] [ R] [ A] [ R] [ A] :
A)
@[protected, instance]
def unitization.mul_action {S : Type u_2} {R : Type u_3} {A : Type u_4} [monoid S] [ R] [ A] :
A)
Equations
@[protected, instance]
def unitization.distrib_mul_action {S : Type u_2} {R : Type u_3} {A : Type u_4} [monoid S] [add_monoid R] [add_monoid A] [ R] [ A] :
A)
Equations
@[protected, instance]
def unitization.module {S : Type u_2} {R : Type u_3} {A : Type u_4} [semiring S] [ R] [ A] :
A)
Equations
@[simp]
theorem unitization.fst_zero {R : Type u_3} {A : Type u_4} [has_zero R] [has_zero A] :
0.fst = 0
@[simp]
theorem unitization.snd_zero {R : Type u_3} {A : Type u_4} [has_zero R] [has_zero A] :
0.snd = 0
@[simp]
theorem unitization.fst_add {R : Type u_3} {A : Type u_4} [has_add R] [has_add A] (x₁ x₂ : A) :
(x₁ + x₂).fst = x₁.fst + x₂.fst
@[simp]
theorem unitization.snd_add {R : Type u_3} {A : Type u_4} [has_add R] [has_add A] (x₁ x₂ : A) :
(x₁ + x₂).snd = x₁.snd + x₂.snd
@[simp]
theorem unitization.fst_neg {R : Type u_3} {A : Type u_4} [has_neg R] [has_neg A] (x : A) :
(-x).fst = -x.fst
@[simp]
theorem unitization.snd_neg {R : Type u_3} {A : Type u_4} [has_neg R] [has_neg A] (x : A) :
(-x).snd = -x.snd
@[simp]
theorem unitization.fst_smul {S : Type u_2} {R : Type u_3} {A : Type u_4} [ R] [ A] (s : S) (x : A) :
(s x).fst = s x.fst
@[simp]
theorem unitization.snd_smul {S : Type u_2} {R : Type u_3} {A : Type u_4} [ R] [ A] (s : S) (x : A) :
(s x).snd = s x.snd
@[simp]
theorem unitization.inl_zero {R : Type u_3} (A : Type u_4) [has_zero R] [has_zero A] :
@[simp]
theorem unitization.inl_add {R : Type u_3} (A : Type u_4) [has_add R] (r₁ r₂ : R) :
unitization.inl (r₁ + r₂) =
@[simp]
theorem unitization.inl_neg {R : Type u_3} (A : Type u_4) [has_neg R] [add_group A] (r : R) :
@[simp]
theorem unitization.inl_smul {S : Type u_2} {R : Type u_3} (A : Type u_4) [monoid S] [add_monoid A] [ R] [ A] (s : S) (r : R) :
@[simp]
theorem unitization.coe_zero (R : Type u_3) {A : Type u_4} [has_zero R] [has_zero A] :
0 = 0
@[simp]
theorem unitization.coe_add (R : Type u_3) {A : Type u_4} [has_add A] (m₁ m₂ : A) :
(m₁ + m₂) = m₁ + m₂
@[simp]
theorem unitization.coe_neg (R : Type u_3) {A : Type u_4} [add_group R] [has_neg A] (m : A) :
@[simp]
theorem unitization.coe_smul {S : Type u_2} (R : Type u_3) {A : Type u_4} [has_zero R] [has_zero S] [ R] [ A] (r : S) (m : A) :
(r m) = r m
theorem unitization.inl_fst_add_coe_snd_eq {R : Type u_3} {A : Type u_4} (x : A) :
+ (x.snd) = x
theorem unitization.ind {R : Type u_1} {A : Type u_2} {P : A → Prop} (h : ∀ (r : R) (a : A), P + a)) (x : A) :
P x

To show a property hold on all unitization R A it suffices to show it holds on terms of the form inl r + a.

This can be used as induction x using unitization.ind.

theorem unitization.linear_map_ext {S : Type u_2} {R : Type u_3} {A : Type u_4} {N : Type u_1} [semiring S] [ R] [ A] [ N] ⦃f g : A →ₗ[S] N⦄ (hl : ∀ (r : R), f = g ) (hr : ∀ (a : A), f a = g a) :
f = g

This cannot be marked @[ext] as it ends up being used instead of linear_map.prod_ext when working with R × A.

@[simp]
theorem unitization.coe_hom_apply (R : Type u_3) (A : Type u_4) [semiring R] [ A] (ᾰ : A) :
A) =
def unitization.coe_hom (R : Type u_3) (A : Type u_4) [semiring R] [ A] :

The canonical R-linear inclusion A → unitization R A.

Equations
@[simp]
theorem unitization.snd_hom_apply (R : Type u_3) (A : Type u_4) [semiring R] [ A] (x : A) :
A) x = x.snd
def unitization.snd_hom (R : Type u_3) (A : Type u_4) [semiring R] [ A] :
A →ₗ[R] A

The canonical R-linear projection unitization R A → A.

Equations

### Multiplicative structure #

@[protected, instance]
def unitization.has_one {R : Type u_1} {A : Type u_2} [has_one R] [has_zero A] :
Equations
@[protected, instance]
def unitization.has_mul {R : Type u_1} {A : Type u_2} [has_mul R] [has_add A] [has_mul A] [ A] :
Equations
@[simp]
theorem unitization.fst_one {R : Type u_1} {A : Type u_2} [has_one R] [has_zero A] :
1.fst = 1
@[simp]
theorem unitization.snd_one {R : Type u_1} {A : Type u_2} [has_one R] [has_zero A] :
1.snd = 0
@[simp]
theorem unitization.fst_mul {R : Type u_1} {A : Type u_2} [has_mul R] [has_add A] [has_mul A] [ A] (x₁ x₂ : A) :
(x₁ * x₂).fst = x₁.fst * x₂.fst
@[simp]
theorem unitization.snd_mul {R : Type u_1} {A : Type u_2} [has_mul R] [has_add A] [has_mul A] [ A] (x₁ x₂ : A) :
(x₁ * x₂).snd = x₁.fst x₂.snd + x₂.fst x₁.snd + x₁.snd * x₂.snd
@[simp]
theorem unitization.inl_one {R : Type u_1} (A : Type u_2) [has_one R] [has_zero A] :
@[simp]
theorem unitization.inl_mul {R : Type u_1} (A : Type u_2) [monoid R] [ A] (r₁ r₂ : R) :
unitization.inl (r₁ * r₂) =
theorem unitization.inl_mul_inl {R : Type u_1} (A : Type u_2) [monoid R] [ A] (r₁ r₂ : R) :
= unitization.inl (r₁ * r₂)
@[simp]
theorem unitization.coe_mul (R : Type u_1) {A : Type u_2} [semiring R] [has_mul A] [ A] (a₁ a₂ : A) :
(a₁ * a₂) = a₁ * a₂
theorem unitization.inl_mul_coe {R : Type u_1} {A : Type u_2} [semiring R] [ A] (r : R) (a : A) :
= (r a)
theorem unitization.coe_mul_inl {R : Type u_1} {A : Type u_2} [semiring R] [ A] (r : R) (a : A) :
= (r a)
@[protected, instance]
def unitization.mul_one_class {R : Type u_1} {A : Type u_2} [monoid R] [ A] :
Equations
@[protected, instance]
def unitization.non_assoc_semiring {R : Type u_1} {A : Type u_2} [semiring R] [ A] :
Equations
@[protected, instance]
def unitization.monoid {R : Type u_1} {A : Type u_2} [comm_monoid R] [ A] [ A] [ A] :
Equations
@[protected, instance]
def unitization.comm_monoid {R : Type u_1} {A : Type u_2} [comm_monoid R] [ A] [ A] [ A] :
Equations
@[protected, instance]
def unitization.semiring {R : Type u_1} {A : Type u_2} [ A] [ A] [ A] :
Equations
@[protected, instance]
def unitization.comm_semiring {R : Type u_1} {A : Type u_2} [ A] [ A] [ A] :
Equations
@[simp]
theorem unitization.inl_ring_hom_apply (R : Type u_1) (A : Type u_2) [semiring R] [ A] (r : R) :
def unitization.inl_ring_hom (R : Type u_1) (A : Type u_2) [semiring R] [ A] :
R →+* A

The canonical inclusion of rings R →+* unitization R A.

Equations

### Star structure #

@[protected, instance]
def unitization.has_star {R : Type u_1} {A : Type u_2} [has_star R] [has_star A] :
Equations
@[simp]
theorem unitization.fst_star {R : Type u_1} {A : Type u_2} [has_star R] [has_star A] (x : A) :
@[simp]
theorem unitization.snd_star {R : Type u_1} {A : Type u_2} [has_star R] [has_star A] (x : A) :
@[simp]
theorem unitization.inl_star {R : Type u_1} {A : Type u_2} [has_star R] [add_monoid A] (r : R) :
@[simp]
theorem unitization.coe_star {R : Type u_1} {A : Type u_2} [add_monoid R] [has_star A] (a : A) :
@[protected, instance]
def unitization.star_add_monoid {R : Type u_1} {A : Type u_2} [add_monoid R] [add_monoid A]  :
Equations
@[protected, instance]
def unitization.star_module {R : Type u_1} {A : Type u_2} [star_ring R] [ A] [ A] :
A)
@[protected, instance]
def unitization.star_ring {R : Type u_1} {A : Type u_2} [star_ring R] [star_ring A] [ A] [ A] [ A] [ A] :
Equations

### Algebra structure #

@[protected, instance]
def unitization.algebra (S : Type u_1) (R : Type u_2) (A : Type u_3) [ A] [ A] [ A] [ R] [ A] [ A] :
A)
Equations
theorem unitization.algebra_map_eq_inl_comp (S : Type u_1) (R : Type u_2) (A : Type u_3) [ A] [ A] [ A] [ R] [ A] [ A] :
A)) =
theorem unitization.algebra_map_eq_inl_ring_hom_comp (S : Type u_1) (R : Type u_2) (A : Type u_3) [ A] [ A] [ A] [ R] [ A] [ A] :
A) = .comp R)
theorem unitization.algebra_map_eq_inl (R : Type u_2) (A : Type u_3) [ A] [ A] [ A] :
theorem unitization.algebra_map_eq_inl_hom (R : Type u_2) (A : Type u_3) [ A] [ A] [ A] :
A) =
def unitization.fst_hom (R : Type u_2) (A : Type u_3) [ A] [ A] [ A] :
A →ₐ[R] R

The canonical R-algebra projection unitization R A → R.

Equations
@[simp]
theorem unitization.fst_hom_apply (R : Type u_2) (A : Type u_3) [ A] [ A] [ A] (x : A) :
A) x = x.fst
def unitization.coe_non_unital_alg_hom (R : Type u_1) (A : Type u_2) [ A] :

The coercion from a non-unital R-algebra A to its unitization unitization R A realized as a non-unital algebra homomorphism.

Equations
@[simp]
theorem unitization.coe_non_unital_alg_hom_apply (R : Type u_1) (A : Type u_2) [ A] (ᾰ : A) :
theorem unitization.alg_hom_ext {S : Type u_1} {R : Type u_2} {A : Type u_3} [ A] [ A] [ A] {B : Type u_4} [semiring B] [ B] [ R] [ A] [ A] {φ ψ : A →ₐ[S] B} (h : ∀ (a : A), φ a = ψ a) (h' : ∀ (r : R), φ ( A)) r) = ψ ( A)) r)) :
φ = ψ
@[ext]
theorem unitization.alg_hom_ext' {R : Type u_2} {A : Type u_3} [ A] [ A] [ A] {C : Type u_5} [ring C] [ C] {φ ψ : A →ₐ[R] C}  :
φ = ψ
@[simp]
theorem unitization.lift_apply_apply {R : Type u_2} {A : Type u_3} [ A] [ A] [ A] {C : Type u_5} [ring C] [ C] (φ : A →ₙₐ[R] C) (x : A) :
x = C) x.fst + φ x.snd
def unitization.lift {R : Type u_2} {A : Type u_3} [ A] [ A] [ A] {C : Type u_5} [ring C] [ C] :
(A →ₙₐ[R] C) A →ₐ[R] C)

Non-unital algebra homomorphisms from A into a unital R-algebra C lift uniquely to unitization R A →ₐ[R] C. This is the universal property of the unitization.

Equations
theorem unitization.lift_symm_apply {R : Type u_2} {A : Type u_3} [ A] [ A] [ A] {C : Type u_5} [ring C] [ C] (φ : A →ₐ[R] C) (a : A) :