# Unitization norms #

Given a not-necessarily-unital normed `๐`

-algebra `A`

, it is frequently of interest to equip its
`Unitization`

with a norm which simultaneously makes it into a normed algebra and also satisfies
two properties:

`โ1โ = 1`

(i.e.,`NormOneClass`

)- The embedding of
`A`

in`Unitization ๐ A`

is an isometry. (i.e.,`Isometry Unitization.inr`

)

One way to do this is to pull back the norm from `WithLp 1 (๐ ร A)`

, that is,
`โ(k, a)โ = โkโ + โaโ`

using `Unitization.addEquiv`

(i.e., the identity map).
This is implemented for the type synonym `WithLp 1 (Unitization ๐ A)`

in
`WithLp.instUnitizationNormedAddCommGroup`

, and it is shown there that this is a Banach algebra.
However, when the norm on `A`

is *regular* (i.e., `ContinuousLinearMap.mul`

is an isometry), there
is another natural choice: the pullback of the norm on `๐ ร (A โL[๐] A)`

under the map
`(k, a) โฆ (k, k โข 1 + ContinuousLinearMap.mul ๐ A a)`

. It turns out that among all norms on the
unitization satisfying the properties specified above, the norm inherited from
`WithLp 1 (๐ ร A)`

is maximal, and the norm inherited from this pullback is minimal.
Of course, this means that `WithLp.equiv : WithLp 1 (Unitization ๐ A) โ Unitization ๐ A`

can be
upgraded to a continuous linear equivalence (when `๐`

and `A`

are complete).

structure on `Unitization ๐ A`

using the pullback described above. The reason for choosing this norm
is that for a Cโ-algebra `A`

its norm is always regular, and the pullback norm on `Unitization ๐ A`

is then also a Cโ-norm.

## Main definitions #

`Unitization.splitMul : Unitization ๐ A โโ[๐] (๐ ร (A โL[๐] A))`

: The first coordinate of this map is just`Unitization.fst`

and the second is the`Unitization.lift`

of the left regular representation of`A`

(i.e.,`NonUnitalAlgHom.Lmul`

). We use this map to pull back the`NormedRing`

and`NormedAlgebra`

structures.

## Main statements #

`Unitization.instNormedRing`

,`Unitization.instNormedAlgebra`

,`Unitization.instNormOneClass`

,`Unitization.instCompleteSpace`

: when`A`

is a non-unital Banach`๐`

-algebra with a regular norm, then`Unitization ๐ A`

is a unital Banach`๐`

-algebra with`โ1โ = 1`

.`Unitization.norm_inr`

,`Unitization.isometry_inr`

: the natural inclusion`A โ Unitization ๐ A`

is an isometry, or in mathematical parlance, the norm on`A`

extends to a norm on`Unitization ๐ A`

.

## Implementation details #

We ensure that the uniform structure, and hence also the topological structure, is definitionally
equal to the pullback of `instUniformSpaceProd`

along `Unitization.addEquiv`

(this is essentially
viewing `Unitization ๐ A`

as `๐ ร A`

) by means of forgetful inheritance. The same is true of the
bornology.

Given `(k, a) : Unitization ๐ A`

, the second coordinate of `Unitization.splitMul (k, a)`

is
the natural representation of `Unitization ๐ A`

on `A`

given by multiplication on the left in
`A โL[๐] A`

; note that this is not just `NonUnitalAlgHom.Lmul`

for a few reasons: (a) that would
either be `A`

acting on `A`

, or (b) `Unitization ๐ A`

acting on `Unitization ๐ A`

, and (c) that's a
`NonUnitalAlgHom`

but here we need an `AlgHom`

. In addition, the first coordinate of
`Unitization.splitMul (k, a)`

should just be `k`

. See `Unitization.splitMul_apply`

also.

## Equations

- Unitization.splitMul ๐ A = (Unitization.lift 0).prod (Unitization.lift (NonUnitalAlgHom.Lmul ๐ A))

## Instances For

this lemma establishes that if `ContinuousLinearMap.mul ๐ A`

is injective, then so is
`Unitization.splitMul ๐ A`

. When `A`

is a `RegularNormedAlgebra`

, then
`ContinuousLinearMap.mul ๐ A`

is an isometry, and is therefore automatically injective.

In a `RegularNormedAlgebra`

, the map `Unitization.splitMul ๐ A`

is injective.
We will use this to pull back the norm from `๐ ร (A โL[๐] A)`

to `Unitization ๐ A`

.

Pull back the normed ring structure from `๐ ร (A โL[๐] A)`

to `Unitization ๐ A`

using the
algebra homomorphism `Unitization.splitMul ๐ A`

. This does not give us the desired topology,
uniformity or bornology on `Unitization ๐ A`

(which we want to agree with `Prod`

), so we only use
it as a local instance to build the real one.

## Equations

- Unitization.normedRingAux = NormedRing.induced (Unitization ๐ A) (๐ ร (A โL[๐] A)) (Unitization.splitMul ๐ A) โฏ

## Instances For

Pull back the normed algebra structure from `๐ ร (A โL[๐] A)`

to `Unitization ๐ A`

using the
algebra homomorphism `Unitization.splitMul ๐ A`

. This uses the wrong `NormedRing`

instance (i.e.,
`Unitization.normedRingAux`

), so we only use it as a local instance to build the real one.

## Equations

- Unitization.normedAlgebraAux = NormedAlgebra.induced ๐ (Unitization ๐ A) (๐ ร (A โL[๐] A)) (Unitization.splitMul ๐ A)

## Instances For

This is often the more useful lemma to rewrite the norm as opposed to `Unitization.norm_def`

.

This is often the more useful lemma to rewrite the norm as opposed to
`Unitization.nnnorm_def`

.

The uniformity on `Unitization ๐ A`

is inherited from `๐ ร A`

.

## Equations

- Unitization.instUniformSpace = UniformSpace.comap (โ(Unitization.addEquiv ๐ A)) instUniformSpaceProd

The natural equivalence between `Unitization ๐ A`

and `๐ ร A`

as a uniform equivalence.

## Equations

- Unitization.uniformEquivProd = (โ(Unitization.addEquiv ๐ A)).toUniformEquivOfUniformInducing โฏ

## Instances For

The bornology on `Unitization ๐ A`

is inherited from `๐ ร A`

.

## Equations

- Unitization.instBornology = Bornology.induced โ(Unitization.addEquiv ๐ A)

**Alias** of `Unitization.isUniformEmbedding_addEquiv`

.

`Unitization ๐ A`

is complete whenever `๐`

and `A`

are also.

## Equations

- โฏ = โฏ

Pull back the metric structure from `๐ ร (A โL[๐] A)`

to `Unitization ๐ A`

using the
algebra homomorphism `Unitization.splitMul ๐ A`

, but replace the bornology and the uniformity so
that they coincide with `๐ ร A`

.

## Equations

- Unitization.instMetricSpace = (NormedRing.toMetricSpace.replaceUniformity โฏ).replaceBornology โฏ

Pull back the normed ring structure from `๐ ร (A โL[๐] A)`

to `Unitization ๐ A`

using the
algebra homomorphism `Unitization.splitMul ๐ A`

.

## Equations

- Unitization.instNormedRing = NormedRing.mk โฏ โฏ

Pull back the normed algebra structure from `๐ ร (A โL[๐] A)`

to `Unitization ๐ A`

using the
algebra homomorphism `Unitization.splitMul ๐ A`

.

## Equations

- Unitization.instNormedAlgebra = NormedAlgebra.mk โฏ

## Equations

- โฏ = โฏ