NRR.ConfigurationSpace — configurations of distinct labelled sites

Config n is the subtype of injective maps Fin n → Plane. Its topology is induced by the point map, and permutations act by precomposition with σ.symm. The action is continuous and free.

def NRR.Config (n : ℕ) : Type

Configuration space of n distinct labelled points in the plane.

Equations

• NRR.Config n = { p : Fin n → NRR.E2 // Function.Injective p }

def NRR.Config.pts {n : ℕ} (p : Config n) : Fin n → E2

The underlying point map of a configuration.

Equations

• p.pts = ↑p

@[instance_reducible]

noncomputable instance NRR.instMetricSpaceConfig (n : ℕ) : MetricSpace (Config n)

Metric on configuration space: the metric induced by the point map Config.pts from the finite product Fin n → E2. Its associated topology is definitionally the same as the subspace topology, since Config.pts = Subtype.val.

Equations

• NRR.instMetricSpaceConfig n = MetricSpace.induced NRR.Config.pts ⋯ inferInstance

theorem NRR.Config.topology_eq_induced (n : ℕ) : inferInstance = TopologicalSpace.induced pts inferInstance

The metric topology on Config n is definitionally the topology induced by the point map Config.pts; equivalently, the subspace topology from Fin n → E2.

def NRR.Config.toFun {n : ℕ} (s : Config n) : Fin n → E2

The underlying point map of a configuration, as a bundled function. Compatibility alias of Config.pts.

Equations

• s.toFun = s.pts

@[simp]

theorem NRR.Config.toFun_apply {n : ℕ} (s : Config n) (i : Fin n) : s.toFun i = s.pts i

theorem NRR.Config.injective {n : ℕ} (s : Config n) : Function.Injective s.pts

The point map of a configuration is injective.

theorem NRR.Config.injective_pts {n : ℕ} (s : Config n) : Function.Injective s.pts

Injectivity accessor for a configuration. A configuration s : Config n bundles a site map s.pts together with a proof that it is injective; this exposes that proof under the name injective_pts, matching the requested configuration API.

theorem NRR.Config.continuous_pts {n : ℕ} : Continuous fun (s : Config n) => s.pts

The projection Config.pts is continuous for the induced topology (the induced-topology domain theorem).

def NRR.Config.relabel {n : ℕ} (σ : Equiv.Perm (Fin n)) (s : Config n) : Config n

Relabelling of a configuration. For a permutation σ : Equiv.Perm (Fin n) and a configuration s : Config n, the relabelled configuration Config.relabel σ s is obtained by precomposing the point map with σ.symm, i.e. (Config.relabel σ s).pts i = s.pts (σ.symm i). This σ.symm convention is fixed for the remainder of the current development.

Equations

• NRR.Config.relabel σ s = ⟨fun (i : Fin n) => s.pts ((Equiv.symm σ) i), ⋯⟩

@[simp]

theorem NRR.Config.relabel_pts {n : ℕ} (σ : Equiv.Perm (Fin n)) (s : Config n) (i : Fin n) : (relabel σ s).pts i = s.pts ((Equiv.symm σ) i)

@[simp]

theorem NRR.Config.relabel_one {n : ℕ} (s : Config n) : relabel 1 s = s

theorem NRR.Config.relabel_mul {n : ℕ} (σ τ : Equiv.Perm (Fin n)) (s : Config n) : relabel (σ * τ) s = relabel σ (relabel τ s)

@[instance_reducible]

instance NRR.Config.permAction (n : ℕ) : MulAction (Equiv.Perm (Fin n)) (Config n)

The Sₙ‑action σ • s := Config.relabel σ s on the configuration space, by relabelling via precomposition with σ.symm.

Equations

• NRR.Config.permAction n = { smul := fun (σ : Equiv.Perm (Fin n)) (s : NRR.Config n) => NRR.Config.relabel σ s, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem NRR.Config.smul_def {n : ℕ} (σ : Equiv.Perm (Fin n)) (s : Config n) : σ • s = relabel σ s

theorem NRR.Config.continuous_relabel {n : ℕ} (σ : Equiv.Perm (Fin n)) : Continuous fun (s : Config n) => relabel σ s

Relabelling is continuous for the topology induced by the point map.

theorem NRR.Config.relabel_eq_self_imp {n : ℕ} (σ : Equiv.Perm (Fin n)) (s : Config n) (h : relabel σ s = s) : σ = 1

Freeness of relabelling. If relabelling a configuration by σ leaves it unchanged, then σ is the identity permutation.

theorem NRR.Config.relabel_eq_self_iff {n : ℕ} (σ : Equiv.Perm (Fin n)) (s : Config n) : relabel σ s = s ↔ σ = 1

Freeness of relabelling, biconditional form. Relabelling a configuration by σ leaves it unchanged iff σ is the identity permutation.

theorem NRR.Config.smul_eq_self_imp {n : ℕ} (σ : Equiv.Perm (Fin n)) (s : Config n) (h : σ • s = s) : σ = 1

Freeness for the MulAction. Wrapper over Config.relabel_eq_self_imp: if the Sₙ‑action fixes a configuration then the permutation is the identity.

theorem NRR.Config.action_free (n : ℕ) {σ : Equiv.Perm (Fin n)} {p : Config n} (h : σ • p = p) : σ = 1

The Sₙ‑action on the configuration space is free.

theorem NRR.Config.continuous_smul (n : ℕ) (σ : Equiv.Perm (Fin n)) : Continuous fun (p : Config n) => σ • p

The Sₙ‑action is continuous (by homeomorphisms).