mathlib documentation

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 #

Main results #

TODO #

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

The canonical inclusion R → unitization R A.

Equations
@[protected, instance]
def unitization.has_coe_t {R : Type u_1} {A : Type u_2} [has_zero R] :

The canonical inclusion A → unitization R A.

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

The canonical projection unitization R A → R.

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

The canonical projection unitization R A → A.

Equations
@[ext]
theorem unitization.ext {R : Type u_1} {A : Type u_2} {x y : unitization R 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) :
@[simp]
theorem unitization.snd_inl {R : Type u_1} (A : Type u_2) [has_zero A] (r : R) :
@[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} [add_semigroup R] [add_semigroup A] :
Equations
@[protected, instance]
def unitization.add_zero_class {R : Type u_3} {A : Type u_4} [add_zero_class R] [add_zero_class A] :
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_monoid {R : Type u_3} {A : Type u_4} [add_comm_monoid R] [add_comm_monoid A] :
Equations
@[protected, instance]
def unitization.add_comm_group {R : Type u_3} {A : Type u_4} [add_comm_group R] [add_comm_group A] :
Equations
@[protected, instance]
def unitization.has_scalar {S : Type u_2} {R : Type u_3} {A : Type u_4} [has_scalar S R] [has_scalar S 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} [has_scalar T R] [has_scalar T A] [has_scalar S R] [has_scalar S A] [has_scalar T S] [is_scalar_tower T S R] [is_scalar_tower T S A] :
@[protected, instance]
def unitization.smul_comm_class {T : Type u_1} {S : Type u_2} {R : Type u_3} {A : Type u_4} [has_scalar T R] [has_scalar T A] [has_scalar S R] [has_scalar S A] [smul_comm_class T S R] [smul_comm_class T S A] :
@[protected, instance]
def unitization.is_central_scalar {S : Type u_2} {R : Type u_3} {A : Type u_4} [has_scalar S R] [has_scalar S A] [has_scalar Sᵐᵒᵖ R] [has_scalar Sᵐᵒᵖ A] [is_central_scalar S R] [is_central_scalar S A] :
@[protected, instance]
def unitization.mul_action {S : Type u_2} {R : Type u_3} {A : Type u_4} [monoid S] [mul_action S R] [mul_action S 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] [distrib_mul_action S R] [distrib_mul_action S A] :
Equations
@[protected, instance]
def unitization.module {S : Type u_2} {R : Type u_3} {A : Type u_4} [semiring S] [add_comm_monoid R] [add_comm_monoid A] [module S R] [module S 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₂ : unitization R 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₂ : unitization R 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 : unitization R 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 : unitization R A) :
(-x).snd = -x.snd
@[simp]
theorem unitization.fst_smul {S : Type u_2} {R : Type u_3} {A : Type u_4} [has_scalar S R] [has_scalar S A] (s : S) (x : unitization R A) :
(s x).fst = s x.fst
@[simp]
theorem unitization.snd_smul {S : Type u_2} {R : Type u_3} {A : Type u_4} [has_scalar S R] [has_scalar S A] (s : S) (x : unitization R 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] [add_zero_class A] (r₁ 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] [has_scalar S R] [distrib_mul_action S 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} [add_zero_class R] [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] [smul_with_zero S R] [has_scalar S 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} [add_zero_class R] [add_zero_class A] (x : unitization R A) :
theorem unitization.ind {R : Type u_1} {A : Type u_2} [add_zero_class R] [add_zero_class A] {P : unitization R A → Prop} (h : ∀ (r : R) (a : A), P (unitization.inl r + a)) (x : unitization R 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] [add_comm_monoid R] [add_comm_monoid A] [add_comm_monoid N] [module S R] [module S A] [module S N] ⦃f g : unitization R A →ₗ[S] N⦄ (hl : ∀ (r : R), f (unitization.inl r) = g (unitization.inl r)) (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] [add_comm_monoid A] [module R A] (ᾰ : A) :
def unitization.coe_hom (R : Type u_3) (A : Type u_4) [semiring R] [add_comm_monoid A] [module 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] [add_comm_monoid A] [module R A] (x : unitization R A) :
def unitization.snd_hom (R : Type u_3) (A : Type u_4) [semiring R] [add_comm_monoid A] [module 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] [has_scalar R 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] [has_scalar R A] (x₁ x₂ : unitization R 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] [has_scalar R A] (x₁ x₂ : unitization R 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] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] (r₁ r₂ : R) :
theorem unitization.inl_mul_inl {R : Type u_1} (A : Type u_2) [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] (r₁ r₂ : R) :
@[simp]
theorem unitization.coe_mul (R : Type u_1) {A : Type u_2} [semiring R] [add_comm_monoid A] [has_mul A] [smul_with_zero R A] (a₁ a₂ : A) :
(a₁ * a₂) = a₁ * a₂
theorem unitization.inl_mul_coe {R : Type u_1} {A : Type u_2} [semiring R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] (r : R) (a : A) :
theorem unitization.coe_mul_inl {R : Type u_1} {A : Type u_2} [semiring R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] (r : R) (a : A) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem unitization.inl_ring_hom_apply (R : Type u_1) (A : Type u_2) [semiring R] [non_unital_semiring A] [module R A] (r : R) :
def unitization.inl_ring_hom (R : Type u_1) (A : Type u_2) [semiring R] [non_unital_semiring A] [module 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 : unitization R A) :
@[simp]
theorem unitization.snd_star {R : Type u_1} {A : Type u_2} [has_star R] [has_star A] (x : unitization R A) :
@[simp]
theorem unitization.inl_star {R : Type u_1} {A : Type u_2} [has_star R] [add_monoid A] [star_add_monoid A] (r : R) :
@[simp]
theorem unitization.coe_star {R : Type u_1} {A : Type u_2} [add_monoid R] [star_add_monoid R] [has_star A] (a : A) :
@[protected, instance]
def unitization.star_module {R : Type u_1} {A : Type u_2} [comm_semiring R] [star_ring R] [add_comm_monoid A] [star_add_monoid A] [module R A] [star_module R A] :

Algebra structure #

@[protected, instance]
def unitization.algebra (S : Type u_1) (R : Type u_2) (A : Type u_3) [comm_semiring S] [comm_semiring R] [non_unital_semiring A] [module R A] [is_scalar_tower R A A] [smul_comm_class R A A] [algebra S R] [distrib_mul_action S A] [is_scalar_tower S R A] :
Equations
def unitization.fst_hom (R : Type u_2) (A : Type u_3) [comm_semiring R] [non_unital_semiring A] [module R A] [is_scalar_tower R A A] [smul_comm_class R A A] :

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

Equations
@[simp]
theorem unitization.fst_hom_apply (R : Type u_2) (A : Type u_3) [comm_semiring R] [non_unital_semiring A] [module R A] [is_scalar_tower R A A] [smul_comm_class R A A] (x : unitization R A) :
def unitization.coe_non_unital_alg_hom (R : Type u_1) (A : Type u_2) [comm_semiring R] [non_unital_semiring A] [module R 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) [comm_semiring R] [non_unital_semiring A] [module R A] (ᾰ : A) :
theorem unitization.alg_hom_ext {S : Type u_1} {R : Type u_2} {A : Type u_3} [comm_semiring S] [comm_semiring R] [non_unital_semiring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A A] {B : Type u_4} [semiring B] [algebra S B] [algebra S R] [distrib_mul_action S A] [is_scalar_tower S R A] {φ ψ : unitization R A →ₐ[S] B} (h : ∀ (a : A), φ a = ψ a) (h' : ∀ (r : R), φ ((algebra_map R (unitization R A)) r) = ψ ((algebra_map R (unitization R A)) r)) :
φ = ψ
@[simp]
theorem unitization.lift_apply_apply {R : Type u_2} {A : Type u_3} [comm_semiring R] [non_unital_semiring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A A] {C : Type u_5} [ring C] [algebra R C] (φ : A →ₙₐ[R] C) (x : unitization R A) :
def unitization.lift {R : Type u_2} {A : Type u_3} [comm_semiring R] [non_unital_semiring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A A] {C : Type u_5} [ring C] [algebra 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} [comm_semiring R] [non_unital_semiring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A A] {C : Type u_5} [ring C] [algebra R C] (φ : unitization R A →ₐ[R] C) (a : A) :