The quotient of an action by a fixed-point-free involution

Paper I, Proposition I:2279, first half: an action passing Checks 1–3 of the associated test is a Z-aligned permutation strategy. Let J be a fixed-point-free involution of Fin N. Its orbits are the pairs {p, J p}, with representatives Reps J, the points p < J p. A permutation τ commuting with J (CommJ J τ) permutes the orbits, and the choice of representatives makes this a signed permutation ind J τ of Reps J: the representative r goes to the representative of τ r, with sign - when τ r is not itself a representative. This is the action of τ on the (-1)-eigenspace of J, in the basis e_r - e_{J r}.

• ind_mul, ind_one, ind_J: ind J is multiplicative on the centralizer of J, and sends J to -1.
• ind_fix_iff: ind J τ fixes r with sign + exactly when τ fixes r.
• quotStrat σ hσ: for an action σ passing Checks 1–3, the Z-aligned permutation strategy of the signed permutations ind J X(x, i), transported to Fin m, m = |Reps J| = N / 2.

def MIPRE.Tailored.Sofic.CommJ {N : ℕ} (J τ : Equiv.Perm (Fin N)) : Prop

τ commutes with J.

Equations

• MIPRE.Tailored.Sofic.CommJ J τ = ∀ (p : Fin N), τ (J p) = J (τ p)

def MIPRE.Tailored.Sofic.FFInvol {N : ℕ} (J : Equiv.Perm (Fin N)) : Prop

J is a fixed-point-free involution.

Equations

• MIPRE.Tailored.Sofic.FFInvol J = ((∀ (p : Fin N), J (J p) = p) ∧ ∀ (p : Fin N), J p ≠ p)

@[reducible, inline]

abbrev MIPRE.Tailored.Sofic.Reps {N : ℕ} (J : Equiv.Perm (Fin N)) : Type

The representatives of the J-orbits: the points p < J p.

Equations

• MIPRE.Tailored.Sofic.Reps J = { p : Fin N // p < J p }

def MIPRE.Tailored.Sofic.rep {N : ℕ} (J : Equiv.Perm (Fin N)) (p : Fin N) : Fin N

The representative of the orbit of p.

Equations

• MIPRE.Tailored.Sofic.rep J p = if p < J p then p else J p

theorem MIPRE.Tailored.Sofic.CommJ.one {N : ℕ} {J : Equiv.Perm (Fin N)} : CommJ J 1

theorem MIPRE.Tailored.Sofic.CommJ.mul {N : ℕ} {J τ₁ τ₂ : Equiv.Perm (Fin N)} (h₁ : CommJ J τ₁) (h₂ : CommJ J τ₂) : CommJ J (τ₁ * τ₂)

theorem MIPRE.Tailored.Sofic.CommJ.inv {N : ℕ} {J τ : Equiv.Perm (Fin N)} (h : CommJ J τ) : CommJ J τ⁻¹

theorem MIPRE.Tailored.Sofic.CommJ.self {N : ℕ} {J : Equiv.Perm (Fin N)} : CommJ J J

theorem MIPRE.Tailored.Sofic.FFInvol.lt_J_J_iff {N : ℕ} {J : Equiv.Perm (Fin N)} (hJ : FFInvol J) (p : Fin N) : J p < J (J p) ↔ ¬p < J p

theorem MIPRE.Tailored.Sofic.FFInvol.decide_lt_J_J {N : ℕ} {J : Equiv.Perm (Fin N)} (hJ : FFInvol J) (p : Fin N) : decide (J p < J (J p)) = !decide (p < J p)

theorem MIPRE.Tailored.Sofic.FFInvol.rep_lt {N : ℕ} {J : Equiv.Perm (Fin N)} (hJ : FFInvol J) (p : Fin N) : rep J p < J (rep J p)

theorem MIPRE.Tailored.Sofic.FFInvol.rep_of_lt {N : ℕ} {J : Equiv.Perm (Fin N)} {p : Fin N} (h : p < J p) : rep J p = p

theorem MIPRE.Tailored.Sofic.FFInvol.rep_J {N : ℕ} {J : Equiv.Perm (Fin N)} (hJ : FFInvol J) (p : Fin N) : rep J (J p) = rep J p

theorem MIPRE.Tailored.Sofic.FFInvol.rep_eq {N : ℕ} {J : Equiv.Perm (Fin N)} (p : Fin N) : rep J p = p ∨ rep J p = J p

theorem MIPRE.Tailored.Sofic.FFInvol.rep_rep_comm {N : ℕ} {J : Equiv.Perm (Fin N)} (hJ : FFInvol J) {τ : Equiv.Perm (Fin N)} (hτ : CommJ J τ) (p : Fin N) : rep J (τ (rep J p)) = rep J (τ p)

The induced signed permutation

def MIPRE.Tailored.Sofic.indPerm {N : ℕ} {J : Equiv.Perm (Fin N)} (hJ : FFInvol J) (τ : Equiv.Perm (Fin N)) (hτ : CommJ J τ) : Equiv.Perm (Reps J)

The permutation of the representatives induced by τ.

Equations

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

noncomputable def MIPRE.Tailored.Sofic.ind {N : ℕ} (J τ : Equiv.Perm (Fin N)) : SignedPerm (Reps J)

The signed permutation of the representatives induced by τ: r ↦ ± rep(τ r), with sign - when τ r is not a representative (the identity when J is not a fixed-point-free involution or τ does not commute with it).

Equations

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

theorem MIPRE.Tailored.Sofic.ind_perm_apply {N : ℕ} {J : Equiv.Perm (Fin N)} (hJ : FFInvol J) {τ : Equiv.Perm (Fin N)} (hτ : CommJ J τ) (r : Reps J) : ↑((ind J τ).perm r) = rep J (τ ↑r)

theorem MIPRE.Tailored.Sofic.ind_sign {N : ℕ} {J : Equiv.Perm (Fin N)} (hJ : FFInvol J) {τ : Equiv.Perm (Fin N)} (hτ : CommJ J τ) (r : Reps J) : (ind J τ).sign r = decide ¬τ ↑r < J (τ ↑r)

theorem MIPRE.Tailored.Sofic.ind_mul {N : ℕ} {J : Equiv.Perm (Fin N)} (hJ : FFInvol J) {τ₁ τ₂ : Equiv.Perm (Fin N)} (h₁ : CommJ J τ₁) (h₂ : CommJ J τ₂) : ind J (τ₁ * τ₂) = ind J τ₁ * ind J τ₂

theorem MIPRE.Tailored.Sofic.ind_one {N : ℕ} {J : Equiv.Perm (Fin N)} (hJ : FFInvol J) : ind J 1 = 1

theorem MIPRE.Tailored.Sofic.ind_J {N : ℕ} {J : Equiv.Perm (Fin N)} (hJ : FFInvol J) : ind J J = SignedPerm.negOne

theorem MIPRE.Tailored.Sofic.ind_fix_iff {N : ℕ} {J : Equiv.Perm (Fin N)} (hJ : FFInvol J) {τ : Equiv.Perm (Fin N)} (hτ : CommJ J τ) (r : Reps J) : (ind J τ).perm r = r ∧ (ind J τ).sign r = false ↔ τ ↑r = ↑r

ind J τ fixes r with sign + exactly when τ fixes r.

theorem MIPRE.Tailored.Sofic.ind_perm_eq_one {N : ℕ} {J : Equiv.Perm (Fin N)} (hJ : FFInvol J) {τ : Equiv.Perm (Fin N)} (hτ : CommJ J τ) (hr : ∀ (p : Fin N), τ p = p ∨ τ p = J p) : (ind J τ).perm = 1

A readable variable induces a diagonal signed permutation.

theorem MIPRE.Tailored.Sofic.ind_sign_eq {N : ℕ} {J : Equiv.Perm (Fin N)} (hJ : FFInvol J) {τ : Equiv.Perm (Fin N)} (hτ : CommJ J τ) (hr : ∀ (p : Fin N), τ p = p ∨ τ p = J p) (r : Reps J) : (ind J τ).sign r = decide (τ ↑r ≠ ↑r)

theorem MIPRE.Tailored.Sofic.card_le_two_mul_card_reps {N : ℕ} {J : Equiv.Perm (Fin N)} (hJ : FFInvol J) : N ≤ 2 * Fintype.card (Reps J)

There are N / 2 orbits: N ≤ 2 |Reps J|.

theorem MIPRE.Tailored.Sofic.reps_nonempty {N : ℕ} {J : Equiv.Perm (Fin N)} (hJ : FFInvol J) (hN : 0 < N) : Nonempty (Reps J)

The quotient strategy

theorem MIPRE.Tailored.Sofic.Checks.ffInvol {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (hσ : Checks g σ) : FFInvol (genPerm σ genJ)

theorem MIPRE.Tailored.Sofic.Checks.commJ_X {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (hσ : Checks g σ) {x i : ℕ} (hx : x < g.nV + 1) (hi : i < g.lenAt x) : CommJ (genPerm σ genJ) (genPerm σ (genX g x i))

theorem MIPRE.Tailored.Sofic.Checks.readable' {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (hσ : Checks g σ) {x i : ℕ} (hx : x < g.nV + 1) (hi : i < g.lenRAt x) (p : Fin σ.N) : (genPerm σ (genX g x i)) p = p ∨ (genPerm σ (genX g x i)) p = (genPerm σ genJ) p

noncomputable def MIPRE.Tailored.Sofic.repEquiv {g : TailoredGameValue.TailoredGameData} (σ : SubgroupTestValue.FiniteAction (nGen g)) : Reps (genPerm σ genJ) ≃ Fin (Fintype.card (Reps (genPerm σ genJ)))

The enumeration of the representatives.

Equations

• MIPRE.Tailored.Sofic.repEquiv σ = Fintype.equivFin (MIPRE.Tailored.Sofic.Reps (MIPRE.Tailored.Sofic.genPerm σ MIPRE.Tailored.Sofic.genJ))

noncomputable def MIPRE.Tailored.Sofic.indF {g : TailoredGameValue.TailoredGameData} (σ : SubgroupTestValue.FiniteAction (nGen g)) (τ : Equiv.Perm (Fin σ.N)) : SignedPerm (Fin (Fintype.card (Reps (genPerm σ genJ))))

The induced signed permutation, on Fin m.

Equations

• MIPRE.Tailored.Sofic.indF σ τ = MIPRE.Tailored.SignedPerm.map (MIPRE.Tailored.Sofic.repEquiv σ) (MIPRE.Tailored.Sofic.ind (MIPRE.Tailored.Sofic.genPerm σ MIPRE.Tailored.Sofic.genJ) τ)

theorem MIPRE.Tailored.Sofic.SignedPerm.map_mul' {Ω : Type u_1} {Ω' : Type u_2} (e : Ω ≃ Ω') (s t : SignedPerm Ω) : SignedPerm.map e (s * t) = SignedPerm.map e s * SignedPerm.map e t

theorem MIPRE.Tailored.Sofic.SignedPerm.map_one' {Ω : Type u_1} {Ω' : Type u_2} (e : Ω ≃ Ω') : SignedPerm.map e 1 = 1

theorem MIPRE.Tailored.Sofic.indF_mul {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (hσ : Checks g σ) {τ₁ τ₂ : Equiv.Perm (Fin σ.N)} (h₁ : CommJ (genPerm σ genJ) τ₁) (h₂ : CommJ (genPerm σ genJ) τ₂) : indF σ (τ₁ * τ₂) = indF σ τ₁ * indF σ τ₂

theorem MIPRE.Tailored.Sofic.indF_one {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (hσ : Checks g σ) : indF σ 1 = 1

theorem MIPRE.Tailored.Sofic.toMatrix_indF_J {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (hσ : Checks g σ) : (indF σ (genPerm σ genJ)).toMatrix = -1

noncomputable def MIPRE.Tailored.Sofic.repPt {g : TailoredGameValue.TailoredGameData} (σ : SubgroupTestValue.FiniteAction (nGen g)) (j : Fin (Fintype.card (Reps (genPerm σ genJ)))) : Fin σ.N

The point of Fin N representing the basis point j.

Equations

• MIPRE.Tailored.Sofic.repPt σ j = ↑((MIPRE.Tailored.Sofic.repEquiv σ).symm j)

theorem MIPRE.Tailored.Sofic.indF_fix_iff {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (hσ : Checks g σ) {τ : Equiv.Perm (Fin σ.N)} (hτ : CommJ (genPerm σ genJ) τ) (j : Fin (Fintype.card (Reps (genPerm σ genJ)))) : (indF σ τ).perm j = j ∧ (indF σ τ).sign j = false ↔ τ (repPt σ j) = repPt σ j

theorem MIPRE.Tailored.Sofic.indF_perm_eq_one {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (hσ : Checks g σ) {τ : Equiv.Perm (Fin σ.N)} (hτ : CommJ (genPerm σ genJ) τ) (hr : ∀ (p : Fin σ.N), τ p = p ∨ τ p = (genPerm σ genJ) p) : (indF σ τ).perm = 1

theorem MIPRE.Tailored.Sofic.indF_sign_eq {g : TailoredGameValue.TailoredGameData} {σ : SubgroupTestValue.FiniteAction (nGen g)} (hσ : Checks g σ) {τ : Equiv.Perm (Fin σ.N)} (hτ : CommJ (genPerm σ genJ) τ) (hr : ∀ (p : Fin σ.N), τ p = p ∨ τ p = (genPerm σ genJ) p) (j : Fin (Fintype.card (Reps (genPerm σ genJ)))) : (indF σ τ).sign j = decide (τ (repPt σ j) ≠ repPt σ j)

noncomputable def MIPRE.Tailored.Sofic.quotU {g : TailoredGameValue.TailoredGameData} (σ : SubgroupTestValue.FiniteAction (nGen g)) (x : Fin (g.nV + 1)) (i : Fin g.ansLen) : Matrix (Fin (Fintype.card (Reps (genPerm σ genJ)))) (Fin (Fintype.card (Reps (genPerm σ genJ)))) ℂ

The observable of the quotient strategy, before packaging.

Equations

• MIPRE.Tailored.Sofic.quotU σ x i = if ↑i < g.lenAt ↑x then (MIPRE.Tailored.Sofic.indF σ (MIPRE.Tailored.Sofic.genPerm σ (MIPRE.Tailored.Sofic.genX g ↑x ↑i))).toMatrix else 1

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.Sofic.quotStrat {g : TailoredGameValue.TailoredGameData} (σ : SubgroupTestValue.FiniteAction (nGen g)) (hσ : Checks g σ) : ZStrat g

The quotient strategy (Proposition I:2279): an action passing Checks 1–3 gives a Z-aligned permutation strategy on the J-orbits.

Equations

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