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.

structure Unitization (R : Type u_1) (A : Type u_2) extends R × A : Type (max u_1 u_2)

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

• fst : R
• snd : A

theorem Unitization.ext_iff {R : Type u_1} {A : Type u_2} {x y : Unitization R A} : x = y ↔ x.toProd.1 = y.toProd.1 ∧ x.toProd.2 = y.toProd.2

theorem Unitization.ext {R : Type u_1} {A : Type u_2} {x y : Unitization R A} (fst : x.toProd.1 = y.toProd.1) (snd : x.toProd.2 = y.toProd.2) : x = y

def Unitization.delabMk : Lean.PrettyPrinter.Delaborator.Delab

This prevents mk x being printed as { toProd := x } by delabStructureInstance.

theorem Unitization.mk_toProd {R : Type u_1} {A : Type u_2} (x : Unitization R A) : mk x.toProd = x

theorem Unitization.toProd_mk {R : Type u_1} {A : Type u_2} (x : R × A) : (mk x).toProd = x

def Unitization.equiv {R : Type u_1} {A : Type u_2} : Unitization R A ≃ R × A

The canonical equivalence between Unitization R A and R × A.

@[simp]

theorem Unitization.equiv_symm_apply {R : Type u_1} {A : Type u_2} (toProd : R × A) : equiv.symm toProd = mk toProd

@[simp]

theorem Unitization.equiv_apply {R : Type u_1} {A : Type u_2} (self : Unitization R A) : equiv self = self.toProd

theorem Unitization.toProd_injective {R : Type u_1} {A : Type u_2} : Function.Injective toProd

theorem Unitization.toProd_surjective {R : Type u_1} {A : Type u_2} : Function.Surjective toProd

theorem Unitization.toProd_bijective {R : Type u_1} {A : Type u_2} : Function.Bijective toProd

theorem Unitization.mk_injective {R : Type u_1} {A : Type u_2} : Function.Injective mk

theorem Unitization.mk_surjective {R : Type u_1} {A : Type u_2} : Function.Surjective mk

theorem Unitization.mk_bijective {R : Type u_1} {A : Type u_2} : Function.Bijective mk

@[simp]

theorem Unitization.toProd_inj_iff {R : Type u_1} {A : Type u_2} {x y : Unitization R A} : x.toProd = y.toProd ↔ x = y

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.

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.

@[implicit_reducible]

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

@[simp]

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

@[simp]

theorem Unitization.snd_inl {R : Type u_1} (A : Type u_2) [Zero A] (r : R) : (inl r).toProd.2 = 0

@[simp]

theorem Unitization.fst_inr (R : Type u_1) {A : Type u_2} [Zero R] (a : A) : (↑a).toProd.1 = 0

@[simp]

theorem Unitization.snd_inr (R : Type u_1) {A : Type u_2} [Zero R] (a : A) : (↑a).toProd.2 = 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

@[simp]

theorem Unitization.inr_inj {R : Type u_1} {A : Type u_2} [Zero R] {x y : A} : ↑x = ↑y ↔ x = y

@[simp]

theorem Unitization.inl_inj {R : Type u_1} {A : Type u_2} [Zero A] {x y : R} : inl x = inl y ↔ x = y

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.toProd.1 = 0

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Unitization.instSub {R : Type u_3} {A : Type u_4} [Sub R] [Sub A] : Sub (Unitization R A)

@[implicit_reducible]

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

@[implicit_reducible]

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)

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[simp]

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

@[simp]

theorem Unitization.toProd_add {R : Type u_3} {A : Type u_4} [Add R] [Add A] (x₁ x₂ : Unitization R A) : (x₁ + x₂).toProd = x₁.toProd + x₂.toProd

@[simp]

theorem Unitization.toProd_neg {R : Type u_3} {A : Type u_4} [Neg R] [Neg A] (x : Unitization R A) : (-x).toProd = -x.toProd

@[simp]

theorem Unitization.toProd_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).toProd = s • x.toProd

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)

@[implicit_reducible]

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)

@[implicit_reducible]

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)

@[implicit_reducible]

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)

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.

@[simp]

theorem Unitization.addEquiv_symm_apply (R : Type u_3) (A : Type u_4) [Add R] [Add A] (toProd : R × A) : (addEquiv R A).symm toProd = mk toProd

@[simp]

theorem Unitization.addEquiv_apply (R : Type u_3) (A : Type u_4) [Add R] [Add A] (self : Unitization R A) : (addEquiv R A) self = self.toProd

theorem Unitization.toEquiv_addEquiv {R : Type u_3} {A : Type u_4} [Add R] [Add A] : (addEquiv R A).toEquiv = equiv

def Unitization.linearEquiv (S : Type u_2) (R : Type u_3) (A : Type u_4) [Semiring S] [AddCommMonoid R] [AddCommMonoid A] [Module S R] [Module S A] : Unitization R A ≃ₗ[S] R × A

The identity map between Unitization R A and R × A as a LinearEquiv.

@[simp]

theorem Unitization.linearEquiv_symm_apply (S : Type u_2) (R : Type u_3) (A : Type u_4) [Semiring S] [AddCommMonoid R] [AddCommMonoid A] [Module S R] [Module S A] (a✝ : R × A) : (linearEquiv S R A).symm a✝ = mk a✝

@[simp]

theorem Unitization.linearEquiv_apply (S : Type u_2) (R : Type u_3) (A : Type u_4) [Semiring S] [AddCommMonoid R] [AddCommMonoid A] [Module S R] [Module S A] (a✝ : Unitization R A) : (linearEquiv S R A) a✝ = a✝.toProd

@[simp]

theorem Unitization.toAddEquiv_linearEquiv {S : Type u_2} {R : Type u_3} {A : Type u_4} [Semiring S] [AddCommMonoid R] [AddCommMonoid A] [Module S R] [Module S A] : (linearEquiv S R A).toAddEquiv = addEquiv R A

@[simp]

theorem Unitization.fst_zero {R : Type u_3} {A : Type u_4} [Zero R] [Zero A] : (toProd 0).1 = 0

@[simp]

theorem Unitization.snd_zero {R : Type u_3} {A : Type u_4} [Zero R] [Zero A] : (toProd 0).2 = 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₂).toProd.1 = x₁.toProd.1 + x₂.toProd.1

@[simp]

theorem Unitization.snd_add {R : Type u_3} {A : Type u_4} [Add R] [Add A] (x₁ x₂ : Unitization R A) : (x₁ + x₂).toProd.2 = x₁.toProd.2 + x₂.toProd.2

@[simp]

theorem Unitization.fst_neg {R : Type u_3} {A : Type u_4} [Neg R] [Neg A] (x : Unitization R A) : (-x).toProd.1 = -x.toProd.1

@[simp]

theorem Unitization.snd_neg {R : Type u_3} {A : Type u_4} [Neg R] [Neg A] (x : Unitization R A) : (-x).toProd.2 = -x.toProd.2

@[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).toProd.1 = s • x.toProd.1

@[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).toProd.2 = s • x.toProd.2

@[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] [AddGroup 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} [AddGroup 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.toProd.1 + ↑x.toProd.2 = 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} [CommSemiring 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

theorem Unitization.linearMap_ext_iff {S : Type u_2} {R : Type u_3} {A : Type u_4} {N : Type u_5} [CommSemiring S] [AddCommMonoid R] [AddCommMonoid A] [AddCommMonoid N] [Module S R] [Module S A] [Module S N] {f g : Unitization R A →ₗ[S] N} : f = g ↔ (∀ (r : R), f (inl r) = g (inl r)) ∧ ∀ (a : A), f ↑a = g ↑a

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

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

@[simp]

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

theorem Unitization.inrHom_injective {S : Type u_2} {R : Type u_3} {A : Type u_4} [Semiring S] [Semiring R] [AddCommMonoid A] [Module S R] [Module S A] : Function.Injective ⇑(inrHom S R A)

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

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

@[simp]

theorem Unitization.sndHom_apply (S : Type u_2) (R : Type u_3) (A : Type u_4) [Semiring S] [Semiring R] [AddCommMonoid A] [Module S R] [Module S A] (a : Unitization R A) : (sndHom S R A) a = a.toProd.2

Multiplicative structure

@[implicit_reducible]

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

@[implicit_reducible]

instance Unitization.instMul {R : Type u_1} {A : Type u_2} [Mul R] [Add A] [Mul A] [SMul R A] : Mul (Unitization R A)

@[simp]

theorem Unitization.fst_one {R : Type u_1} {A : Type u_2} [One R] [Zero A] : (toProd 1).1 = 1

@[simp]

theorem Unitization.snd_one {R : Type u_1} {A : Type u_2} [One R] [Zero A] : (toProd 1).2 = 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₂).toProd.1 = x₁.toProd.1 * x₂.toProd.1

@[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₂).toProd.2 = x₁.toProd.1 • x₂.toProd.2 + x₂.toProd.1 • x₁.toProd.2 + x₁.toProd.2 * x₂.toProd.2

@[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)

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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)

@[implicit_reducible]

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)

@[implicit_reducible]

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)

@[implicit_reducible]

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)

@[implicit_reducible]

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

@[implicit_reducible]

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)

@[implicit_reducible]

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)

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.

@[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

@[implicit_reducible]

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

@[simp]

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

@[simp]

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

@[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

@[implicit_reducible]

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

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)

@[implicit_reducible]

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)

Algebra structure

@[implicit_reducible]

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)

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.

@[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] (a : Unitization R A) : (fstHom R A) a = a.toProd.1

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.

@[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

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.

@[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.

@[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✝).toProd.2

@[simp]

theorem Unitization.inrRangeEquiv_apply_coe_fst (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)).toProd.1 = 0

@[simp]

theorem Unitization.inrRangeEquiv_apply_coe_snd (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)).toProd.2 = 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.

@[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.toProd.1 + φ x.toProd.2

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.

@[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

@[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)

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) = fun (x : Unitization R A) => x.toProd.1

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.

@[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 {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_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)).

@[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.toProd.1 + ↑(φ x.toProd.2)

@[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.

theorem Unitization.isStarProjection_inr_iff {R : Type u_1} {A : Type u_2} [Semiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] {p : A} : IsStarProjection ↑p ↔ IsStarProjection p

theorem IsStarProjection.inr {R : Type u_1} {A : Type u_2} [Semiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] {p : A} : IsStarProjection p → IsStarProjection ↑p

Alias of the reverse direction of Unitization.isStarProjection_inr_iff.

theorem IsStarProjection.of_inr {R : Type u_1} {A : Type u_2} [Semiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] {p : A} : IsStarProjection ↑p → IsStarProjection p

Alias of the forward direction of Unitization.isStarProjection_inr_iff.