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

For possibly non-unital `RegularNormedAlgebra`

s `A`

(over `𝕜`

), we construct a `NormedAlgebra`

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 bornology on `Unitization 𝕜 A`

is inherited from `𝕜 × A`

.

## Equations

- Unitization.instBornology = Bornology.induced ⇑(Unitization.addEquiv 𝕜 A)

`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

- ⋯ = ⋯