Stability of involutions, fixed-point-free involutions and commuting involutions

The group-stability facts of paper I's interlude (I:2558–2649), in the form the perturbation argument (Proposition I:2267) uses them:

• invFix (Claim I:2561): a permutation ζ is within #{x | ζ² x ≠ x} points of an involution, the one that agrees with ζ where ζ² x = x and fixes the other points.
• fpfFix (Claim I:2582): an involution τ commuting with a fixed-point-free involution s is within #{x | τ x = x} points of a fixed-point-free involution: send the fixed points of τ along s. The paper instead pads an odd set by a point and matches the fixed points; here the perturbation first doubles the action, which supplies s (the swap of the two copies) and makes every set even.
• commFix (Claims I:2600 and I:2643, combined): involutions X i, i < ℓ, with a central involution J, and readable ones (i < ℓR) acting as 1 or J, all hold at every point of the set U of points p such that every ordered product X_{i₁} ⋯ X_{iᵣ} p (and the same at J p) is a point at which these relations hold. U is invariant under every X i and J, so restricting the X i to U and setting them to the identity off it gives commuting involutions, commuting with J, the readable ones aligned with J, and at most 2^{ℓ+1} times the number of bad points are changed. This replaces the paper's Glebsky–Rivera step (Claim I:2643, applied to F₂^ℓ with a 4^ℓ loss) and its separate repairs of the involution, commutation-with-J and readability conditions, with a 2^{ℓ+1} loss.

Almost involutions

def MIPRE.Tailored.Sofic.invFix {α : Type u_1} [DecidableEq α] (ζ : Equiv.Perm α) : Equiv.Perm α

The involution near a permutation ζ (Claim I:2561): ζ where ζ² x = x, the identity elsewhere.

Equations

• MIPRE.Tailored.Sofic.invFix ζ = Function.Involutive.toPerm (fun (x : α) => if ζ (ζ x) = x then ζ x else x) ⋯

theorem MIPRE.Tailored.Sofic.invFix_apply {α : Type u_1} [DecidableEq α] (ζ : Equiv.Perm α) (x : α) : (invFix ζ) x = if ζ (ζ x) = x then ζ x else x

theorem MIPRE.Tailored.Sofic.invFix_invol {α : Type u_1} [DecidableEq α] (ζ : Equiv.Perm α) (x : α) : (invFix ζ) ((invFix ζ) x) = x

theorem MIPRE.Tailored.Sofic.diffCard_invFix {α : Type u_1} [Fintype α] [DecidableEq α] (ζ : Equiv.Perm α) : diffCard (invFix ζ) ζ ≤ {x : α | ζ (ζ x) ≠ x}.card

theorem MIPRE.Tailored.Sofic.invFix_comm {α : Type u_1} [DecidableEq α] (ζ s : Equiv.Perm α) (h : ∀ (x : α), ζ (s x) = s (ζ x)) (x : α) : (invFix ζ) (s x) = s ((invFix ζ) x)

Almost fixed-point-free involutions

def MIPRE.Tailored.Sofic.fpfFix {α : Type u_1} [DecidableEq α] (τ s : Equiv.Perm α) (hτ : ∀ (x : α), τ (τ x) = x) (hs : ∀ (x : α), s (s x) = x) (hc : ∀ (x : α), τ (s x) = s (τ x)) : Equiv.Perm α

The fixed-point-free involution near an involution τ that commutes with a fixed-point-free involution s (Claim I:2582): s on the fixed points of τ, τ elsewhere.

Equations

• MIPRE.Tailored.Sofic.fpfFix τ s hτ hs hc = Function.Involutive.toPerm (fun (x : α) => if τ x = x then s x else τ x) ⋯

theorem MIPRE.Tailored.Sofic.fpfFix_apply {α : Type u_1} [DecidableEq α] {τ s : Equiv.Perm α} {hτ : ∀ (x : α), τ (τ x) = x} {hs : ∀ (x : α), s (s x) = x} {hc : ∀ (x : α), τ (s x) = s (τ x)} (x : α) : (fpfFix τ s hτ hs hc) x = if τ x = x then s x else τ x

theorem MIPRE.Tailored.Sofic.fpfFix_invol {α : Type u_1} [DecidableEq α] {τ s : Equiv.Perm α} {hτ : ∀ (x : α), τ (τ x) = x} {hs : ∀ (x : α), s (s x) = x} {hc : ∀ (x : α), τ (s x) = s (τ x)} (x : α) : (fpfFix τ s hτ hs hc) ((fpfFix τ s hτ hs hc) x) = x

theorem MIPRE.Tailored.Sofic.fpfFix_free {α : Type u_1} [DecidableEq α] {τ s : Equiv.Perm α} {hτ : ∀ (x : α), τ (τ x) = x} {hs : ∀ (x : α), s (s x) = x} {hc : ∀ (x : α), τ (s x) = s (τ x)} (hfree : ∀ (x : α), s x ≠ x) (x : α) : (fpfFix τ s hτ hs hc) x ≠ x

theorem MIPRE.Tailored.Sofic.diffCard_fpfFix {α : Type u_1} [Fintype α] [DecidableEq α] {τ s : Equiv.Perm α} {hτ : ∀ (x : α), τ (τ x) = x} {hs : ∀ (x : α), s (s x) = x} {hc : ∀ (x : α), τ (s x) = s (τ x)} : diffCard (fpfFix τ s hτ hs hc) τ ≤ {x : α | τ x = x}.card

Ordered products

def MIPRE.Tailored.Sofic.ordProd {α : Type u_1} (X : ℕ → Equiv.Perm α) (S : Finset ℕ) : ℕ → ℕ → Equiv.Perm α

The ordered product X_j^{[j ∈ S]} X_{j+1}^{[j+1 ∈ S]} ⋯ X_{j+n-1}^{[j+n-1 ∈ S]}.

Equations

• MIPRE.Tailored.Sofic.ordProd X S x✝ 0 = 1
• MIPRE.Tailored.Sofic.ordProd X S x✝ n.succ = (if x✝ ∈ S then X x✝ else 1) * MIPRE.Tailored.Sofic.ordProd X S (x✝ + 1) n

theorem MIPRE.Tailored.Sofic.ordProd_succ {α : Type u_1} (X : ℕ → Equiv.Perm α) (S : Finset ℕ) (j n : ℕ) : ordProd X S j (n + 1) = (if j ∈ S then X j else 1) * ordProd X S (j + 1) n

theorem MIPRE.Tailored.Sofic.ordProd_congr {α : Type u_1} (X : ℕ → Equiv.Perm α) (S S' : Finset ℕ) (n j : ℕ) : (∀ (m : ℕ), j ≤ m → m < j + n → (m ∈ S ↔ m ∈ S')) → ordProd X S j n = ordProd X S' j n

theorem MIPRE.Tailored.Sofic.ordProd_skip {α : Type u_1} (X : ℕ → Equiv.Perm α) (S : Finset ℕ) (n k j : ℕ) : (∀ (m : ℕ), j ≤ m → m < j + k → m ∉ S) → ordProd X S j (k + n) = ordProd X S (j + k) n

theorem MIPRE.Tailored.Sofic.ordProd_suffix {α : Type u_1} (X : ℕ → Equiv.Perm α) (S : Finset ℕ) (ℓ j : ℕ) (hj : j ≤ ℓ) : ordProd X S j (ℓ - j) = ordProd X ({x ∈ S | j ≤ x}) 0 ℓ

A suffix of an ordered product is the full product over the tail of S.

@[simp]

theorem MIPRE.Tailored.Sofic.ordProd_empty {α : Type u_1} (X : ℕ → Equiv.Perm α) (n j : ℕ) : ordProd X ∅ j n = 1

Commuting involutions

def MIPRE.Tailored.Sofic.LocGood {α : Type u_1} (X : ℕ → Equiv.Perm α) (ℓ ℓR : ℕ) (J : Equiv.Perm α) (q : α) : Prop

The relations of Checks 1–3 at a point q: the X i, i < ℓ, commute and are involutions at q, commute with J at q, and the readable ones act at q as 1 or J.

Equations

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

def MIPRE.Tailored.Sofic.InGood {α : Type u_1} (X : ℕ → Equiv.Perm α) (ℓ ℓR : ℕ) (J : Equiv.Perm α) (p : α) : Prop

The good set: every ordered product of the X i takes p, and J p, to a point at which the relations hold.

Equations

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

theorem MIPRE.Tailored.Sofic.locGood_of_inGood {α : Type u_1} {X : ℕ → Equiv.Perm α} {ℓ ℓR : ℕ} {J : Equiv.Perm α} {p : α} (h : InGood X ℓ ℓR J p) : LocGood X ℓ ℓR J p

theorem MIPRE.Tailored.Sofic.inGood_X {α : Type u_1} [DecidableEq α] {X : ℕ → Equiv.Perm α} {ℓ ℓR : ℕ} {J : Equiv.Perm α} {p : α} (h : InGood X ℓ ℓR J p) {k : ℕ} (hk : k < ℓ) : InGood X ℓ ℓR J ((X k) p)

theorem MIPRE.Tailored.Sofic.inGood_J {α : Type u_1} {X : ℕ → Equiv.Perm α} {ℓ ℓR : ℕ} {J : Equiv.Perm α} (hJ : ∀ (x : α), J (J x) = x) {p : α} (h : InGood X ℓ ℓR J p) : InGood X ℓ ℓR J (J p)

theorem MIPRE.Tailored.Sofic.inGood_of_J {α : Type u_1} {X : ℕ → Equiv.Perm α} {ℓ ℓR : ℕ} {J : Equiv.Perm α} (hJ : ∀ (x : α), J (J x) = x) {p : α} (h : InGood X ℓ ℓR J (J p)) : InGood X ℓ ℓR J p

noncomputable def MIPRE.Tailored.Sofic.commFix {α : Type u_1} [DecidableEq α] (X : ℕ → Equiv.Perm α) (ℓ ℓR : ℕ) (J : Equiv.Perm α) (i : ℕ) : Equiv.Perm α

The commuting repair of X i (Claims I:2600 and I:2643): X i on the good set, the identity off it.

Equations

• MIPRE.Tailored.Sofic.commFix X ℓ ℓR J i = Function.Involutive.toPerm (fun (q : α) => if i < ℓ ∧ MIPRE.Tailored.Sofic.InGood X ℓ ℓR J q then (X i) q else q) ⋯

theorem MIPRE.Tailored.Sofic.commFix_apply {α : Type u_1} [DecidableEq α] {X : ℕ → Equiv.Perm α} {ℓ ℓR : ℕ} {J : Equiv.Perm α} (i : ℕ) (q : α) : (commFix X ℓ ℓR J i) q = if i < ℓ ∧ InGood X ℓ ℓR J q then (X i) q else q

theorem MIPRE.Tailored.Sofic.commFix_of_good {α : Type u_1} [DecidableEq α] {X : ℕ → Equiv.Perm α} {ℓ ℓR : ℕ} {J : Equiv.Perm α} {i : ℕ} (hi : i < ℓ) {q : α} (h : InGood X ℓ ℓR J q) : (commFix X ℓ ℓR J i) q = (X i) q

theorem MIPRE.Tailored.Sofic.commFix_of_bad {α : Type u_1} [DecidableEq α] {X : ℕ → Equiv.Perm α} {ℓ ℓR : ℕ} {J : Equiv.Perm α} (i : ℕ) {q : α} (h : ¬InGood X ℓ ℓR J q) : (commFix X ℓ ℓR J i) q = q

theorem MIPRE.Tailored.Sofic.commFix_invol {α : Type u_1} [DecidableEq α] {X : ℕ → Equiv.Perm α} {ℓ ℓR : ℕ} {J : Equiv.Perm α} (i : ℕ) (q : α) : (commFix X ℓ ℓR J i) ((commFix X ℓ ℓR J i) q) = q

theorem MIPRE.Tailored.Sofic.commFix_comm {α : Type u_1} [DecidableEq α] {X : ℕ → Equiv.Perm α} {ℓ ℓR : ℕ} {J : Equiv.Perm α} {i i' : ℕ} (hi : i < ℓ) (hi' : i' < ℓ) : commFix X ℓ ℓR J i * commFix X ℓ ℓR J i' = commFix X ℓ ℓR J i' * commFix X ℓ ℓR J i

theorem MIPRE.Tailored.Sofic.commFix_J {α : Type u_1} [DecidableEq α] {X : ℕ → Equiv.Perm α} {ℓ ℓR : ℕ} {J : Equiv.Perm α} (hJ : ∀ (x : α), J (J x) = x) {i : ℕ} (hi : i < ℓ) : J * commFix X ℓ ℓR J i = commFix X ℓ ℓR J i * J

theorem MIPRE.Tailored.Sofic.commFix_readable {α : Type u_1} [DecidableEq α] {X : ℕ → Equiv.Perm α} {ℓ ℓR : ℕ} {J : Equiv.Perm α} (hR : ℓR ≤ ℓ) {i : ℕ} (hi : i < ℓR) (q : α) : (commFix X ℓ ℓR J i) q = q ∨ (commFix X ℓ ℓR J i) q = J q

theorem MIPRE.Tailored.Sofic.diffCard_commFix {α : Type u_1} [Fintype α] [DecidableEq α] {X : ℕ → Equiv.Perm α} {ℓ ℓR : ℕ} {J : Equiv.Perm α} {i : ℕ} (hi : i < ℓ) : diffCard (commFix X ℓ ℓR J i) (X i) ≤ 2 ^ (ℓ + 1) * {q : α | ¬LocGood X ℓ ℓR J q}.card

The repair changes X i at most at 2^{ℓ+1} times as many points as there are points where the relations fail.