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
      • a = (0, a)
      Instances For
        instance Unitization.instCoeTCOfZero {R : Type u_1} {A : Type u_2} [Zero R] :
        Equations
        • Unitization.instCoeTCOfZero = { coe := Unitization.inr }
        def Unitization.fst {R : Type u_1} {A : Type u_2} (x : Unitization R A) :
        R

        The canonical projection Unitization R A → R.

        Equations
        • x.fst = x.1
        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
          • x.snd = x.2
          Instances For
            theorem Unitization.ext {R : Type u_1} {A : Type u_2} {x : Unitization R A} {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) :
            (Unitization.inl r).fst = r
            @[simp]
            theorem Unitization.snd_inl {R : Type u_1} (A : Type u_2) [Zero A] (r : R) :
            (Unitization.inl r).snd = 0
            @[simp]
            theorem Unitization.fst_inr (R : Type u_1) {A : Type u_2} [Zero R] (a : A) :
            (a).fst = 0
            @[simp]
            theorem Unitization.snd_inr (R : Type u_1) {A : Type u_2} [Zero R] (a : A) :
            (a).snd = a
            theorem Unitization.inl_injective {R : Type u_1} {A : Type u_2} [Zero A] :
            Function.Injective 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] :
            Equations
            • =
            instance Unitization.instNontrivialRight {𝕜 : Type u_3} {A : Type u_4} [Nonempty 𝕜] [Nontrivial 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) => x.fst = 0
            Equations
            • =
            instance Unitization.instInhabited {R : Type u_3} {A : Type u_4} [Inhabited R] [Inhabited A] :
            Equations
            • Unitization.instInhabited = instInhabitedProd
            instance Unitization.instZero {R : Type u_3} {A : Type u_4} [Zero R] [Zero A] :
            Equations
            • Unitization.instZero = Prod.instZero
            instance Unitization.instAdd {R : Type u_3} {A : Type u_4} [Add R] [Add A] :
            Equations
            • Unitization.instAdd = Prod.instAdd
            instance Unitization.instNeg {R : Type u_3} {A : Type u_4} [Neg R] [Neg A] :
            Equations
            • Unitization.instNeg = Prod.instNeg
            Equations
            • Unitization.instAddSemigroup = Prod.instAddSemigroup
            Equations
            • Unitization.instAddZeroClass = Prod.instAddZeroClass
            instance Unitization.instAddMonoid {R : Type u_3} {A : Type u_4} [AddMonoid R] [AddMonoid A] :
            Equations
            • Unitization.instAddMonoid = Prod.instAddMonoid
            instance Unitization.instAddGroup {R : Type u_3} {A : Type u_4} [AddGroup R] [AddGroup A] :
            Equations
            • Unitization.instAddGroup = Prod.instAddGroup
            Equations
            • Unitization.instAddCommSemigroup = Prod.instAddCommSemigroup
            Equations
            • Unitization.instAddCommMonoid = Prod.instAddCommMonoid
            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] :
            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] :
            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] :
            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] :
            Equations
            • =
            instance Unitization.instMulAction {S : Type u_2} {R : Type u_3} {A : Type u_4} [Monoid S] [MulAction S R] [MulAction S A] :
            Equations
            • Unitization.instMulAction = Prod.mulAction
            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] :
            Equations
            • Unitization.instModule = Prod.instModule
            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] :
              @[simp]
              theorem Unitization.snd_zero {R : Type u_3} {A : Type u_4} [Zero R] [Zero A] :
              @[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) :
              (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₁ : Unitization R A) (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] :
              @[simp]
              theorem Unitization.inl_add {R : Type u_3} (A : Type u_4) [Add R] [AddZeroClass A] (r₁ : R) (r₂ : R) :
              @[simp]
              theorem Unitization.inl_neg {R : Type u_3} (A : Type u_4) [Neg R] [AddGroup A] (r : 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) :
              @[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 x.fst + x.snd = x
              theorem Unitization.ind {R : Type u_5} {A : Type u_6} [AddZeroClass R] [AddZeroClass A] {P : Unitization R AProp} (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] :

              The canonical R-linear inclusion A → Unitization R 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) :
                (Unitization.sndHom R A) x = x.snd
                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

                  Multiplicative structure #

                  instance Unitization.instOne {R : Type u_1} {A : Type u_2} [One R] [Zero 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] :
                  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] :
                  @[simp]
                  theorem Unitization.snd_one {R : Type u_1} {A : Type u_2} [One R] [Zero A] :
                  @[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) :
                  (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₁ : Unitization R A) (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] :
                  @[simp]
                  theorem Unitization.inl_mul {R : Type u_1} (A : Type u_2) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] (r₁ : R) (r₂ : 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) :
                  @[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)
                  Equations
                  • Unitization.instMulOneClass = let __src := Unitization.instOne; let __src_1 := Unitization.instMul; MulOneClass.mk
                  Equations
                  • Unitization.instNonAssocSemiring = let __src := Unitization.instMulOneClass; let __src_1 := Unitization.instAddCommMonoid; NonAssocSemiring.mk
                  Equations
                  • Unitization.instMonoid = let __src := Unitization.instMulOneClass; Monoid.mk npowRec
                  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] :
                  Equations
                  • Unitization.instSemiring = let __src := Unitization.instMonoid; let __src_1 := Unitization.instNonAssocSemiring; Semiring.mk Monoid.npow
                  Equations
                  • Unitization.instCommSemiring = let __src := Unitization.instCommMonoid; let __src_1 := Unitization.instNonAssocSemiring; CommSemiring.mk
                  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] :
                  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] :
                  Equations
                  • Unitization.instCommRing = let __src := Unitization.instAddCommGroup; let __src_1 := Unitization.instCommSemiring; CommRing.mk
                  @[simp]
                  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
                  • Unitization.inlRingHom R A = { toFun := Unitization.inl, map_one' := , map_mul' := , map_zero' := , map_add' := }
                  Instances For

                    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) :
                    @[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
                    Equations
                    Equations
                    • =
                    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] :
                    Equations
                    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_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
                    @[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 = x.fst
                    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
                    • Unitization.fstHom R A = { toFun := Unitization.fst, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
                    Instances For
                      @[simp]
                      @[simp]

                      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

                        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
                          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 : (φ).comp (Unitization.inrNonUnitalAlgHom R A) = (ψ).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) :
                          φ.toAlgHom x = (algebraMap R C) x.fst + φ x.snd
                          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
                          • φ.toAlgHom = { toFun := fun (x : Unitization R A) => (algebraMap R C) x.fst + φ x.snd, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
                          Instances For
                            @[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) x.fst + φ x.snd
                            @[simp]
                            theorem Unitization.lift_symm_apply {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {C : Type u_5} [Semiring C] [Algebra R C] (φ : Unitization R A →ₐ[R] C) :
                            @[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 φ = φ.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] :

                            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
                              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 : (φ).comp (Unitization.inrNonUnitalStarAlgHom R A) = (ψ).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 := φ.toAlgHom, map_star' := }
                              @[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) x.fst + φ x.snd
                              @[simp]
                              theorem Unitization.starLift_symm_apply {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [Semiring C] [Algebra R C] [StarRing C] [StarModule R C] (φ : Unitization R A →⋆ₐ[R] C) :
                              Unitization.starLift.symm φ = φ.toNonUnitalStarAlgHom.comp (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] :

                              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_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
                                @[simp]
                                theorem Unitization.isStarNormal_inr {R : Type u_1} {A : Type u_2} [Semiring R] [AddCommMonoid A] [Mul A] [SMulWithZero R A] [StarAddMonoid R] [Star A] {a : A} :
                                instance Unitization.instIsStarNormal (R : Type u_1) {A : Type u_2} [Semiring R] [AddCommMonoid A] [Mul A] [SMulWithZero R A] [StarAddMonoid R] [Star A] (a : A) [IsStarNormal a] :
                                Equations
                                • =
                                @[simp]
                                theorem Unitization.isSelfAdjoint_inr {R : Type u_1} {A : Type u_2} [Semiring R] [StarAddMonoid R] [Star A] {a : A} :
                                theorem IsSelfAdjoint.inr (R : Type u_1) {A : Type u_2} [Semiring R] [StarAddMonoid R] [Star A] {a : A} (ha : IsSelfAdjoint 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 IsStarNormal.of_inr {R : Type u_1} {A : Type u_2} [Semiring R] [AddCommMonoid A] [Mul A] [SMulWithZero R A] [StarAddMonoid R] [Star A] {a : A} :

                                Alias of the forward direction of Unitization.isStarNormal_inr.