Abstract compact prime configuration model

The concrete polyhedron used in the paper will eventually instantiate this structure. The structure records only compact topological and equivariant data; it does not postulate a zero-count or separation theorem.

structure NRR.PrimeConfigurationModel {p : ℕ} (hp : Nat.Prime p) : Type 1

A compact prime configuration space with its equivariant configuration and reference maps.

• Point : Type

  The compact metric parameter space of the prime configuration model.

• metricSpace : MetricSpace self.Point
• compactSpace : CompactSpace self.Point
• nonemptyPoint : Nonempty self.Point
• pointAction : MulAction (↥(PrimeSymmetry p)) self.Point
• continuous_smul (g : ↥(PrimeSymmetry p)) : Continuous fun (x : self.Point) => g • x
• toConfig : C(self.Point, Config p)

  The continuous map from model points to labelled configurations.

• toConfig_equivariant : IsPrimeEquivariant ⇑self.toConfig
• reference : C(self.Point, ZeroSum p)

  The reference continuous map to the zero-sum representation.

• reference_equivariant : IsPrimeEquivariant ⇑self.reference

@[simp]

theorem NRR.PrimeConfigurationModel.toConfig_smul {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (g : ↥(PrimeSymmetry p)) (x : M.Point) : M.toConfig (g • x) = g • M.toConfig x

@[simp]

theorem NRR.PrimeConfigurationModel.reference_smul {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (g : ↥(PrimeSymmetry p)) (x : M.Point) : M.reference (g • x) = g • M.reference x

theorem NRR.PrimeConfigurationModel.smul_eq_self_imp {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) (g : ↥(PrimeSymmetry p)) (x : M.Point) (h : g • x = x) : g = 1

theorem NRR.PrimeConfigurationModel.action_free {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) {g : ↥(PrimeSymmetry p)} {x : M.Point} : g • x = x → g = 1

def NRR.PrimeConfigurationModel.referenceZeroSet {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) : Set M.Point

Zero set of the model's equivariant reference map.

Equations

• M.referenceZeroSet = {x : M.Point | M.reference x = 0}

theorem NRR.PrimeConfigurationModel.referenceZeroSet_invariant {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) : IsPrimeInvariant M.referenceZeroSet

theorem NRR.PrimeConfigurationModel.isClosed_referenceZeroSet {p : ℕ} {hp : Nat.Prime p} (M : PrimeConfigurationModel hp) : IsClosed M.referenceZeroSet