Elementary equivariant-map API

This file deliberately stays below the PL and obstruction-theory layers. It records only the pointwise equations needed by the configuration-model construction.

def NRR.IsPrimeEquivariant {p : ℕ} {X : Type u_1} {Y : Type u_2} [MulAction (↥(PrimeSymmetry p)) X] [MulAction (↥(PrimeSymmetry p)) Y] (f : X → Y) : Prop

A map commuting with the selected prime-symmetry actions.

Equations

• NRR.IsPrimeEquivariant f = ∀ (g : ↥(NRR.PrimeSymmetry p)) (x : X), f (g • x) = g • f x

theorem NRR.IsPrimeEquivariant.id {p : ℕ} {X : Type u_1} [MulAction (↥(PrimeSymmetry p)) X] : IsPrimeEquivariant fun (x : X) => x

theorem NRR.IsPrimeEquivariant.comp {p : ℕ} {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [MulAction (↥(PrimeSymmetry p)) X] [MulAction (↥(PrimeSymmetry p)) Y] [MulAction (↥(PrimeSymmetry p)) Z] {f : X → Y} {g : Y → Z} (hg : IsPrimeEquivariant g) (hf : IsPrimeEquivariant f) : IsPrimeEquivariant (g ∘ f)

theorem NRR.IsPrimeEquivariant.const_zero {p : ℕ} {X : Type u_1} {Y : Type u_2} [MulAction (↥(PrimeSymmetry p)) X] [Zero Y] [MulAction (↥(PrimeSymmetry p)) Y] (hzero : ∀ (g : ↥(PrimeSymmetry p)), g • 0 = 0) : IsPrimeEquivariant fun (x : X) => 0

def NRR.IsPrimeInvariant {p : ℕ} {X : Type u_1} [MulAction (↥(PrimeSymmetry p)) X] (S : Set X) : Prop

Invariance of a subset under the selected action.

Equations

• NRR.IsPrimeInvariant S = ∀ (g : ↥(NRR.PrimeSymmetry p)), ∀ x ∈ S, g • x ∈ S

theorem NRR.IsPrimeEquivariant.preimage_invariant {p : ℕ} {X : Type u_1} {Y : Type u_2} [MulAction (↥(PrimeSymmetry p)) X] [MulAction (↥(PrimeSymmetry p)) Y] {f : X → Y} {T : Set Y} (hf : IsPrimeEquivariant f) (hT : IsPrimeInvariant T) : IsPrimeInvariant (f ⁻¹' T)

theorem NRR.IsPrimeEquivariant.zeroSet_invariant {p : ℕ} {X : Type u_1} {Y : Type u_2} [MulAction (↥(PrimeSymmetry p)) X] [Zero Y] [MulAction (↥(PrimeSymmetry p)) Y] {f : X → Y} (hf : IsPrimeEquivariant f) (hzero : ∀ (g : ↥(PrimeSymmetry p)), g • 0 = 0) : IsPrimeInvariant {x : X | f x = 0}

def NRR.PrimeSymmetry.smulParamProd {p : ℕ} {X : Type u_1} {P : Type u_4} [MulAction (↥(PrimeSymmetry p)) X] (g : ↥(PrimeSymmetry p)) (z : P × X) : P × X

Trivial action on a parameter and the existing action on the second factor.

Equations

• NRR.PrimeSymmetry.smulParamProd g z = (z.1, g • z.2)

theorem NRR.PrimeSymmetry.smulParamProd_one {p : ℕ} {X : Type u_1} {P : Type u_4} [MulAction (↥(PrimeSymmetry p)) X] (z : P × X) : smulParamProd 1 z = z

theorem NRR.PrimeSymmetry.smulParamProd_mul {p : ℕ} {X : Type u_1} {P : Type u_4} [MulAction (↥(PrimeSymmetry p)) X] (g h : ↥(PrimeSymmetry p)) (z : P × X) : smulParamProd (g * h) z = smulParamProd g (smulParamProd h z)

@[simp]

theorem NRR.PrimeSymmetry.smulParamProd_apply {p : ℕ} {X : Type u_1} {P : Type u_4} [MulAction (↥(PrimeSymmetry p)) X] (g : ↥(PrimeSymmetry p)) (z : P × X) : smulParamProd g z = (z.1, g • z.2)

def NRR.IsPrimeEquivariantHomotopy {p : ℕ} {X : Type u_1} {Y : Type u_2} [MulAction (↥(PrimeSymmetry p)) X] [MulAction (↥(PrimeSymmetry p)) Y] (H : X × ↑(Set.Icc 0 1) → Y) : Prop

Pointwise equivariance of a homotopy with a trivially acted-on interval parameter.

Equations

• NRR.IsPrimeEquivariantHomotopy H = ∀ (g : ↥(NRR.PrimeSymmetry p)) (x : X) (t : ↑(Set.Icc 0 1)), H (g • x, t) = g • H (x, t)