Pointwise limits of character fusions

The fusion construction produces a sequence of circle-valued homomorphisms. Every group element is eventually protected, so its values form a Cauchy sequence. This file isolates the complete metric argument: the pointwise limit is again a homomorphism, and a geometric bound on a tail gives an explicit bound from the first point of that tail to the limit.

noncomputable def Wallace.pointwiseLimitCharacter {G : Type u} [AddGroup G] (f : ℕ → G →+ UnitAddCircle) (hf : ∀ (x : G), CauchySeq fun (n : ℕ) => (f n) x) : G →+ UnitAddCircle

The pointwise limit of a pointwise-Cauchy sequence of additive characters.

Equations

• Wallace.pointwiseLimitCharacter f hf = { toFun := fun (x : G) => Filter.atTop.limUnder fun (n : ℕ) => (f n) x, map_zero' := ⋯, map_add' := ⋯ }

theorem Wallace.tendsto_pointwiseLimitCharacter {G : Type u} [AddGroup G] (f : ℕ → G →+ UnitAddCircle) (hf : ∀ (x : G), CauchySeq fun (n : ℕ) => (f n) x) (x : G) : Filter.Tendsto (fun (n : ℕ) => (f n) x) Filter.atTop (nhds ((pointwiseLimitCharacter f hf) x))

The defining sequence converges pointwise to pointwiseLimitCharacter.