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

• Unitization R A = (R × A)

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

The canonical inclusion R → Unitization R A.

Equations

• Unitization.inl r = (r, 0)

def Unitization.inr {R : Type u_1} {A : Type u_2} [Zero R] (a : A) : Unitization R A

The canonical inclusion A → Unitization R A.

Equations

• ↑a = (0, a)

instance Unitization.instCoeTCOfZero {R : Type u_1} {A : Type u_2} [Zero R] : CoeTC A (Unitization R A)

Equations

• Unitization.instCoeTCOfZero = { coe := Unitization.inr }

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

The canonical projection Unitization R A → R.

Equations

• x.fst = x.1

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

The canonical projection Unitization R A → A.

Equations

• x.snd = x.2

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

theorem Unitization.ext_iff {R : Type u_1} {A : Type u_2} {x y : Unitization R A} : x = y ↔ x.fst = y.fst ∧ x.snd = y.snd

@[simp]

theorem Unitization.fst_inl {R : Type u_1} (A : Type u_2) [Zero A] (r : R) : (inl r).fst = r

@[simp]

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

theorem Unitization.inr_injective {R : Type u_1} {A : Type u_2} [Zero R] : Function.Injective inr

instance Unitization.instNontrivialLeft {𝕜 : Type u_3} {A : Type u_4} [Nontrivial 𝕜] [Nonempty A] : Nontrivial (Unitization 𝕜 A)

instance Unitization.instNontrivialRight {𝕜 : Type u_3} {A : Type u_4} [Nonempty 𝕜] [Nontrivial A] : Nontrivial (Unitization 𝕜 A)

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 (Unitization R A) A inr fun (x : Unitization R A) => x.fst = 0

instance Unitization.instInhabited {R : Type u_3} {A : Type u_4} [Inhabited R] [Inhabited A] : Inhabited (Unitization R A)

Equations

• Unitization.instInhabited = instInhabitedProd

instance Unitization.instZero {R : Type u_3} {A : Type u_4} [Zero R] [Zero A] : Zero (Unitization R A)

Equations

• Unitization.instZero = Prod.instZero

instance Unitization.instAdd {R : Type u_3} {A : Type u_4} [Add R] [Add A] : Add (Unitization R A)

Equations

• Unitization.instAdd = Prod.instAdd

instance Unitization.instNeg {R : Type u_3} {A : Type u_4} [Neg R] [Neg A] : Neg (Unitization R A)

Equations

• Unitization.instNeg = Prod.instNeg

instance Unitization.instAddSemigroup {R : Type u_3} {A : Type u_4} [AddSemigroup R] [AddSemigroup A] : AddSemigroup (Unitization R A)

Equations

• Unitization.instAddSemigroup = Prod.instAddSemigroup

instance Unitization.instAddZeroClass {R : Type u_3} {A : Type u_4} [AddZeroClass R] [AddZeroClass A] : AddZeroClass (Unitization R A)

Equations

• Unitization.instAddZeroClass = Prod.instAddZeroClass

instance Unitization.instAddMonoid {R : Type u_3} {A : Type u_4} [AddMonoid R] [AddMonoid A] : AddMonoid (Unitization R A)

Equations

• Unitization.instAddMonoid = Prod.instAddMonoid

instance Unitization.instAddGroup {R : Type u_3} {A : Type u_4} [AddGroup R] [AddGroup A] : AddGroup (Unitization R A)

Equations

• Unitization.instAddGroup = Prod.instAddGroup

instance Unitization.instAddCommSemigroup {R : Type u_3} {A : Type u_4} [AddCommSemigroup R] [AddCommSemigroup A] : AddCommSemigroup (Unitization R A)

Equations

• Unitization.instAddCommSemigroup = Prod.instAddCommSemigroup

instance Unitization.instAddCommMonoid {R : Type u_3} {A : Type u_4} [AddCommMonoid R] [AddCommMonoid A] : AddCommMonoid (Unitization R A)

Equations

• Unitization.instAddCommMonoid = Prod.instAddCommMonoid

instance Unitization.instAddCommGroup {R : Type u_3} {A : Type u_4} [AddCommGroup R] [AddCommGroup A] : AddCommGroup (Unitization R A)

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 (Unitization R A)

Equations

• Unitization.instSMul = Prod.instSMul

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] [IsScalarTower T S R] [IsScalarTower T S A] : IsScalarTower T S (Unitization R A)

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] [SMulCommClass T S R] [SMulCommClass T S A] : SMulCommClass T S (Unitization R A)

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] [IsCentralScalar S R] [IsCentralScalar S A] : IsCentralScalar S (Unitization R A)

instance Unitization.instMulAction {S : Type u_2} {R : Type u_3} {A : Type u_4} [Monoid S] [MulAction S R] [MulAction S A] : MulAction S (Unitization R A)

Equations

• Unitization.instMulAction = Prod.mulAction

instance Unitization.instDistribMulAction {S : Type u_2} {R : Type u_3} {A : Type u_4} [Monoid S] [AddMonoid R] [AddMonoid A] [DistribMulAction S R] [DistribMulAction S A] : DistribMulAction S (Unitization R A)

Equations

• Unitization.instDistribMulAction = Prod.distribMulAction

instance Unitization.instModule {S : Type u_2} {R : Type u_3} {A : Type u_4} [Semiring S] [AddCommMonoid R] [AddCommMonoid A] [Module S R] [Module S A] : Module S (Unitization R A)

Equations

• Unitization.instModule = Prod.instModule

def Unitization.addEquiv (R : Type u_3) (A : Type u_4) [Add R] [Add A] : Unitization R A ≃+ R × A

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

Equations

• Unitization.addEquiv R A = AddEquiv.refl (Unitization R A)

@[simp]

theorem Unitization.fst_zero {R : Type u_3} {A : Type u_4} [Zero R] [Zero A] : fst 0 = 0

@[simp]

theorem Unitization.snd_zero {R : Type u_3} {A : Type u_4} [Zero R] [Zero A] : snd 0 = 0

@[simp]

theorem Unitization.fst_add {R : Type u_3} {A : Type u_4} [Add R] [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} [Add R] [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} [Neg R] [Neg A] (x : Unitization R A) : (-x).fst = -x.fst

@[simp]

theorem Unitization.snd_neg {R : Type u_3} {A : Type u_4} [Neg R] [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} [SMul S R] [SMul 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} [SMul S R] [SMul 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) [Zero R] [Zero A] : inl 0 = 0

@[simp]

theorem Unitization.inl_add {R : Type u_3} (A : Type u_4) [Add R] [AddZeroClass A] (r₁ r₂ : R) : inl (r₁ + r₂) = inl r₁ + inl r₂

@[simp]

theorem Unitization.inl_neg {R : Type u_3} (A : Type u_4) [Neg R] [SubtractionMonoid A] (r : R) : inl (-r) = -inl r

@[simp]

theorem Unitization.inl_sub {R : Type u_3} (A : Type u_4) [AddGroup R] [AddGroup A] (r₁ r₂ : R) : inl (r₁ - r₂) = inl r₁ - inl r₂

@[simp]

theorem Unitization.inl_smul {S : Type u_2} {R : Type u_3} (A : Type u_4) [Zero A] [SMul S R] [SMulZeroClass S A] (s : S) (r : R) : inl (s • r) = s • inl 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} [AddZeroClass R] [Add A] (m₁ m₂ : A) : ↑(m₁ + m₂) = ↑m₁ + ↑m₂

@[simp]

theorem Unitization.inr_neg (R : Type u_3) {A : Type u_4} [SubtractionMonoid R] [Neg A] (m : A) : ↑(-m) = -↑m

@[simp]

theorem Unitization.inr_sub (R : Type u_3) {A : Type u_4} [AddGroup R] [AddGroup A] (m₁ m₂ : A) : ↑(m₁ - m₂) = ↑m₁ - ↑m₂

@[simp]

theorem Unitization.inr_smul {S : Type u_2} (R : Type u_3) {A : Type u_4} [Zero R] [SMulZeroClass S R] [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} [AddZeroClass R] [AddZeroClass A] (x : Unitization R A) : inl x.fst + ↑x.snd = x

theorem Unitization.ind {R : Type u_5} {A : Type u_6} [AddZeroClass R] [AddZeroClass A] {P : Unitization R A → Prop} (inl_add_inr : ∀ (r : R) (a : A), P (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.

theorem Unitization.linearMap_ext {S : Type u_2} {R : Type u_3} {A : Type u_4} {N : Type u_5} [Semiring S] [AddCommMonoid R] [AddCommMonoid A] [AddCommMonoid N] [Module S R] [Module S A] [Module S N] ⦃f g : Unitization R A →ₗ[S] N⦄ (hl : ∀ (r : R), f (inl r) = g (inl r)) (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.

def Unitization.inrHom (R : Type u_3) (A : Type u_4) [Semiring R] [AddCommMonoid A] [Module R A] : A →ₗ[R] Unitization R A

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

Equations

• Unitization.inrHom R A = { toFun := Unitization.inr, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Unitization.inrHom_apply (R : Type u_3) (A : Type u_4) [Semiring R] [AddCommMonoid A] [Module R A] (a : A) : (inrHom R A) a = ↑a

def Unitization.sndHom (R : Type u_3) (A : Type u_4) [Semiring R] [AddCommMonoid A] [Module R A] : Unitization R A →ₗ[R] A

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

Equations

• Unitization.sndHom R A = { toFun := Unitization.snd, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Unitization.sndHom_apply (R : Type u_3) (A : Type u_4) [Semiring R] [AddCommMonoid A] [Module R A] (x : Unitization R A) : (sndHom R A) x = x.snd

Multiplicative structure

instance Unitization.instOne {R : Type u_1} {A : Type u_2} [One R] [Zero A] : One (Unitization R A)

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 (Unitization R A)

Equations

• Unitization.instMul = { mul := fun (x y : Unitization R A) => (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] : fst 1 = 1

@[simp]

theorem Unitization.snd_one {R : Type u_1} {A : Type u_2} [One R] [Zero A] : snd 1 = 0

@[simp]

theorem Unitization.fst_mul {R : Type u_1} {A : Type u_2} [Mul R] [Add A] [Mul A] [SMul 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} [Mul R] [Add A] [Mul A] [SMul 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) [One R] [Zero A] : inl 1 = 1

@[simp]

theorem Unitization.inl_mul {R : Type u_1} (A : Type u_2) [Mul R] [NonUnitalNonAssocSemiring A] [SMulZeroClass R A] (r₁ r₂ : R) : inl (r₁ * r₂) = inl r₁ * inl r₂

theorem Unitization.inl_mul_inl {R : Type u_1} (A : Type u_2) [Mul R] [NonUnitalNonAssocSemiring A] [SMulZeroClass R A] (r₁ r₂ : R) : inl r₁ * inl r₂ = inl (r₁ * r₂)

@[simp]

theorem Unitization.inr_mul (R : Type u_1) {A : Type u_2} [MulZeroClass R] [AddZeroClass A] [Mul A] [SMulWithZero R A] (a₁ a₂ : A) : ↑(a₁ * a₂) = ↑a₁ * ↑a₂

theorem Unitization.inl_mul_inr {R : Type u_1} {A : Type u_2} [MulZeroClass R] [NonUnitalNonAssocSemiring A] [SMulZeroClass R A] (r : R) (a : A) : inl r * ↑a = ↑(r • a)

theorem Unitization.inr_mul_inl {R : Type u_1} {A : Type u_2} [MulZeroClass R] [NonUnitalNonAssocSemiring A] [SMulZeroClass R A] (r : R) (a : A) : ↑a * inl r = ↑(r • a)

instance Unitization.instMulOneClass {R : Type u_1} {A : Type u_2} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] : MulOneClass (Unitization R A)

Equations

• Unitization.instMulOneClass = { toOne := Unitization.instOne, toMul := Unitization.instMul, one_mul := ⋯, mul_one := ⋯ }

instance Unitization.instNonAssocSemiring {R : Type u_1} {A : Type u_2} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] : NonAssocSemiring (Unitization R A)

Equations

• One or more equations did not get rendered due to their size.

instance Unitization.instMonoid {R : Type u_1} {A : Type u_2} [CommMonoid R] [NonUnitalSemiring A] [DistribMulAction R A] [IsScalarTower R A A] [SMulCommClass R A A] : Monoid (Unitization R A)

Equations

• One or more equations did not get rendered due to their size.

instance Unitization.instCommMonoid {R : Type u_1} {A : Type u_2} [CommMonoid R] [NonUnitalCommSemiring A] [DistribMulAction R A] [IsScalarTower R A A] [SMulCommClass R A A] : CommMonoid (Unitization R A)

Equations

• Unitization.instCommMonoid = { toMonoid := Unitization.instMonoid, mul_comm := ⋯ }

instance Unitization.instSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : Semiring (Unitization R A)

Equations

• One or more equations did not get rendered due to their size.

instance Unitization.instCommSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalCommSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : CommSemiring (Unitization R A)

Equations

• One or more equations did not get rendered due to their size.

instance Unitization.instNonAssocRing {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] : NonAssocRing (Unitization R A)

Equations

• One or more equations did not get rendered due to their size.

instance Unitization.instRing {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : Ring (Unitization R A)

Equations

• One or more equations did not get rendered due to their size.

instance Unitization.instCommRing {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalCommRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : CommRing (Unitization R A)

Equations

• One or more equations did not get rendered due to their size.

def Unitization.inlRingHom (R : Type u_1) (A : Type u_2) [Semiring R] [NonUnitalSemiring A] [Module R A] : R →+* Unitization R A

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

Equations

• Unitization.inlRingHom R A = { toFun := Unitization.inl, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Unitization.inlRingHom_apply (R : Type u_1) (A : Type u_2) [Semiring R] [NonUnitalSemiring A] [Module R A] (r : R) : (inlRingHom R A) r = inl r

Star structure

instance Unitization.instStar {R : Type u_1} {A : Type u_2} [Star R] [Star A] : Star (Unitization R A)

Equations

• Unitization.instStar = { star := fun (ra : Unitization R A) => (star ra.fst, star ra.snd) }

@[simp]

theorem Unitization.fst_star {R : Type u_1} {A : Type u_2} [Star R] [Star A] (x : Unitization R A) : (star x).fst = star x.fst

@[simp]

theorem Unitization.snd_star {R : Type u_1} {A : Type u_2} [Star R] [Star A] (x : Unitization R A) : (star x).snd = star x.snd

@[simp]

theorem Unitization.inl_star {R : Type u_1} {A : Type u_2} [Star R] [AddMonoid A] [StarAddMonoid A] (r : R) : inl (star r) = star (inl r)

@[simp]

theorem Unitization.inr_star {R : Type u_1} {A : Type u_2} [AddMonoid R] [StarAddMonoid R] [Star A] (a : A) : ↑(star a) = star ↑a

instance Unitization.instStarAddMonoid {R : Type u_1} {A : Type u_2} [AddMonoid R] [AddMonoid A] [StarAddMonoid R] [StarAddMonoid A] : StarAddMonoid (Unitization R A)

Equations

• Unitization.instStarAddMonoid = { toStar := Unitization.instStar, star_involutive := ⋯, star_add := ⋯ }

instance Unitization.instStarModule {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] : StarModule R (Unitization R A)

instance Unitization.instStarRing {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [NonUnitalNonAssocSemiring A] [StarRing A] [Module R A] [StarModule R A] : StarRing (Unitization R A)

Equations

• Unitization.instStarRing = { toInvolutiveStar := Unitization.instStarAddMonoid.toInvolutiveStar, star_mul := ⋯, star_add := ⋯ }

Algebra structure

instance Unitization.instAlgebra (S : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring S] [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [Algebra S R] [DistribMulAction S A] [IsScalarTower S R A] : Algebra S (Unitization R A)

Equations

• Unitization.instAlgebra S R A = { toSMul := Unitization.instSMul, algebraMap := (Unitization.inlRingHom R A).comp (algebraMap S R), commutes' := ⋯, smul_def' := ⋯ }

theorem Unitization.algebraMap_eq_inl_comp (S : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring S] [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [Algebra S R] [DistribMulAction S A] [IsScalarTower S R A] : ⇑(algebraMap S (Unitization R A)) = inl ∘ ⇑(algebraMap S R)

theorem Unitization.algebraMap_eq_inlRingHom_comp (S : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring S] [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [Algebra S R] [DistribMulAction S A] [IsScalarTower S R A] : algebraMap S (Unitization R A) = (inlRingHom R A).comp (algebraMap S R)

theorem Unitization.algebraMap_eq_inl (R : Type u_2) (A : Type u_3) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ⇑(algebraMap R (Unitization R A)) = inl

theorem Unitization.algebraMap_eq_inlRingHom (R : Type u_2) (A : Type u_3) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : algebraMap R (Unitization R A) = inlRingHom R A

def Unitization.fstHom (R : Type u_2) (A : Type u_3) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : Unitization R A →ₐ[R] R

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

Equations

• Unitization.fstHom R A = { toFun := Unitization.fst, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem Unitization.fstHom_apply (R : Type u_2) (A : Type u_3) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : Unitization R A) : (fstHom R A) x = x.fst

def Unitization.inrNonUnitalAlgHom (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalSemiring A] [Module R A] : A →ₙₐ[R] Unitization 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

• Unitization.inrNonUnitalAlgHom R A = { toFun := Unitization.inr, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Unitization.inrNonUnitalAlgHom_toFun (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalSemiring A] [Module R A] (a : A) : (inrNonUnitalAlgHom R A) a = ↑a

@[simp]

theorem Unitization.inrNonUnitalAlgHom_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalSemiring A] [Module R A] (a : A) : (inrNonUnitalAlgHom R A) a = ↑a

def Unitization.inrNonUnitalStarAlgHom (R : Type u_1) (A : Type u_2) [CommSemiring R] [StarAddMonoid R] [NonUnitalSemiring A] [Star A] [Module R A] : A →⋆ₙₐ[R] Unitization 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

• Unitization.inrNonUnitalStarAlgHom R A = { toNonUnitalAlgHom := Unitization.inrNonUnitalAlgHom R A, map_star' := ⋯ }

@[simp]

theorem Unitization.inrNonUnitalStarAlgHom_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [StarAddMonoid R] [NonUnitalSemiring A] [Star A] [Module R A] (a : A) : (inrNonUnitalStarAlgHom R A) a = ↑a

def Unitization.inrRangeEquiv (R : Type u_1) (A : Type u_2) [CommSemiring R] [StarAddMonoid R] [NonUnitalSemiring A] [Star A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : A ≃⋆ₐ[R] ↥(NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom R A))

The star algebra equivalence obtained by restricting Unitization.inrNonUnitalStarAlgHom to its range.

Equations

• Unitization.inrRangeEquiv R A = StarAlgEquiv.ofLeftInverse' ⋯

@[simp]

theorem Unitization.inrRangeEquiv_symm_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [StarAddMonoid R] [NonUnitalSemiring A] [Star A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (a✝ : ↥(NonUnitalStarAlgHom.range (inrNonUnitalStarAlgHom R A))) : (inrRangeEquiv R A).symm a✝ = (↑a✝).snd

@[simp]

theorem Unitization.inrRangeEquiv_apply_coe (R : Type u_1) (A : Type u_2) [CommSemiring R] [StarAddMonoid R] [NonUnitalSemiring A] [Star A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (a : A) : ↑((inrRangeEquiv R A) a) = ↑(inrNonUnitalStarAlgHom R A) a

theorem Unitization.algHom_ext {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {B : Type u_4} [Semiring B] [Algebra S B] [Algebra S R] [DistribMulAction S A] [IsScalarTower S R A] {F : Type u_6} [FunLike F (Unitization R A) B] [AlgHomClass F S (Unitization R A) B] {φ ψ : F} (h : ∀ (a : A), φ ↑a = ψ ↑a) (h' : ∀ (r : R), φ ((algebraMap R (Unitization R A)) r) = ψ ((algebraMap R (Unitization R A)) r)) : φ = ψ

theorem Unitization.algHom_ext'' {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {C : Type u_5} [Semiring C] [Algebra R C] {F : Type u_6} [FunLike F (Unitization R A) C] [AlgHomClass F R (Unitization R A) C] {φ ψ : F} (h : ∀ (a : A), φ ↑a = ψ ↑a) : φ = ψ

theorem Unitization.algHom_ext' {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {C : Type u_5} [Semiring C] [Algebra R C] {φ ψ : Unitization R A →ₐ[R] C} (h : (↑φ).comp (inrNonUnitalAlgHom R A) = (↑ψ).comp (inrNonUnitalAlgHom R A)) : φ = ψ

See note [partially-applied ext lemmas]

theorem Unitization.algHom_ext'_iff {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {C : Type u_5} [Semiring C] [Algebra R C] {φ ψ : Unitization R A →ₐ[R] C} : φ = ψ ↔ (↑φ).comp (inrNonUnitalAlgHom R A) = (↑ψ).comp (inrNonUnitalAlgHom R A)

def NonUnitalAlgHom.toAlgHom {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {C : Type u_5} [Semiring C] [Algebra R C] (φ : A →ₙₐ[R] C) : Unitization R 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 : Unitization R A) => (algebraMap R C) x.fst + φ x.snd, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem NonUnitalAlgHom.toAlgHom_apply {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {C : Type u_5} [Semiring C] [Algebra R C] (φ : A →ₙₐ[R] C) (x : Unitization R A) : φ.toAlgHom x = (algebraMap R C) x.fst + φ x.snd

def Unitization.lift {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {C : Type u_5} [Semiring C] [Algebra R C] : (A →ₙₐ[R] C) ≃ (Unitization R 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

• Unitization.lift = { toFun := NonUnitalAlgHom.toAlgHom, invFun := fun (φ : Unitization R A →ₐ[R] C) => (↑φ).comp (Unitization.inrNonUnitalAlgHom R A), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Unitization.lift_apply_apply {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {C : Type u_5} [Semiring C] [Algebra R C] (φ : A →ₙₐ[R] C) (x : Unitization R A) : (lift φ) x = (algebraMap R C) x.fst + φ x.snd

@[simp]

theorem Unitization.lift_symm_apply {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {C : Type u_5} [Semiring C] [Algebra R C] (φ : Unitization R A →ₐ[R] C) : lift.symm φ = (NonUnitalAlgHomClass.toNonUnitalAlgHom φ).comp (inrNonUnitalAlgHom R A)

@[simp]

theorem Unitization.lift_apply {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {C : Type u_5} [Semiring C] [Algebra R C] (φ : A →ₙₐ[R] C) : lift φ = φ.toAlgHom

theorem Unitization.lift_symm_apply_apply {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {C : Type u_5} [Semiring C] [Algebra R C] (φ : Unitization R A →ₐ[R] C) (a : A) : (lift.symm φ) a = φ ↑a

@[simp]

theorem NonUnitalAlgHom.toAlgHom_zero {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] : ⇑(toAlgHom 0) = Unitization.fst

theorem Unitization.starAlgHom_ext {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [Semiring C] [Algebra R C] [StarRing C] {φ ψ : Unitization R A →⋆ₐ[R] C} (h : (↑φ).comp (inrNonUnitalStarAlgHom R A) = (↑ψ).comp (inrNonUnitalStarAlgHom R A)) : φ = ψ

See note [partially-applied ext lemmas]

theorem Unitization.starAlgHom_ext_iff {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [Semiring C] [Algebra R C] [StarRing C] {φ ψ : Unitization R A →⋆ₐ[R] C} : φ = ψ ↔ (↑φ).comp (inrNonUnitalStarAlgHom R A) = (↑ψ).comp (inrNonUnitalStarAlgHom R A)

def Unitization.starLift {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [Semiring C] [Algebra R C] [StarRing C] [StarModule R C] : (A →⋆ₙₐ[R] C) ≃ (Unitization R A →⋆ₐ[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.

@[simp]

theorem Unitization.starLift_apply_apply {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [Semiring C] [Algebra R C] [StarRing C] [StarModule R C] (φ : A →⋆ₙₐ[R] C) (x : Unitization R A) : (starLift φ) x = (algebraMap R C) x.fst + φ x.snd

@[simp]

theorem Unitization.starLift_symm_apply {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [Semiring C] [Algebra R C] [StarRing C] [StarModule R C] (φ : Unitization R A →⋆ₐ[R] C) : starLift.symm φ = φ.toNonUnitalStarAlgHom.comp (inrNonUnitalStarAlgHom R A)

@[simp]

theorem Unitization.starLift_apply {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [Semiring C] [Algebra R C] [StarRing C] [StarModule R C] (φ : A →⋆ₙₐ[R] C) : starLift φ = { toAlgHom := φ.toAlgHom, map_star' := ⋯ }

@[simp]

theorem Unitization.starLift_symm_apply_apply {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [Semiring C] [Algebra R C] [StarRing C] [StarModule R C] (φ : Unitization R A →⋆ₐ[R] C) (a : A) : (starLift.symm φ) a = φ ↑a

def Unitization.starMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalSemiring B] [StarRing B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] [StarModule R B] (φ : A →⋆ₙₐ[R] B) : Unitization R A →⋆ₐ[R] Unitization R B

The functorial map on morphisms between the category of non-unital C⋆-algebras with non-unital star homomorphisms and unital C⋆-algebras with unital star homomorphisms.

This sends φ : A →⋆ₙₐ[R] B to a map Unitization R A →⋆ₐ[R] Unitization R B given by the formula (r, a) ↦ (r, φ a) (or perhaps more precisely, algebraMap R _ r + ↑a ↦ algebraMap R _ r + ↑(φ a)).

Equations

• Unitization.starMap φ = Unitization.starLift ((Unitization.inrNonUnitalStarAlgHom R B).comp φ)

@[simp]

theorem Unitization.starMap_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalSemiring B] [StarRing B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] [StarModule R B] (φ : A →⋆ₙₐ[R] B) (x : Unitization R A) : (starMap φ) x = (algebraMap R (Unitization R B)) x.fst + ↑(φ x.snd)

@[simp]

theorem Unitization.starMap_inr {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalSemiring B] [StarRing B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] [StarModule R B] (φ : A →⋆ₙₐ[R] B) (a : A) : (starMap φ) ↑a = ↑(φ a)

@[simp]

theorem Unitization.starMap_inl {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalSemiring B] [StarRing B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] [StarModule R B] (φ : A →⋆ₙₐ[R] B) (r : R) : (starMap φ) (inl r) = (algebraMap R (Unitization R B)) r

theorem Unitization.starMap_injective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalSemiring B] [StarRing B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] [StarModule R B] {φ : A →⋆ₙₐ[R] B} (hφ : Function.Injective ⇑φ) : Function.Injective ⇑(starMap φ)

If φ : A →⋆ₙₐ[R] B is injective, the lift starMap φ : Unitization R A →⋆ₐ[R] Unitization R B is also injective.

theorem Unitization.starMap_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalSemiring B] [StarRing B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] [StarModule R B] {φ : A →⋆ₙₐ[R] B} (hφ : Function.Surjective ⇑φ) : Function.Surjective ⇑(starMap φ)

If φ : A →⋆ₙₐ[R] B is surjective, the lift starMap φ : Unitization R A →⋆ₐ[R] Unitization R B is also surjective.

theorem Unitization.starMap_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalSemiring B] [StarRing B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] [NonUnitalSemiring C] [StarRing C] [Module R C] [SMulCommClass R C C] [IsScalarTower R C C] [StarModule R B] [StarModule R C] {φ : A →⋆ₙₐ[R] B} {ψ : B →⋆ₙₐ[R] C} : starMap (ψ.comp φ) = (starMap ψ).comp (starMap φ)

starMap is functorial: starMap (ψ.comp φ) = (starMap ψ).comp (starMap φ).

@[simp]

theorem Unitization.starMap_id {R : Type u_1} {B : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring B] [StarRing B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] [StarModule R B] : starMap (NonUnitalStarAlgHom.id R B) = StarAlgHom.id R (Unitization R B)

starMap is functorial: starMap (NonUnitalStarAlgHom.id R B) = StarAlgHom.id R (Unitization R B).

@[simp]

theorem Unitization.isSelfAdjoint_inr {R : Type u_1} {A : Type u_2} [Semiring R] [StarAddMonoid R] [Star A] {a : A} : IsSelfAdjoint ↑a ↔ IsSelfAdjoint a

theorem IsSelfAdjoint.of_inr {R : Type u_1} {A : Type u_2} [Semiring R] [StarAddMonoid R] [Star A] {a : A} : IsSelfAdjoint ↑a → IsSelfAdjoint a

Alias of the forward direction of Unitization.isSelfAdjoint_inr.

theorem IsSelfAdjoint.inr (R : Type u_1) {A : Type u_2} [Semiring R] [StarAddMonoid R] [Star A] {a : A} (ha : IsSelfAdjoint a) : IsSelfAdjoint ↑a

@[simp]

theorem Unitization.isStarNormal_inr {R : Type u_1} {A : Type u_2} [Semiring R] [StarAddMonoid R] [Star A] {a : A} [AddCommMonoid A] [Mul A] [SMulWithZero R A] : IsStarNormal ↑a ↔ IsStarNormal a

theorem IsStarNormal.of_inr {R : Type u_1} {A : Type u_2} [Semiring R] [StarAddMonoid R] [Star A] {a : A} [AddCommMonoid A] [Mul A] [SMulWithZero R A] : IsStarNormal ↑a → IsStarNormal a

Alias of the forward direction of Unitization.isStarNormal_inr.

instance Unitization.instIsStarNormal (R : Type u_1) {A : Type u_2} [Semiring R] [StarAddMonoid R] [Star A] [AddCommMonoid A] [Mul A] [SMulWithZero R A] (a : A) [IsStarNormal a] : IsStarNormal ↑a

@[simp]

theorem Unitization.isIdempotentElem_inr_iff (R : Type u_1) {A : Type u_2} [MulZeroClass R] [AddZeroClass A] [Mul A] [SMulWithZero R A] {a : A} : IsIdempotentElem ↑a ↔ IsIdempotentElem a

theorem Unitization.IsIdempotentElem.inr (R : Type u_1) {A : Type u_2} [MulZeroClass R] [AddZeroClass A] [Mul A] [SMulWithZero R A] {a : A} : IsIdempotentElem a → IsIdempotentElem ↑a

Alias of the reverse direction of Unitization.isIdempotentElem_inr_iff.