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.instCoeTCUnitization {R : Type u_1} {A : Type u_2} [Zero R] : CoeTC A (Unitization R A)

Equations

• Unitization.instCoeTCUnitization = { 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

• Unitization.fst x = 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

• Unitization.snd x = x.2

theorem Unitization.ext {R : Type u_1} {A : Type u_2} {x : Unitization R A} {y : Unitization R A} (h1 : Unitization.fst x = Unitization.fst y) (h2 : Unitization.snd x = Unitization.snd y) : x = y

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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] : Unitization.fst 0 = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[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) : Unitization.fst (s • x) = s • Unitization.fst x

@[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) : Unitization.snd (s • x) = s • Unitization.snd x

@[simp]

theorem Unitization.inl_zero {R : Type u_3} (A : Type u_4) [Zero R] [Zero A] : Unitization.inl 0 = 0

@[simp]

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

@[simp]

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

@[simp]

theorem Unitization.inl_smul {S : Type u_2} {R : Type u_3} (A : Type u_4) [Monoid S] [AddMonoid A] [SMul S R] [DistribMulAction S A] (s : S) (r : R) : Unitization.inl (s • r) = s • Unitization.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₁ : A) (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_smul {S : Type u_2} (R : Type u_3) {A : Type u_4} [Zero R] [Zero S] [SMulWithZero 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) : Unitization.inl (Unitization.fst x) + ↑(Unitization.snd x) = x

theorem Unitization.ind {R : Type u_5} {A : Type u_6} [AddZeroClass R] [AddZeroClass A] {P : Unitization R A → Prop} (h : ∀ (r : R) (a : A), P (Unitization.inl r + ↑a)) (x : Unitization R A) : P x

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

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

theorem Unitization.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 : Unitization R A →ₗ[S] N⦄ ⦃g : Unitization R A →ₗ[S] N⦄ (hl : ∀ (r : R), f (Unitization.inl r) = g (Unitization.inl r)) (hr : ∀ (a : A), f ↑a = g ↑a) : f = g

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

@[simp]

theorem Unitization.inrHom_apply (R : Type u_3) (A : Type u_4) [Semiring R] [AddCommMonoid A] [Module R A] (a : A) : (Unitization.inrHom R A) a = ↑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 = let __src := LinearMap.inr R R A; { toAddHom := { toFun := Unitization.inr, 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) : (Unitization.sndHom R A) x = Unitization.snd x

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 = let __src := LinearMap.snd R R A; { toAddHom := { toFun := Unitization.snd, map_add' := ⋯ }, map_smul' := ⋯ }

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] : Unitization.fst 1 = 1

@[simp]

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

@[simp]

theorem Unitization.snd_mul {R : Type u_1} {A : Type u_2} [Mul R] [Add A] [Mul A] [SMul R A] (x₁ : Unitization R A) (x₂ : Unitization R A) : Unitization.snd (x₁ * x₂) = Unitization.fst x₁ • Unitization.snd x₂ + Unitization.fst x₂ • Unitization.snd x₁ + Unitization.snd x₁ * Unitization.snd x₂

@[simp]

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

@[simp]

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

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

@[simp]

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

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

theorem Unitization.inr_mul_inl {R : Type u_1} {A : Type u_2} [Semiring R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] (r : R) (a : A) : ↑a * Unitization.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 = let __src := Unitization.instOne; let __src_1 := Unitization.instMul; MulOneClass.mk ⋯ ⋯

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

Equations

• Unitization.instNonAssocSemiring = let __src := Unitization.instMulOneClass; let __src_1 := Unitization.instAddCommMonoid; NonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

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

• Unitization.instMonoid = let __src := Unitization.instMulOneClass; Monoid.mk ⋯ ⋯ npowRec ⋯ ⋯

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 = let __src := Unitization.instMonoid; CommMonoid.mk ⋯

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

• 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} [CommSemiring R] [NonUnitalCommSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : CommSemiring (Unitization R A)

Equations

• Unitization.instCommSemiring = let __src := Unitization.instCommMonoid; let __src_1 := Unitization.instNonAssocSemiring; CommSemiring.mk ⋯

instance Unitization.instNonAssocRing {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] : NonAssocRing (Unitization 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} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : Ring (Unitization R A)

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} [CommRing R] [NonUnitalCommRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : CommRing (Unitization R A)

Equations

• Unitization.instCommRing = let __src := Unitization.instAddCommGroup; let __src_1 := Unitization.instCommSemiring; CommRing.mk ⋯

@[simp]

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

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 = { toMonoidHom := { toOneHom := { toFun := Unitization.inl, map_one' := ⋯ }, map_mul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

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 (Unitization.fst ra), star (Unitization.snd ra)) }

@[simp]

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

@[simp]

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

@[simp]

theorem Unitization.inl_star {R : Type u_1} {A : Type u_2} [Star R] [AddMonoid A] [StarAddMonoid A] (r : R) : Unitization.inl (star r) = star (Unitization.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 = StarAddMonoid.mk ⋯

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)

Equations

• ⋯ = ⋯

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 = let __src := Unitization.instStarAddMonoid; StarRing.mk ⋯

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 = let __src := RingHom.comp (Unitization.inlRingHom R A) (algebraMap S R); Algebra.mk __src ⋯ ⋯

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)) = Unitization.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) = RingHom.comp (Unitization.inlRingHom R A) (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)) = Unitization.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) = Unitization.inlRingHom R A

@[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) : (Unitization.fstHom R A) x = Unitization.fst x

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

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

@[simp]

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

@[simp]

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

def Unitization.inrNonUnitalAlgHom (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalSemiring A] [Module R A] : A →ₛₙₐ[MonoidHom.id 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 = { toDistribMulActionHom := { toMulActionHom := { toFun := Unitization.inr, map_smul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }, map_mul' := ⋯ }

@[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) : (Unitization.inrNonUnitalStarAlgHom 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' := ⋯ }

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} {ψ : 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} {ψ : 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} {ψ : Unitization R A →ₐ[R] C} (h : NonUnitalAlgHom.comp (↑φ) (Unitization.inrNonUnitalAlgHom R A) = NonUnitalAlgHom.comp (↑ψ) (Unitization.inrNonUnitalAlgHom R A)) : φ = ψ

See note [partially-applied ext lemmas]

@[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 →ₛₙₐ[MonoidHom.id R] C) (x : Unitization R A) : (NonUnitalAlgHom.toAlgHom φ) x = (algebraMap R C) (Unitization.fst x) + φ (Unitization.snd x)

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 →ₛₙₐ[MonoidHom.id 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

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

@[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 →ₛₙₐ[MonoidHom.id R] C) : Unitization.lift φ = NonUnitalAlgHom.toAlgHom φ

@[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 →ₛₙₐ[MonoidHom.id R] C) (x : Unitization R A) : (Unitization.lift φ) x = (algebraMap R C) (Unitization.fst x) + φ (Unitization.snd x)

@[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) : Unitization.lift.symm φ = NonUnitalAlgHom.comp (NonUnitalAlgHomClass.toNonUnitalAlgHom φ) (Unitization.inrNonUnitalAlgHom R A)

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 →ₛₙₐ[MonoidHom.id 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

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

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) : (Unitization.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] : ⇑(NonUnitalAlgHom.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} {ψ : Unitization R A →⋆ₐ[R] C} (h : NonUnitalStarAlgHom.comp (↑φ) (Unitization.inrNonUnitalStarAlgHom R A) = NonUnitalStarAlgHom.comp (↑ψ) (Unitization.inrNonUnitalStarAlgHom R A)) : φ = ψ

See note [partially-applied ext lemmas]

@[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) : (Unitization.starLift φ) x = (algebraMap R C) (Unitization.fst x) + φ (Unitization.snd x)

@[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) : Unitization.starLift.symm φ = NonUnitalStarAlgHom.comp (StarAlgHom.toNonUnitalStarAlgHom φ) (Unitization.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) : Unitization.starLift φ = { toAlgHom := NonUnitalAlgHom.toAlgHom φ.toNonUnitalAlgHom, map_star' := ⋯ }

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_symm_apply_apply {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [Semiring C] [Algebra R C] (φ : Unitization R A →ₐ[R] C) (a : A) : (Unitization.lift.symm φ) a = φ ↑a