The pointwise-convergence topology on S∞ = Equiv.Perm ℕ (issue #27, commit 1)

The infinite symmetric group Equiv.Perm ℕ carries a canonical Polish topology — the topology of pointwise convergence. Mathlib puts no topology on Equiv.Perm ℕ, so we install it here via the pair embedding

embed : Equiv.Perm ℕ → (ℕ → ℕ) × (ℕ → ℕ),   embed σ = (⇑σ, ⇑σ⁻¹)

into a product of two copies of Baire space ℕ → ℕ. The image is the closed set of pairs of mutually inverse functions, so embed is a closed embedding — the route to Polishness (commit 2).

Main results

• NatPerm.embed, instTopologicalSpacePermNat: the pair embedding and the induced topology.
• NatPerm.isClosedEmbedding_embed: embed is a closed embedding, cut out by the two inverse equations (NatPerm.range_embed, NatPerm.isClosed_range_embed).
• NatPerm.continuous_apply_perm, NatPerm.continuous_inv_apply: the evaluations σ ↦ σ n and σ ↦ σ⁻¹ n are continuous.
• NatPerm.isClopen_stab and NatPerm.hasBasis_nhds: the acceptance lemma — the finite pointwise stabilizers {σ | ∀ i ∈ s, σ i = σ₀ i} are clopen and form a neighborhood basis at every σ₀. This pins the induced topology to the intended pointwise one (the pair embedding could a priori be finer).

Design

NatPerm.continuous_evalComp is the reusable primitive underlying continuity throughout this tranche: evaluating a continuous function-valued map at a continuously varying discrete index is continuous, because the index can be frozen on a clopen neighborhood. It powers the closed-range computation here and the continuity of multiplication (commit 2) and of the logic action (commit 3).

theorem NatPerm.continuous_evalComp {X : Type u_1} {I : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace Y] {f : X → I → Y} (hf : Continuous f) {e : X → I} (he : Continuous e) : Continuous fun (x : X) => f x (e x)

Localized evaluation. If f : X → I → Y is continuous and e : X → I is continuous into a discrete space I, then x ↦ f x (e x) is continuous: near any x₀ the index e x is frozen at e x₀ on the clopen set e ⁻¹' {e x₀}, where the map reduces to the continuous x ↦ f x (e x₀).

The embedding and the induced topology

def NatPerm.embed (σ : Equiv.Perm ℕ) : (ℕ → ℕ) × (ℕ → ℕ)

The pair embedding σ ↦ (σ, σ⁻¹) of Equiv.Perm ℕ into (ℕ → ℕ) × (ℕ → ℕ).

Equations

• NatPerm.embed σ = (⇑σ, ⇑σ⁻¹)

@[implicit_reducible]

instance NatPerm.instTopologicalSpacePermNat : TopologicalSpace (Equiv.Perm ℕ)

The topology of pointwise convergence on Equiv.Perm ℕ, induced by the pair embedding.

Equations

• NatPerm.instTopologicalSpacePermNat = TopologicalSpace.induced NatPerm.embed inferInstance

theorem NatPerm.isInducing_embed : Topology.IsInducing embed

theorem NatPerm.continuous_embed : Continuous embed

theorem NatPerm.embed_injective : Function.Injective embed

theorem NatPerm.continuous_coe : Continuous fun (σ : Equiv.Perm ℕ) => ⇑σ

The coercion σ ↦ ⇑σ into ℕ → ℕ is continuous.

theorem NatPerm.continuous_coe_inv : Continuous fun (σ : Equiv.Perm ℕ) => ⇑σ⁻¹

The inverse coercion σ ↦ ⇑σ⁻¹ into ℕ → ℕ is continuous.

theorem NatPerm.continuous_apply_perm (n : ℕ) : Continuous fun (σ : Equiv.Perm ℕ) => σ n

Evaluation σ ↦ σ n is continuous.

theorem NatPerm.continuous_inv_apply (n : ℕ) : Continuous fun (σ : Equiv.Perm ℕ) => σ⁻¹ n

Evaluation σ ↦ σ⁻¹ n is continuous.

The image is closed

theorem NatPerm.range_embed : Set.range embed = {p : (ℕ → ℕ) × (ℕ → ℕ) | (∀ (n : ℕ), p.1 (p.2 n) = n) ∧ ∀ (n : ℕ), p.2 (p.1 n) = n}

The image of embed is the set of pairs of mutually inverse functions.

theorem NatPerm.isClosed_range_embed : IsClosed (Set.range embed)

theorem NatPerm.isClosedEmbedding_embed : Topology.IsClosedEmbedding embed

embed is a closed embedding: pointwise-inducing, injective, with closed range.

Acceptance lemma: finite pointwise stabilizers are a clopen neighborhood basis

def NatPerm.stab (s : Finset ℕ) (σ₀ : Equiv.Perm ℕ) : Set (Equiv.Perm ℕ)

The finite pointwise stabilizer: permutations agreeing with σ₀ on the finite set s.

Equations

• NatPerm.stab s σ₀ = {σ : Equiv.Perm ℕ | ∀ i ∈ s, σ i = σ₀ i}

theorem NatPerm.isClopen_stab (s : Finset ℕ) (σ₀ : Equiv.Perm ℕ) : IsClopen (stab s σ₀)

Each finite pointwise stabilizer is clopen.

theorem NatPerm.hasBasis_nhds_fun (a : ℕ → ℕ) : (nhds a).HasBasis (fun (x : Finset ℕ) => True) fun (s : Finset ℕ) => {g : ℕ → ℕ | ∀ i ∈ s, g i = a i}

Cylinder neighborhood basis in ℕ → ℕ: sets fixing finitely many coordinates.

theorem NatPerm.hasBasis_nhds (σ₀ : Equiv.Perm ℕ) : (nhds σ₀).HasBasis (fun (x : Finset ℕ) => True) fun (s : Finset ℕ) => stab s σ₀

Acceptance lemma. The finite pointwise stabilizers form a neighborhood basis at every σ₀, so the induced topology is exactly the pointwise-convergence topology — controlling σ on a finite set already controls σ⁻¹ on the corresponding image, so the inverse coordinates in the pair embedding contribute no finer neighborhoods.