Restricted prime-symmetry actions

All actions use the established relabelling convention v i = old (σ.symm i).

@[instance_reducible]

instance NRR.PrimeSymmetry.labelAction {p : ℕ} : MulAction (↥(PrimeSymmetry p)) (Fin p)

Equations

• NRR.PrimeSymmetry.labelAction = { smul := fun (g : ↥(NRR.PrimeSymmetry p)) (i : Fin p) => ((NRR.PrimeSymmetry.toPerm p) g) i, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem NRR.PrimeSymmetry.smul_label {p : ℕ} (g : ↥(PrimeSymmetry p)) (i : Fin p) : g • i = ((toPerm p) g) i

@[instance_reducible]

instance NRR.PrimeSymmetry.configAction {p : ℕ} : MulAction (↥(PrimeSymmetry p)) (Config p)

Equations

• NRR.PrimeSymmetry.configAction = { smul := fun (g : ↥(NRR.PrimeSymmetry p)) (s : NRR.Config p) => NRR.Config.relabel ((NRR.PrimeSymmetry.toPerm p) g) s, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem NRR.PrimeSymmetry.smul_config {p : ℕ} (g : ↥(PrimeSymmetry p)) (s : Config p) : g • s = Config.relabel ((toPerm p) g) s

@[instance_reducible]

instance NRR.PrimeSymmetry.coordinateAction {p : ℕ} : MulAction (↥(PrimeSymmetry p)) (Fin p → ℝ)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NRR.PrimeSymmetry.smul_coordinate_apply {p : ℕ} (g : ↥(PrimeSymmetry p)) (v : Fin p → ℝ) (i : Fin p) : (g • v) i = v ((Equiv.symm ((toPerm p) g)) i)

@[instance_reducible]

instance NRR.PrimeSymmetry.coordinateSMulZero {p : ℕ} : SMulZeroClass (↥(PrimeSymmetry p)) (Fin p → ℝ)

Equations

• NRR.PrimeSymmetry.coordinateSMulZero = { toSMul := NRR.PrimeSymmetry.coordinateAction.toSMul, smul_zero := ⋯ }

@[instance_reducible]

instance NRR.PrimeSymmetry.zeroSumAction {p : ℕ} : MulAction (↥(PrimeSymmetry p)) (ZeroSum p)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NRR.PrimeSymmetry.smul_zeroSum_apply {p : ℕ} (g : ↥(PrimeSymmetry p)) (v : ZeroSum p) (i : Fin p) : ↑(g • v) i = ↑v ((Equiv.symm ((toPerm p) g)) i)

@[instance_reducible]

instance NRR.PrimeSymmetry.zeroSumSMulZero {p : ℕ} : SMulZeroClass (↥(PrimeSymmetry p)) (ZeroSum p)

Equations

• NRR.PrimeSymmetry.zeroSumSMulZero = { toSMul := NRR.PrimeSymmetry.zeroSumAction.toSMul, smul_zero := ⋯ }

theorem NRR.PrimeSymmetry.continuous_smul_config {p : ℕ} (g : ↥(PrimeSymmetry p)) : Continuous fun (s : Config p) => g • s

theorem NRR.PrimeSymmetry.continuous_smul_zeroSum {p : ℕ} (g : ↥(PrimeSymmetry p)) : Continuous fun (v : ZeroSum p) => g • v

theorem NRR.PrimeSymmetry.config_smul_eq_self_imp {p : ℕ} (g : ↥(PrimeSymmetry p)) (s : Config p) (h : g • s = s) : g = 1

theorem NRR.PrimeSymmetry.config_action_free {p : ℕ} {g : ↥(PrimeSymmetry p)} {s : Config p} : g • s = s → g = 1