Approximate units: images and products

An approximate unit is a proper filter along which the left and the right multiplications by each element converge to it; Filter.IsApproximateUnit.iff_neBot_and_tendsto_prod packages the two convergences as a single one in the product α × α.

The image of an approximate unit under a continuous surjective multiplicative map is again an approximate unit, Filter.IsApproximateUnit.map. Surjectivity is what lets every element of the target be written as an image, so that its products with the image filter converge. This is the input for transferring approximate units, and quantities computed as their limits, from a C⋆-algebra to its quotients.

theorem Filter.IsApproximateUnit.iff_neBot_and_tendsto_prod {α : Type u_1} [TopologicalSpace α] [Mul α] {l : Filter α} : l.IsApproximateUnit ↔ l.NeBot ∧ ∀ (a : α), Tendsto (fun (e : α) => (e * a, a * e)) l (nhds (a, a))

A filter is an approximate unit iff it is proper and, for every a, the pair of products (e * a, a * e) tends to (a, a) along it.

theorem Filter.IsApproximateUnit.map {α : Type u_1} {β : Type u_2} {F : Type u_3} [TopologicalSpace α] [Mul α] [TopologicalSpace β] [Mul β] [FunLike F α β] [MulHomClass F α β] {l : Filter α} (hl : l.IsApproximateUnit) (f : F) (hf : Continuous ⇑f) (hf' : Function.Surjective ⇑f) : (Filter.map (⇑f) l).IsApproximateUnit

The image of an approximate unit under a continuous surjective multiplicative map is an approximate unit.