# Unitization of a non-unital algebra #

Given a non-unital R-algebra A (given via the type classes [NonUnitalRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A]) we construct the minimal unital R-algebra containing A as an ideal. This object 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 fun 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.coeNonUnitalAlgHom: coercion as a non-unital algebra homomorphism.
• NonUnitalAlgHom.toAlgHom φ: 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.
• Unitization.lift: the universal property of the unitization, the extension NonUnitalAlgHom.toAlgHom actually implements an equivalence (A →ₙₐ[R] B) ≃ (Unitization R A ≃ₐ[R] B)

## Main results #

• AlgHom.ext': an extensionality lemma for algebra homomorphisms whose domain is Unitization R A; it suffices that they agree on A.

## 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
def Unitization.inl {R : Type u_1} {A : Type u_2} [Zero A] (r : R) :

The canonical inclusion R → Unitization R A.

Equations
• = (r, 0)
Instances For
def Unitization.inr {R : Type u_1} {A : Type u_2} [Zero R] (a : A) :

The canonical inclusion A → Unitization R A.

Equations
• a = (0, a)
Instances For
instance Unitization.instCoeTCOfZero {R : Type u_1} {A : Type u_2} [Zero R] :
CoeTC A ()
Equations
• Unitization.instCoeTCOfZero = { coe := Unitization.inr }
def Unitization.fst {R : Type u_1} {A : Type u_2} (x : ) :
R

The canonical projection Unitization R A → R.

Equations
• x.fst = x.1
Instances For
def Unitization.snd {R : Type u_1} {A : Type u_2} (x : ) :
A

The canonical projection Unitization R A → A.

Equations
• x.snd = x.2
Instances For
theorem Unitization.ext {R : Type u_1} {A : Type u_2} {x : } {y : } (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) [Zero A] (r : R) :
().fst = r
@[simp]
theorem Unitization.snd_inl {R : Type u_1} (A : Type u_2) [Zero A] (r : R) :
().snd = 0
@[simp]
theorem Unitization.fst_inr (R : Type u_1) {A : Type u_2} [Zero R] (a : A) :
(a).fst = 0
@[simp]
theorem Unitization.snd_inr (R : Type u_1) {A : Type u_2} [Zero R] (a : A) :
(a).snd = a
theorem Unitization.inl_injective {R : Type u_1} {A : Type u_2} [Zero A] :
Function.Injective Unitization.inl
theorem Unitization.inr_injective {R : Type u_1} {A : Type u_2} [Zero R] :
Function.Injective Unitization.inr
instance Unitization.instNontrivialLeft {𝕜 : Type u_3} {A : Type u_4} [] [] :
Equations
• =
instance Unitization.instNontrivialRight {𝕜 : Type u_3} {A : Type u_4} [] [] :
Equations
• =

### Structures inherited from Prod#

Additive operators and scalar multiplication operate elementwise.

instance Unitization.instCanLift {R : Type u_3} {A : Type u_4} [Zero R] :
CanLift () A Unitization.inr fun (x : ) => x.fst = 0
Equations
• =
instance Unitization.instInhabited {R : Type u_3} {A : Type u_4} [] [] :
Equations
• Unitization.instInhabited = instInhabitedProd
instance Unitization.instZero {R : Type u_3} {A : Type u_4} [Zero R] [Zero A] :
Zero ()
Equations
• Unitization.instZero = Prod.instZero
instance Unitization.instAdd {R : Type u_3} {A : Type u_4} [Add R] [Add A] :
Add ()
Equations
• Unitization.instAdd = Prod.instAdd
instance Unitization.instNeg {R : Type u_3} {A : Type u_4} [Neg R] [Neg A] :
Neg ()
Equations
• Unitization.instNeg = Prod.instNeg
instance Unitization.instAddSemigroup {R : Type u_3} {A : Type u_4} [] [] :
Equations
• Unitization.instAddSemigroup = Prod.instAddSemigroup
instance Unitization.instAddZeroClass {R : Type u_3} {A : Type u_4} [] [] :
Equations
• Unitization.instAddZeroClass = Prod.instAddZeroClass
instance Unitization.instAddMonoid {R : Type u_3} {A : Type u_4} [] [] :
Equations
• Unitization.instAddMonoid = Prod.instAddMonoid
instance Unitization.instAddGroup {R : Type u_3} {A : Type u_4} [] [] :
Equations
• Unitization.instAddGroup = Prod.instAddGroup
instance Unitization.instAddCommSemigroup {R : Type u_3} {A : Type u_4} [] [] :
Equations
• Unitization.instAddCommSemigroup = Prod.instAddCommSemigroup
instance Unitization.instAddCommMonoid {R : Type u_3} {A : Type u_4} [] [] :
Equations
• Unitization.instAddCommMonoid = Prod.instAddCommMonoid
instance Unitization.instAddCommGroup {R : Type u_3} {A : Type u_4} [] [] :
Equations
• Unitization.instAddCommGroup = Prod.instAddCommGroup
instance Unitization.instSMul {S : Type u_2} {R : Type u_3} {A : Type u_4} [SMul S R] [SMul S A] :
SMul S ()
Equations
• Unitization.instSMul = Prod.smul
instance Unitization.instIsScalarTower {T : Type u_1} {S : Type u_2} {R : Type u_3} {A : Type u_4} [SMul T R] [SMul T A] [SMul S R] [SMul S A] [SMul T S] [] [] :
Equations
• =
instance Unitization.instSMulCommClass {T : Type u_1} {S : Type u_2} {R : Type u_3} {A : Type u_4} [SMul T R] [SMul T A] [SMul S R] [SMul S A] [] [] :
Equations
• =
instance Unitization.instIsCentralScalar {S : Type u_2} {R : Type u_3} {A : Type u_4} [SMul S R] [SMul S A] [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ A] [] [] :
Equations
• =
instance Unitization.instMulAction {S : Type u_2} {R : Type u_3} {A : Type u_4} [] [] [] :
Equations
• Unitization.instMulAction = Prod.mulAction
instance Unitization.instDistribMulAction {S : Type u_2} {R : Type u_3} {A : Type u_4} [] [] [] [] [] :
Equations
• Unitization.instDistribMulAction = Prod.distribMulAction
instance Unitization.instModule {S : Type u_2} {R : Type u_3} {A : Type u_4} [] [] [] [Module S R] [Module S A] :
Module S ()
Equations
• Unitization.instModule = Prod.instModule
def Unitization.addEquiv (R : Type u_3) (A : Type u_4) [Add R] [Add A] :
≃+ R × A

The identity map between Unitization R A and R × A as an AddEquiv.

Equations
Instances For
@[simp]
theorem Unitization.fst_zero {R : Type u_3} {A : Type u_4} [Zero R] [Zero A] :
@[simp]
theorem Unitization.snd_zero {R : Type u_3} {A : Type u_4} [Zero R] [Zero A] :
@[simp]
theorem Unitization.fst_add {R : Type u_3} {A : Type u_4} [Add R] [Add A] (x₁ : ) (x₂ : ) :
(x₁ + x₂).fst = x₁.fst + x₂.fst
@[simp]
theorem Unitization.snd_add {R : Type u_3} {A : Type u_4} [Add R] [Add A] (x₁ : ) (x₂ : ) :
(x₁ + x₂).snd = x₁.snd + x₂.snd
@[simp]
theorem Unitization.fst_neg {R : Type u_3} {A : Type u_4} [Neg R] [Neg A] (x : ) :
(-x).fst = -x.fst
@[simp]
theorem Unitization.snd_neg {R : Type u_3} {A : Type u_4} [Neg R] [Neg A] (x : ) :
(-x).snd = -x.snd
@[simp]
theorem Unitization.fst_smul {S : Type u_2} {R : Type u_3} {A : Type u_4} [SMul S R] [SMul S A] (s : S) (x : ) :
(s x).fst = s x.fst
@[simp]
theorem Unitization.snd_smul {S : Type u_2} {R : Type u_3} {A : Type u_4} [SMul S R] [SMul S A] (s : S) (x : ) :
(s x).snd = s x.snd
@[simp]
theorem Unitization.inl_zero {R : Type u_3} (A : Type u_4) [Zero R] [Zero A] :
@[simp]
theorem Unitization.inl_add {R : Type u_3} (A : Type u_4) [Add R] [] (r₁ : R) (r₂ : R) :
Unitization.inl (r₁ + r₂) =
@[simp]
theorem Unitization.inl_neg {R : Type u_3} (A : Type u_4) [Neg R] [] (r : R) :
@[simp]
theorem Unitization.inl_smul {S : Type u_2} {R : Type u_3} (A : Type u_4) [] [] [SMul S R] [] (s : S) (r : R) :
@[simp]
theorem Unitization.inr_zero (R : Type u_3) {A : Type u_4} [Zero R] [Zero A] :
0 = 0
@[simp]
theorem Unitization.inr_add (R : Type u_3) {A : Type u_4} [] [Add A] (m₁ : A) (m₂ : A) :
(m₁ + m₂) = m₁ + m₂
@[simp]
theorem Unitization.inr_neg (R : Type u_3) {A : Type u_4} [] [Neg A] (m : A) :
(-m) = -m
@[simp]
theorem Unitization.inr_smul {S : Type u_2} (R : Type u_3) {A : Type u_4} [Zero R] [Zero S] [] [SMul S A] (r : S) (m : A) :
(r m) = r m
theorem Unitization.inl_fst_add_inr_snd_eq {R : Type u_3} {A : Type u_4} [] [] (x : ) :
Unitization.inl x.fst + x.snd = x
theorem Unitization.ind {R : Type u_5} {A : Type u_6} [] [] {P : Prop} (h : ∀ (r : R) (a : A), P ( + a)) (x : ) :
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.linearMap_ext {S : Type u_2} {R : Type u_3} {A : Type u_4} {N : Type u_5} [] [] [] [] [Module S R] [Module S A] [Module S N] ⦃f : →ₗ[S] N ⦃g : →ₗ[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 LinearMap.prod_ext when working with R × A.

@[simp]
theorem Unitization.inrHom_apply (R : Type u_3) (A : Type u_4) [] [] [Module R A] (a : A) :
() a = a
def Unitization.inrHom (R : Type u_3) (A : Type u_4) [] [] [Module R A] :

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

Equations
• = let __src := ; { toFun := Unitization.inr, map_add' := , map_smul' := }
Instances For
@[simp]
theorem Unitization.sndHom_apply (R : Type u_3) (A : Type u_4) [] [] [Module R A] (x : ) :
() x = x.snd
def Unitization.sndHom (R : Type u_3) (A : Type u_4) [] [] [Module R A] :

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

Equations
• = let __src := ; { toFun := Unitization.snd, map_add' := , map_smul' := }
Instances For

### Multiplicative structure #

instance Unitization.instOne {R : Type u_1} {A : Type u_2} [One R] [Zero A] :
One ()
Equations
• Unitization.instOne = { one := (1, 0) }
instance Unitization.instMul {R : Type u_1} {A : Type u_2} [Mul R] [Add A] [Mul A] [SMul R A] :
Mul ()
Equations
• Unitization.instMul = { mul := fun (x y : ) => (x.1 * y.1, x.1 y.2 + y.1 x.2 + x.2 * y.2) }
@[simp]
theorem Unitization.fst_one {R : Type u_1} {A : Type u_2} [One R] [Zero A] :
@[simp]
theorem Unitization.snd_one {R : Type u_1} {A : Type u_2} [One R] [Zero A] :
@[simp]
theorem Unitization.fst_mul {R : Type u_1} {A : Type u_2} [Mul R] [Add A] [Mul A] [SMul R A] (x₁ : ) (x₂ : ) :
(x₁ * x₂).fst = x₁.fst * x₂.fst
@[simp]
theorem Unitization.snd_mul {R : Type u_1} {A : Type u_2} [Mul R] [Add A] [Mul A] [SMul R A] (x₁ : ) (x₂ : ) :
(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) [One R] [Zero A] :
@[simp]
theorem Unitization.inl_mul {R : Type u_1} (A : Type u_2) [] [] (r₁ : R) (r₂ : R) :
Unitization.inl (r₁ * r₂) =
theorem Unitization.inl_mul_inl {R : Type u_1} (A : Type u_2) [] [] (r₁ : R) (r₂ : R) :
= Unitization.inl (r₁ * r₂)
@[simp]
theorem Unitization.inr_mul (R : Type u_1) {A : Type u_2} [] [] [Mul A] [] (a₁ : A) (a₂ : A) :
(a₁ * a₂) = a₁ * a₂
theorem Unitization.inl_mul_inr {R : Type u_1} {A : Type u_2} [] [] (r : R) (a : A) :
* a = (r a)
theorem Unitization.inr_mul_inl {R : Type u_1} {A : Type u_2} [] [] (r : R) (a : A) :
a * = (r a)
instance Unitization.instMulOneClass {R : Type u_1} {A : Type u_2} [] [] :
Equations
• Unitization.instMulOneClass = let __src := Unitization.instOne; let __src_1 := Unitization.instMul;
instance Unitization.instNonAssocSemiring {R : Type u_1} {A : Type u_2} [] [Module R A] :
Equations
• Unitization.instNonAssocSemiring = let __src := Unitization.instMulOneClass; let __src_1 := Unitization.instAddCommMonoid;
instance Unitization.instMonoid {R : Type u_1} {A : Type u_2} [] [] [] [] :
Equations
• Unitization.instMonoid = let __src := Unitization.instMulOneClass; Monoid.mk npowRec
instance Unitization.instCommMonoid {R : Type u_1} {A : Type u_2} [] [] [] [] :
Equations
• Unitization.instCommMonoid = let __src := Unitization.instMonoid;
instance Unitization.instSemiring {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] :
Equations
• Unitization.instSemiring = let __src := Unitization.instMonoid; let __src_1 := Unitization.instNonAssocSemiring; Semiring.mk Monoid.npow
instance Unitization.instCommSemiring {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] :
Equations
• Unitization.instCommSemiring = let __src := Unitization.instCommMonoid; let __src_1 := Unitization.instNonAssocSemiring;
instance Unitization.instNonAssocRing {R : Type u_1} {A : Type u_2} [] [Module R A] :
Equations
• Unitization.instNonAssocRing = let __src := Unitization.instAddCommGroup; let __src_1 := Unitization.instNonAssocSemiring; NonAssocRing.mk
instance Unitization.instRing {R : Type u_1} {A : Type u_2} [] [] [Module R A] [] [] :
Ring ()
Equations
• Unitization.instRing = let __src := Unitization.instAddCommGroup; let __src_1 := Unitization.instSemiring; Ring.mk SubNegMonoid.zsmul
instance Unitization.instCommRing {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] :
Equations
• Unitization.instCommRing = let __src := Unitization.instAddCommGroup; let __src_1 := Unitization.instCommSemiring;
@[simp]
theorem Unitization.inlRingHom_apply (R : Type u_1) (A : Type u_2) [] [Module R A] (r : R) :
() r =
def Unitization.inlRingHom (R : Type u_1) (A : Type u_2) [] [Module R A] :

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

Equations
• = { toFun := Unitization.inl, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For

### Star structure #

instance Unitization.instStar {R : Type u_1} {A : Type u_2} [Star R] [Star A] :
Star ()
Equations
• Unitization.instStar = { star := fun (ra : ) => (star ra.fst, star ra.snd) }
@[simp]
theorem Unitization.fst_star {R : Type u_1} {A : Type u_2} [Star R] [Star A] (x : ) :
(star x).fst = star x.fst
@[simp]
theorem Unitization.snd_star {R : Type u_1} {A : Type u_2} [Star R] [Star A] (x : ) :
(star x).snd = star x.snd
@[simp]
theorem Unitization.inl_star {R : Type u_1} {A : Type u_2} [Star R] [] [] (r : R) :
=
@[simp]
theorem Unitization.inr_star {R : Type u_1} {A : Type u_2} [] [] [Star A] (a : A) :
(star a) = star a
instance Unitization.instStarAddMonoid {R : Type u_1} {A : Type u_2} [] [] [] [] :
Equations
• Unitization.instStarAddMonoid =
instance Unitization.instStarModule {R : Type u_1} {A : Type u_2} [] [] [] [] [Module R A] [] :
Equations
• =
instance Unitization.instStarRing {R : Type u_1} {A : Type u_2} [] [] [] [Module R A] [] :
Equations
• Unitization.instStarRing = let __src := Unitization.instStarAddMonoid;

### Algebra structure #

instance Unitization.instAlgebra (S : Type u_1) (R : Type u_2) (A : Type u_3) [] [] [Module R A] [] [] [Algebra S R] [] [] :
Algebra S ()
Equations
theorem Unitization.algebraMap_eq_inl_comp (S : Type u_1) (R : Type u_2) (A : Type u_3) [] [] [Module R A] [] [] [Algebra S R] [] [] :
(algebraMap S ()) = Unitization.inl ()
theorem Unitization.algebraMap_eq_inlRingHom_comp (S : Type u_1) (R : Type u_2) (A : Type u_3) [] [] [Module R A] [] [] [Algebra S R] [] [] :
algebraMap S () = ().comp ()
theorem Unitization.algebraMap_eq_inl (R : Type u_2) (A : Type u_3) [] [Module R A] [] [] :
(algebraMap R ()) = Unitization.inl
theorem Unitization.algebraMap_eq_inlRingHom (R : Type u_2) (A : Type u_3) [] [Module R A] [] [] :
@[simp]
theorem Unitization.fstHom_apply (R : Type u_2) (A : Type u_3) [] [Module R A] [] [] (x : ) :
() x = x.fst
def Unitization.fstHom (R : Type u_2) (A : Type u_3) [] [Module R A] [] [] :

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

Equations
• = { toFun := Unitization.fst, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem Unitization.inrNonUnitalAlgHom_toFun (R : Type u_1) (A : Type u_2) [] [Module R A] (a : A) :
= a
@[simp]
theorem Unitization.inrNonUnitalAlgHom_apply (R : Type u_1) (A : Type u_2) [] [Module R A] (a : A) :
= a
def Unitization.inrNonUnitalAlgHom (R : Type u_1) (A : Type u_2) [] [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
• = { toFun := Unitization.inr, map_smul' := , map_zero' := , map_add' := , map_mul' := }
Instances For
@[simp]
theorem Unitization.inrNonUnitalStarAlgHom_apply (R : Type u_1) (A : Type u_2) [] [] [Star A] [Module R A] (a : A) :
= a
def Unitization.inrNonUnitalStarAlgHom (R : Type u_1) (A : Type u_2) [] [] [Star A] [Module R A] :

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

Equations
• = { toNonUnitalAlgHom := , map_star' := }
Instances For
theorem Unitization.algHom_ext {S : Type u_1} {R : Type u_2} {A : Type u_3} [] [] [Module R A] [] [] {B : Type u_4} [] [Algebra S B] [Algebra S R] [] [] {F : Type u_6} [FunLike F () B] [AlgHomClass F S () B] {φ : F} {ψ : F} (h : ∀ (a : A), φ a = ψ a) (h' : ∀ (r : R), φ ((algebraMap R ()) r) = ψ ((algebraMap R ()) r)) :
φ = ψ
theorem Unitization.algHom_ext'' {R : Type u_2} {A : Type u_3} [] [Module R A] [] [] {C : Type u_5} [] [Algebra R C] {F : Type u_6} [FunLike F () C] [AlgHomClass F R () C] {φ : F} {ψ : F} (h : ∀ (a : A), φ a = ψ a) :
φ = ψ
theorem Unitization.algHom_ext' {R : Type u_2} {A : Type u_3} [] [Module R A] [] [] {C : Type u_5} [] [Algebra R C] {φ : →ₐ[R] C} {ψ : →ₐ[R] C} (h : (φ).comp = (ψ).comp ) :
φ = ψ

See note [partially-applied ext lemmas]

@[simp]
theorem NonUnitalAlgHom.toAlgHom_apply {R : Type u_2} {A : Type u_3} [] [Module R A] [] [] {C : Type u_5} [] [Algebra R C] (φ : A →ₙₐ[R] C) (x : ) :
φ.toAlgHom x = () x.fst + φ x.snd
def NonUnitalAlgHom.toAlgHom {R : Type u_2} {A : Type u_3} [] [Module R A] [] [] {C : Type u_5} [] [Algebra R C] (φ : A →ₙₐ[R] C) :

A non-unital algebra homomorphism from A into a unital R-algebra C lifts to a unital algebra homomorphism from the unitization into C. This is extended to an Equiv in Unitization.lift and that should be used instead. This declaration only exists for performance reasons.

Equations
• φ.toAlgHom = { toFun := fun (x : ) => () x.fst + φ x.snd, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem Unitization.lift_apply_apply {R : Type u_2} {A : Type u_3} [] [Module R A] [] [] {C : Type u_5} [] [Algebra R C] (φ : A →ₙₐ[R] C) (x : ) :
(Unitization.lift φ) x = () x.fst + φ x.snd
@[simp]
theorem Unitization.lift_symm_apply {R : Type u_2} {A : Type u_3} [] [Module R A] [] [] {C : Type u_5} [] [Algebra R C] (φ : →ₐ[R] C) :
Unitization.lift.symm φ =
@[simp]
theorem Unitization.lift_apply {R : Type u_2} {A : Type u_3} [] [Module R A] [] [] {C : Type u_5} [] [Algebra R C] (φ : A →ₙₐ[R] C) :
Unitization.lift φ = φ.toAlgHom
def Unitization.lift {R : Type u_2} {A : Type u_3} [] [Module R A] [] [] {C : Type u_5} [] [Algebra R C] :
(A →ₙₐ[R] C) ( →ₐ[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
• Unitization.lift = { toFun := NonUnitalAlgHom.toAlgHom, invFun := fun (φ : →ₐ[R] C) => (φ).comp , left_inv := , right_inv := }
Instances For
theorem Unitization.lift_symm_apply_apply {R : Type u_2} {A : Type u_3} [] [Module R A] [] [] {C : Type u_5} [] [Algebra R C] (φ : →ₐ[R] C) (a : A) :
(Unitization.lift.symm φ) a = φ a
@[simp]
theorem NonUnitalAlgHom.toAlgHom_zero {R : Type u_2} {A : Type u_3} [] [Module R A] [] [] :
= Unitization.fst
theorem Unitization.starAlgHom_ext {R : Type u_1} {A : Type u_2} {C : Type u_3} [] [] [] [Module R A] [] [] [] [Algebra R C] [] {φ : →⋆ₐ[R] C} {ψ : →⋆ₐ[R] C} (h : (φ).comp = (ψ).comp ) :
φ = ψ

See note [partially-applied ext lemmas]

@[simp]
theorem Unitization.starLift_apply {R : Type u_1} {A : Type u_2} {C : Type u_3} [] [] [] [Module R A] [] [] [] [Algebra R C] [] [] (φ : A →⋆ₙₐ[R] C) :
Unitization.starLift φ = { toAlgHom := φ.toAlgHom, map_star' := }
@[simp]
theorem Unitization.starLift_apply_apply {R : Type u_1} {A : Type u_2} {C : Type u_3} [] [] [] [Module R A] [] [] [] [Algebra R C] [] [] (φ : A →⋆ₙₐ[R] C) (x : ) :
(Unitization.starLift φ) x = () x.fst + φ x.snd
@[simp]
theorem Unitization.starLift_symm_apply {R : Type u_1} {A : Type u_2} {C : Type u_3} [] [] [] [Module R A] [] [] [] [Algebra R C] [] [] (φ : →⋆ₐ[R] C) :
Unitization.starLift.symm φ = φ.toNonUnitalStarAlgHom.comp
def Unitization.starLift {R : Type u_1} {A : Type u_2} {C : Type u_3} [] [] [] [Module R A] [] [] [] [Algebra R C] [] [] :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Unitization.starLift_symm_apply_apply {R : Type u_1} {A : Type u_2} {C : Type u_3} [] [Module R A] [] [] [] [Algebra R C] (φ : →ₐ[R] C) (a : A) :
(Unitization.lift.symm φ) a = φ a
@[simp]
theorem Unitization.isStarNormal_inr {R : Type u_1} {A : Type u_2} [] [] [Mul A] [] [] [Star A] {a : A} :
instance Unitization.instIsStarNormal (R : Type u_1) {A : Type u_2} [] [] [Mul A] [] [] [Star A] (a : A) [] :
Equations
• =
@[simp]
theorem Unitization.isSelfAdjoint_inr {R : Type u_1} {A : Type u_2} [] [] [Star A] {a : A} :
theorem IsSelfAdjoint.inr (R : Type u_1) {A : Type u_2} [] [] [Star A] {a : A} (ha : ) :
theorem IsSelfAdjoint.of_inr {R : Type u_1} {A : Type u_2} [] [] [Star A] {a : A} :

Alias of the forward direction of Unitization.isSelfAdjoint_inr.

theorem IsStarNormal.of_inr {R : Type u_1} {A : Type u_2} [] [] [Mul A] [] [] [Star A] {a : A} :

Alias of the forward direction of Unitization.isStarNormal_inr.