Documentation

Mathlib.Algebra.Algebra.Unitization

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 algebra.unitization R A is a type synonym for R × A on which we place a different multiplicative structure, namely, (r₁, a₁) * (r₂, a₂) = (r₁ * r₂, r₁ • a₂ + r₂ • a₁ + a₁ * a₂) where the multiplicative identity is (1, 0).

Note, when A is a unital R-algebra, then Unitization R A constructs a new multiplicative identity different from the old one, and so in general Unitization R A and A will not be isomorphic even in the unital case. This approach actually has nice functorial properties.

There is a natural coercion from A to Unitization R A given by 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.

Instances For

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.

Instances For

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.

Instances For

instance Unitization.instCoeTCUnitization {R : Type u_1} {A : Type u_2} [Zero R] :

CoeTC A (Unitization R A)

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

R

The canonical projection Unitization R A → R.

Instances For

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

A

The canonical projection Unitization R A → A.

Instances For

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)

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.instInhabited {R : Type u_3} {A : Type u_4} [Inhabited R] [Inhabited A] :

Inhabited (Unitization R A)

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

Zero (Unitization R A)

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

Add (Unitization R A)

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

Neg (Unitization R A)

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

AddSemigroup (Unitization R A)

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

AddZeroClass (Unitization R A)

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

AddMonoid (Unitization R A)

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

AddGroup (Unitization R A)

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

AddCommSemigroup (Unitization R A)

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

AddCommMonoid (Unitization R A)

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

AddCommGroup (Unitization R A)

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)

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)

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)

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.

Instances For

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

Instances For

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

Instances For

Multiplicative structure #

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

One (Unitization R A)

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] :

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)

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

NonAssocSemiring (Unitization R A)

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)

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)

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)

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)

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

NonAssocRing (Unitization R A)

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)

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)

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

Instances For

Star structure #

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) :

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)

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)

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)

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.

Instances For

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

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

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.

Instances For

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

Instances For

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} [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} [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 →ₙₐ[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 →ₙₐ[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.

Instances For

@[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 (↑φ) (Unitization.inrNonUnitalAlgHom R A)

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

↑(↑Unitization.lift φ) x = ↑(algebraMap R C) (Unitization.fst x) + ↑φ (Unitization.snd x)

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

↑Unitization.lift φ = NonUnitalAlgHom.toAlgHom φ

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.

Instances For

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 {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' := (_ : ∀ (x : Unitization R A), OneHom.toFun (↑↑↑(↑Unitization.lift φ.toNonUnitalAlgHom)) (star x) = star (OneHom.toFun (↑↑↑(↑Unitization.lift φ.toNonUnitalAlgHom)) x)) }

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

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.

Instances For

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