Increasing approximate units: images and uniform convergence

A star-algebra homomorphism between C⋆-algebras is positive and contractive, so it maps the positive part of the closed unit ball into itself. Hence the image of an increasing approximate unit under a surjective homomorphism is an increasing approximate unit of the target, Filter.IsIncreasingApproximateUnit.map. This transfers approximate-unit limits, such as the norm of a positive functional, from a C⋆-algebra to its quotients.

Since an increasing approximate unit eventually lies in the closed unit ball, the convergence e * a → a is uniform for a in a compact set, Filter.IsIncreasingApproximateUnit.tendstoUniformlyOn_mul_right, and so is the convergence a * e → a, Filter.IsIncreasingApproximateUnit.tendstoUniformlyOn_mul_left. This controls e * α_r(b) → α_r(b) uniformly along a compact set of group elements r for a continuous action α, as needed for approximate units of twisted convolution algebras.

TauCeti.CStarAlgebra.norm_mul_star_sub_star_sq_le is the estimate for a positive contraction e that drives the approximate-unit argument showing that closed two-sided ideals are self-adjoint: ‖e * star a - star a‖ ^ 2 ≤ ‖star a * a - e * (star a * a)‖.

theorem Filter.IsIncreasingApproximateUnit.tendstoUniformlyOn_mul_right {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] {l : Filter A} (hl : l.IsIncreasingApproximateUnit) {K : Set A} (hK : IsCompact K) : TendstoUniformlyOn (fun (e a : A) => e * a) id l K

Along an increasing approximate unit, e * a → a uniformly for a in a compact set.

theorem Filter.IsIncreasingApproximateUnit.tendstoUniformlyOn_mul_left {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] {l : Filter A} (hl : l.IsIncreasingApproximateUnit) {K : Set A} (hK : IsCompact K) : TendstoUniformlyOn (fun (e a : A) => a * e) id l K

Along an increasing approximate unit, a * e → a uniformly for a in a compact set.

theorem Filter.IsIncreasingApproximateUnit.map {A : Type u_1} {B : Type u_2} {F : Type u_3} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [NonUnitalCStarAlgebra B] [PartialOrder B] [StarOrderedRing B] [FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] {l : Filter A} (hl : l.IsIncreasingApproximateUnit) (f : F) (hf : Function.Surjective ⇑f) : (Filter.map (⇑f) l).IsIncreasingApproximateUnit

The image of an increasing approximate unit under a surjective star-algebra homomorphism of C⋆-algebras is an increasing approximate unit.

theorem TauCeti.CStarAlgebra.norm_mul_star_sub_star_sq_le {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {e : A} (he₀ : 0 ≤ e) (he₁ : ‖e‖ ≤ 1) (a : A) : ‖e * star a - star a‖ ^ 2 ≤ ‖star a * a - e * (star a * a)‖

For a positive contraction e in a nonunital C⋆-algebra and any a, the C⋆-identity in the unitization gives ‖e * star a - star a‖ ^ 2 ≤ ‖star a * a - e * (star a * a)‖.