Approximate units

An approximate unit is a filter l such that multiplication on the left (or right) by m : α tends to 𝓝 m along the filter, and additionally l ≠ ⊥.

Examples of approximate units include:

• The trivial approximate unit pure 1 in a normed ring.
• 𝓝 1 or 𝓝[≠] 1 in a normed ring (note that the latter is disjoint from pure 1).
• In a C⋆-algebra, the filter generated by the sections fun a ↦ {x | a ≤ x} ∩ closedBall 0 1, where a ranges over the positive elements of norm strictly less than 1.

structure Filter.IsApproximateUnit {α : Type u_1} [TopologicalSpace α] [Mul α] (l : Filter α) : Prop

An approximate unit is a proper filter (i.e., ≠ ⊥) such that multiplication on the left (and separately on the right) by m : α tends to 𝓝 m along the filter.

• tendsto_mul_left (m : α) : Filter.Tendsto (fun (x : α) => m * x) l (nhds m)

  Multiplication on the left by m tends to 𝓝 m along the filter.

• tendsto_mul_right (m : α) : Filter.Tendsto (fun (x : α) => x * m) l (nhds m)

  Multiplication on the right by m tends to 𝓝 m along the filter.

• neBot : l.NeBot

  The filter is not ⊥.

theorem Filter.IsApproximateUnit.pure_one (α : Type u_1) [TopologicalSpace α] [MulOneClass α] : (pure 1).IsApproximateUnit

A unital magma with a topology and bornology has the trivial approximate unit pure 1.

theorem Filter.IsApproximateUnit.mono {α : Type u_1} [TopologicalSpace α] [MulOneClass α] {l l' : Filter α} (hl : l.IsApproximateUnit) (hle : l' ≤ l) [hl' : l'.NeBot] : l'.IsApproximateUnit

If l is an approximate unit and ⊥ < l' ≤ l, then l' is also an approximate unit.

theorem Filter.IsApproximateUnit.nhds_one (α : Type u_1) [TopologicalSpace α] [MulOneClass α] [ContinuousMul α] : (nhds 1).IsApproximateUnit

In a topological unital magma, 𝓝 1 is an approximate unit.

theorem Filter.IsApproximateUnit.iff_neBot_and_le_nhds_one {α : Type u_1} [TopologicalSpace α] [MulOneClass α] [ContinuousMul α] {l : Filter α} : l.IsApproximateUnit ↔ l.NeBot ∧ l ≤ nhds 1

In a topological unital magma, 𝓝 1 is the largest approximate unit.

theorem Filter.IsApproximateUnit.iff_le_nhds_one {α : Type u_1} [TopologicalSpace α] [MulOneClass α] [ContinuousMul α] {l : Filter α} [l.NeBot] : l.IsApproximateUnit ↔ l ≤ nhds 1

In a topological unital magma, 𝓝 1 is the largest approximate unit.