# Unitization equipped with the $L^1$ norm #

In another file, the `Unitization ๐ A`

of a non-unital normed `๐`

-algebra `A`

is equipped with the
norm inherited as the pullback via a map (closely related to) the left-regular representation of the
algebra on itself (see `Unitization.instNormedRing`

).

However, this construction is only valid (and an isometry) when `A`

is a `RegularNormedAlgebra`

.
Sometimes it is useful to consider the unitization of a non-unital algebra with the $L^1$ norm
instead. This file provides that norm on the type synonym `WithLp 1 (Unitization ๐ A)`

, along
with the algebra isomomorphism between `Unitization ๐ A`

and `WithLp 1 (Unitization ๐ A)`

.
Note that `TrivSqZeroExt`

is also equipped with the $L^1$ norm in the analogous way, but it is
registered as an instance without the type synonym.

One application of this is a straightforward proof that the quasispectrum of an element in a non-unital Banach algebra is compact, which can be established by passing to the unitization.

The natural map between `Unitization ๐ A`

and `๐ ร A`

, transferred to their `WithLp 1`

synonyms.

## Equations

- WithLp.unitization_addEquiv_prod ๐ A = (WithLp.linearEquiv 1 ๐ (Unitization ๐ A)).toAddEquiv.trans ((Unitization.addEquiv ๐ A).trans (WithLp.linearEquiv 1 ๐ (๐ ร A)).symm.toAddEquiv)

## Instances For

## Equations

- WithLp.instUnitizationNormedAddCommGroup ๐ A = NormedAddCommGroup.induced (WithLp 1 (Unitization ๐ A)) (WithLp 1 (๐ ร A)) (WithLp.unitization_addEquiv_prod ๐ A) โฏ

Bundle `WithLp.unitization_addEquiv_prod`

as a `UniformEquiv`

.

## Equations

- WithLp.uniformEquiv_unitization_addEquiv_prod ๐ A = { toEquiv := (WithLp.unitization_addEquiv_prod ๐ A).toEquiv, uniformContinuous_toFun := โฏ, uniformContinuous_invFun := โฏ }

## Instances For

## Equations

- โฏ = โฏ

## Equations

- WithLp.instUnitizationRing = inferInstanceAs (Ring (Unitization ๐ A))

## Equations

- WithLp.instAlgebraOfNatENNRealUnitizationOfIsScalarTower = inferInstanceAs (Algebra R (Unitization ๐ A))

`WithLp.equiv`

bundled as an algebra isomorphism with `Unitization ๐ A`

.

## Equations

- WithLp.unitizationAlgEquiv R = { toEquiv := WithLp.equiv 1 (Unitization ๐ A), map_mul' := โฏ, map_add' := โฏ, commutes' := โฏ }

## Instances For

## Equations

- WithLp.instUnitizationNormedRing = NormedRing.mk โฏ โฏ

## Equations

- WithLp.instUnitizationNormedAlgebra = NormedAlgebra.mk โฏ