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 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 #

Main results #

TODO #

def Unitization (R : Type u_1) (A : Type u_2) :
Type (max u_1 u_2)

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

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

    The canonical inclusion R → Unitization R A.

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

      The canonical inclusion A → Unitization R A.

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

        The canonical projection Unitization R A → R.

        Equations
        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.

          Equations
          Instances For
            theorem Unitization.ext {R : Type u_1} {A : Type u_2} {x y : Unitization R A} (h1 : x.fst = y.fst) (h2 : x.snd = y.snd) :
            x = y
            @[simp]
            theorem Unitization.fst_inl {R : Type u_1} (A : Type u_2) [Zero A] (r : R) :
            (inl r).fst = r
            @[simp]
            theorem Unitization.snd_inl {R : Type u_1} (A : Type u_2) [Zero A] (r : R) :
            (inl r).snd = 0
            @[simp]
            theorem Unitization.fst_inr (R : Type u_1) {A : Type u_2} [Zero R] (a : A) :
            (↑a).fst = 0
            @[simp]
            theorem Unitization.snd_inr (R : Type u_1) {A : Type u_2} [Zero R] (a : A) :
            (↑a).snd = a
            instance Unitization.instNontrivialLeft {𝕜 : Type u_3} {A : Type u_4} [Nontrivial 𝕜] [Nonempty A] :
            instance Unitization.instNontrivialRight {𝕜 : Type u_3} {A : Type u_4} [Nonempty 𝕜] [Nontrivial A] :

            Structures inherited from Prod #

            Additive operators and scalar multiplication operate elementwise.

            instance Unitization.instCanLift {R : Type u_3} {A : Type u_4} [Zero R] :
            CanLift (Unitization R A) A inr fun (x : Unitization R A) => x.fst = 0
            instance Unitization.instZero {R : Type u_3} {A : Type u_4} [Zero R] [Zero A] :
            Equations
            instance Unitization.instAdd {R : Type u_3} {A : Type u_4} [Add R] [Add A] :
            Equations
            instance Unitization.instNeg {R : Type u_3} {A : Type u_4} [Neg R] [Neg A] :
            Equations
            instance Unitization.instSMul {S : Type u_2} {R : Type u_3} {A : Type u_4} [SMul S R] [SMul S A] :
            Equations
            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] :
            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] :
            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] :
            def Unitization.addEquiv (R : Type u_3) (A : Type u_4) [Add R] [Add A] :

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

            Equations
            Instances For
              @[simp]
              theorem Unitization.fst_zero {R : Type u_3} {A : Type u_4} [Zero R] [Zero A] :
              fst 0 = 0
              @[simp]
              theorem Unitization.snd_zero {R : Type u_3} {A : Type u_4} [Zero R] [Zero A] :
              snd 0 = 0
              @[simp]
              theorem Unitization.fst_add {R : Type u_3} {A : Type u_4} [Add R] [Add A] (x₁ x₂ : Unitization R A) :
              (x₁ + x₂).fst = x₁.fst + x₂.fst
              @[simp]
              theorem Unitization.snd_add {R : Type u_3} {A : Type u_4} [Add R] [Add A] (x₁ x₂ : Unitization R A) :
              (x₁ + x₂).snd = x₁.snd + x₂.snd
              @[simp]
              theorem Unitization.fst_neg {R : Type u_3} {A : Type u_4} [Neg R] [Neg A] (x : Unitization R A) :
              (-x).fst = -x.fst
              @[simp]
              theorem Unitization.snd_neg {R : Type u_3} {A : Type u_4} [Neg R] [Neg A] (x : Unitization R A) :
              (-x).snd = -x.snd
              @[simp]
              theorem Unitization.fst_smul {S : Type u_2} {R : Type u_3} {A : Type u_4} [SMul S R] [SMul S A] (s : S) (x : Unitization R A) :
              (s x).fst = s x.fst
              @[simp]
              theorem Unitization.snd_smul {S : Type u_2} {R : Type u_3} {A : Type u_4} [SMul S R] [SMul S A] (s : S) (x : Unitization R A) :
              (s x).snd = s x.snd
              @[simp]
              theorem Unitization.inl_zero {R : Type u_3} (A : Type u_4) [Zero R] [Zero A] :
              inl 0 = 0
              @[simp]
              theorem Unitization.inl_add {R : Type u_3} (A : Type u_4) [Add R] [AddZeroClass A] (r₁ r₂ : R) :
              inl (r₁ + r₂) = inl r₁ + inl r₂
              @[simp]
              theorem Unitization.inl_neg {R : Type u_3} (A : Type u_4) [Neg R] [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) [Monoid S] [AddMonoid A] [SMul S R] [DistribMulAction 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] [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) :
              inl x.fst + x.snd = x
              theorem Unitization.ind {R : Type u_5} {A : Type u_6} [AddZeroClass R] [AddZeroClass A] {P : Unitization R AProp} (inl_add_inr : ∀ (r : R) (a : A), P (inl r + a)) (x : Unitization R A) :
              P x

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

              This can be used as induction x.

              theorem Unitization.linearMap_ext {S : Type u_2} {R : Type u_3} {A : Type u_4} {N : Type u_5} [Semiring S] [AddCommMonoid R] [AddCommMonoid A] [AddCommMonoid N] [Module S R] [Module S A] [Module S N] ⦃f g : Unitization R A →ₗ[S] N (hl : ∀ (r : R), f (inl r) = g (inl r)) (hr : ∀ (a : A), f a = g a) :
              f = g

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

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

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

              Equations
              Instances For
                @[simp]
                theorem Unitization.inrHom_apply (R : Type u_3) (A : Type u_4) [Semiring R] [AddCommMonoid A] [Module R A] (a : A) :
                (inrHom R A) a = a
                def Unitization.sndHom (R : Type u_3) (A : Type u_4) [Semiring R] [AddCommMonoid A] [Module R A] :

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

                Equations
                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) :
                  (sndHom R A) x = x.snd

                  Multiplicative structure #

                  instance Unitization.instOne {R : Type u_1} {A : Type u_2} [One R] [Zero A] :
                  Equations
                  instance Unitization.instMul {R : Type u_1} {A : Type u_2} [Mul R] [Add A] [Mul A] [SMul R A] :
                  Equations
                  @[simp]
                  theorem Unitization.fst_one {R : Type u_1} {A : Type u_2} [One R] [Zero A] :
                  fst 1 = 1
                  @[simp]
                  theorem Unitization.snd_one {R : Type u_1} {A : Type u_2} [One R] [Zero A] :
                  snd 1 = 0
                  @[simp]
                  theorem Unitization.fst_mul {R : Type u_1} {A : Type u_2} [Mul R] [Add A] [Mul A] [SMul R A] (x₁ x₂ : Unitization R A) :
                  (x₁ * x₂).fst = x₁.fst * x₂.fst
                  @[simp]
                  theorem Unitization.snd_mul {R : Type u_1} {A : Type u_2} [Mul R] [Add A] [Mul A] [SMul R A] (x₁ x₂ : Unitization R A) :
                  (x₁ * x₂).snd = x₁.fst x₂.snd + x₂.fst x₁.snd + x₁.snd * x₂.snd
                  @[simp]
                  theorem Unitization.inl_one {R : Type u_1} (A : Type u_2) [One R] [Zero A] :
                  inl 1 = 1
                  @[simp]
                  theorem Unitization.inl_mul {R : Type u_1} (A : Type u_2) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction 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) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction 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} [Semiring R] [AddCommMonoid 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} [Semiring R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] (r : R) (a : A) :
                  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 * inl r = ↑(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] :
                  Equations
                  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] :
                  Equations
                  def Unitization.inlRingHom (R : Type u_1) (A : Type u_2) [Semiring R] [NonUnitalSemiring A] [Module R A] :

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

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

                    Star structure #

                    instance Unitization.instStar {R : Type u_1} {A : Type u_2} [Star R] [Star A] :
                    Equations
                    @[simp]
                    theorem Unitization.fst_star {R : Type u_1} {A : Type u_2} [Star R] [Star A] (x : Unitization R A) :
                    (star x).fst = star x.fst
                    @[simp]
                    theorem Unitization.snd_star {R : Type u_1} {A : Type u_2} [Star R] [Star A] (x : Unitization R A) :
                    (star x).snd = star x.snd
                    @[simp]
                    theorem Unitization.inl_star {R : Type u_1} {A : Type u_2} [Star R] [AddMonoid A] [StarAddMonoid A] (r : R) :
                    inl (star r) = star (inl r)
                    @[simp]
                    theorem Unitization.inr_star {R : Type u_1} {A : Type u_2} [AddMonoid R] [StarAddMonoid R] [Star A] (a : A) :
                    (star a) = star a

                    Algebra structure #

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

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

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

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

                      Equations
                      Instances For
                        @[simp]
                        theorem Unitization.inrNonUnitalAlgHom_toFun (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalSemiring A] [Module R A] (a : A) :
                        (inrNonUnitalAlgHom R A) a = a
                        @[simp]
                        theorem Unitization.inrNonUnitalAlgHom_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalSemiring A] [Module R A] (a : A) :
                        (inrNonUnitalAlgHom R A) a = a

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

                        Equations
                        Instances For
                          @[simp]

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

                          Equations
                          Instances For
                            @[simp]
                            theorem Unitization.inrRangeEquiv_apply_coe (R : Type u_1) (A : Type u_2) [CommSemiring R] [StarAddMonoid R] [NonUnitalSemiring A] [Star A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (a : A) :
                            ((inrRangeEquiv R A) a) = (inrNonUnitalStarAlgHom R A) a
                            @[simp]
                            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]

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

                            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
                            Instances For
                              @[simp]
                              theorem NonUnitalAlgHom.toAlgHom_apply {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {C : Type u_5} [Semiring C] [Algebra R C] (φ : A →ₙₐ[R] C) (x : Unitization R A) :
                              φ.toAlgHom x = (algebraMap R C) x.fst + φ x.snd
                              def Unitization.lift {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {C : Type u_5} [Semiring C] [Algebra R C] :

                              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
                              Instances For
                                @[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) :
                                @[simp]
                                theorem Unitization.lift_apply_apply {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {C : Type u_5} [Semiring C] [Algebra R C] (φ : A →ₙₐ[R] C) (x : Unitization R A) :
                                (lift φ) x = (algebraMap R C) x.fst + φ x.snd
                                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
                                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]

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

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

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[simp]
                                  theorem Unitization.starLift_apply_apply {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [Semiring C] [Algebra R C] [StarRing C] [StarModule R C] (φ : A →⋆ₙₐ[R] C) (x : Unitization R A) :
                                  (starLift φ) x = (algebraMap R C) x.fst + φ x.snd
                                  @[simp]
                                  theorem Unitization.starLift_apply {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [Semiring C] [Algebra R C] [StarRing C] [StarModule R C] (φ : A →⋆ₙₐ[R] C) :
                                  starLift φ = { toAlgHom := φ.toAlgHom, map_star' := }
                                  @[simp]
                                  theorem Unitization.starLift_symm_apply_apply {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [Semiring C] [Algebra R C] [StarRing C] [StarModule R C] (φ : Unitization R A →⋆ₐ[R] C) (a : A) :
                                  (starLift.symm φ) a = φ a
                                  def Unitization.starMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalSemiring B] [StarRing B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] [StarModule R B] (φ : A →⋆ₙₐ[R] B) :

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

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

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem Unitization.starMap_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalSemiring B] [StarRing B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] [StarModule R B] (φ : A →⋆ₙₐ[R] B) (x : Unitization R A) :
                                    (starMap φ) x = (algebraMap R (Unitization R B)) x.fst + (φ x.snd)
                                    @[simp]
                                    theorem Unitization.starMap_inr {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalSemiring B] [StarRing B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] [StarModule R B] (φ : A →⋆ₙₐ[R] B) (a : A) :
                                    (starMap φ) a = (φ a)
                                    @[simp]
                                    theorem Unitization.starMap_inl {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalSemiring B] [StarRing B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] [StarModule R B] (φ : A →⋆ₙₐ[R] B) (r : R) :
                                    (starMap φ) (inl r) = (algebraMap R (Unitization R B)) r
                                    theorem Unitization.starMap_injective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalSemiring B] [StarRing B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] [StarModule R B] {φ : A →⋆ₙₐ[R] B} (hφ : Function.Injective φ) :

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

                                    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]

                                    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} :
                                    theorem IsSelfAdjoint.of_inr {R : Type u_1} {A : Type u_2} [Semiring R] [StarAddMonoid R] [Star A] {a : 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) :
                                    @[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] :
                                    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] :

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