The binary deleted permutation module

This file constructs the deleted permutation module for an odd finite permutation set. The explicit equivariant retraction is used in the irreducibility proof: every endomorphism of the deleted module extends to the full permutation module, while the all-ones operator restricts to zero.

@[reducible, inline]

abbrev SaxlCounterexamples.EveryBase.F2 : Type

The binary field used throughout the deleted-module construction.

Equations

• SaxlCounterexamples.EveryBase.F2 = ZMod 2

@[reducible, inline]

abbrev SaxlCounterexamples.EveryBase.PermMod (Ω : Type u_1) : Type u_1

The binary permutation module on Ω.

Equations

• SaxlCounterexamples.EveryBase.PermMod Ω = (Ω → SaxlCounterexamples.EveryBase.F2)

@[instance_reducible]

instance SaxlCounterexamples.EveryBase.permModDistribMulAction {H : Type u_1} {Ω : Type u_2} [Group H] [MulAction H Ω] : DistribMulAction H (PermMod Ω)

Equations

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

instance SaxlCounterexamples.EveryBase.permModSMulCommClass {H : Type u_1} {Ω : Type u_2} [Group H] [MulAction H Ω] : SMulCommClass H F2 (PermMod Ω)

def SaxlCounterexamples.EveryBase.coordSum {Ω : Type u_2} [Fintype Ω] : PermMod Ω →ₗ[F2] F2

Sum all coordinates of a vector in the permutation module.

Equations

• SaxlCounterexamples.EveryBase.coordSum = { toFun := fun (f : SaxlCounterexamples.EveryBase.PermMod Ω) => ∑ x : Ω, f x, map_add' := ⋯, map_smul' := ⋯ }

theorem SaxlCounterexamples.EveryBase.coordSum_smul {H : Type u_1} {Ω : Type u_2} [Group H] [MulAction H Ω] [Fintype Ω] (g : H) (f : PermMod Ω) : coordSum (g • f) = coordSum f

def SaxlCounterexamples.EveryBase.DeletedModule (Ω : Type u_3) [Fintype Ω] : Submodule F2 (PermMod Ω)

The deleted binary permutation module, i.e. the coordinate-sum kernel.

Equations

• SaxlCounterexamples.EveryBase.DeletedModule Ω = SaxlCounterexamples.EveryBase.coordSum.ker

@[instance_reducible]

instance SaxlCounterexamples.EveryBase.deletedModuleDistribMulAction {H : Type u_1} {Ω : Type u_2} [Group H] [MulAction H Ω] [Fintype Ω] : DistribMulAction H ↥(DeletedModule Ω)

Equations

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

instance SaxlCounterexamples.EveryBase.deletedModuleSMulCommClass {H : Type u_1} {Ω : Type u_2} [Group H] [MulAction H Ω] [Fintype Ω] : SMulCommClass H F2 ↥(DeletedModule Ω)

def SaxlCounterexamples.EveryBase.deletedIncl {Ω : Type u_2} [Fintype Ω] : ↥(DeletedModule Ω) →ₗ[F2] PermMod Ω

The inclusion of the deleted module into the full permutation module.

Equations

• SaxlCounterexamples.EveryBase.deletedIncl = (SaxlCounterexamples.EveryBase.DeletedModule Ω).subtype

theorem SaxlCounterexamples.EveryBase.coordSum_one {Ω : Type u_2} [Fintype Ω] (hΩodd : Odd (Fintype.card Ω)) : coordSum 1 = 1

def SaxlCounterexamples.EveryBase.deletedProj {Ω : Type u_2} [Fintype Ω] (hΩodd : Odd (Fintype.card Ω)) : PermMod Ω →ₗ[F2] ↥(DeletedModule Ω)

Since |Ω| is odd, adding the coordinate sum times the all-ones vector is an equivariant retraction onto the deleted module.

Equations

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

@[simp]

theorem SaxlCounterexamples.EveryBase.deletedProj_incl {Ω : Type u_2} [Fintype Ω] (hΩodd : Odd (Fintype.card Ω)) (v : ↥(DeletedModule Ω)) : (deletedProj hΩodd) (deletedIncl v) = v

theorem SaxlCounterexamples.EveryBase.deletedProj_smul {H : Type u_1} {Ω : Type u_2} [Group H] [MulAction H Ω] [Fintype Ω] (hΩodd : Odd (Fintype.card Ω)) (g : H) (f : PermMod Ω) : (deletedProj hΩodd) (g • f) = g • (deletedProj hΩodd) f

def SaxlCounterexamples.EveryBase.extendDeletedEnd {Ω : Type u_2} [Fintype Ω] (hΩodd : Odd (Fintype.card Ω)) (T : ↥(DeletedModule Ω) →ₗ[F2] ↥(DeletedModule Ω)) : PermMod Ω →ₗ[F2] PermMod Ω

Extend a deleted-module endomorphism to the full permutation module by the canonical inclusion/retraction pair.

Equations

• SaxlCounterexamples.EveryBase.extendDeletedEnd hΩodd T = SaxlCounterexamples.EveryBase.deletedIncl ∘ₗ T ∘ₗ SaxlCounterexamples.EveryBase.deletedProj hΩodd

@[simp]

theorem SaxlCounterexamples.EveryBase.extendDeletedEnd_incl {Ω : Type u_2} [Fintype Ω] (hΩodd : Odd (Fintype.card Ω)) (T : ↥(DeletedModule Ω) →ₗ[F2] ↥(DeletedModule Ω)) (v : ↥(DeletedModule Ω)) : (extendDeletedEnd hΩodd T) (deletedIncl v) = deletedIncl (T v)

theorem SaxlCounterexamples.EveryBase.extendDeletedEnd_smul {H : Type u_1} {Ω : Type u_2} [Group H] [MulAction H Ω] [Fintype Ω] (hΩodd : Odd (Fintype.card Ω)) (T : ↥(DeletedModule Ω) →ₗ[F2] ↥(DeletedModule Ω)) (hT : ∀ (g : H) (v : ↥(DeletedModule Ω)), T (g • v) = g • T v) (g : H) (f : PermMod Ω) : (extendDeletedEnd hΩodd T) (g • f) = g • (extendDeletedEnd hΩodd T) f

@[reducible, inline]

noncomputable abbrev SaxlCounterexamples.EveryBase.Vq (d : ℕ) : Submodule F2 (PermMod (Fq d))

The deleted permutation module for the affine group over Fq d.

Equations

• SaxlCounterexamples.EveryBase.Vq d = SaxlCounterexamples.EveryBase.DeletedModule (SaxlCounterexamples.EveryBase.Fq d)

@[instance_reducible]

noncomputable instance SaxlCounterexamples.EveryBase.fqDecidableEq (d : ℕ) : DecidableEq (Fq d)

Equations

• SaxlCounterexamples.EveryBase.fqDecidableEq d = Classical.typeDecidableEq (SaxlCounterexamples.EveryBase.Fq d)

@[instance_reducible]

noncomputable instance SaxlCounterexamples.EveryBase.hqFintype (d : ℕ) : Fintype (Hq d)

Equations

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

instance SaxlCounterexamples.EveryBase.hqNontrivial (d : ℕ) : Nontrivial (Hq d)

@[instance_reducible]

noncomputable instance SaxlCounterexamples.EveryBase.vqFintype (d : ℕ) : Fintype ↥(Vq d)

Equations

• SaxlCounterexamples.EveryBase.vqFintype d = Fintype.ofFinite ↥(SaxlCounterexamples.EveryBase.Vq d)

theorem SaxlCounterexamples.EveryBase.coordSum_ne_zero_q (d : ℕ) (hd : Odd d) : coordSum ≠ 0

theorem SaxlCounterexamples.EveryBase.vq_finrank (d : ℕ) (hd : Odd d) : Module.finrank F2 ↥(Vq d) = 3 ^ d - 1

The deleted module has the paper's dimension 3^d - 1.

theorem SaxlCounterexamples.EveryBase.vq_card (d : ℕ) (hd : Odd d) : Nat.card ↥(Vq d) = 2 ^ (3 ^ d - 1)

Consequently Vq d has exactly 2^(3^d-1) elements.

noncomputable def SaxlCounterexamples.EveryBase.hqRepresentation (d : ℕ) : Representation F2 (Hq d) ↥(Vq d)

The natural representation of Hq d on its deleted module.

Equations

• SaxlCounterexamples.EveryBase.hqRepresentation d = Representation.ofDistribMulAction SaxlCounterexamples.EveryBase.F2 (SaxlCounterexamples.EveryBase.Hq d) ↥(SaxlCounterexamples.EveryBase.Vq d)

noncomputable def SaxlCounterexamples.EveryBase.pairVector (d : ℕ) : ↥(Vq d)

The characteristic vector of {0,1}, written as a deleted vector.

Equations

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

@[simp]

theorem SaxlCounterexamples.EveryBase.pairVector_apply (d : ℕ) (x : Fq d) : ↑(pairVector d) x = (Pi.basisFun F2 (Fq d)) 0 x + (Pi.basisFun F2 (Fq d)) 1 x

theorem SaxlCounterexamples.EveryBase.pairVector_coe_eq_twoPointVector (d : ℕ) : ↑(pairVector d) = twoPointVector d

theorem SaxlCounterexamples.EveryBase.pairVector_zero (d : ℕ) : ↑(pairVector d) 0 = 1

theorem SaxlCounterexamples.EveryBase.pairVector_ne_zero (d : ℕ) : pairVector d ≠ 0

instance SaxlCounterexamples.EveryBase.vqNontrivial (d : ℕ) : Nontrivial ↥(Vq d)

theorem SaxlCounterexamples.EveryBase.pairVector_isRegular (d : ℕ) (hd : Odd d) : Saxl.IsRegularVector (Hq d) (↥(Vq d)) (pairVector d)

theorem SaxlCounterexamples.EveryBase.hq_regularOrbit_exists (d : ℕ) (hd : Odd d) : ∃ (v : ↥(Vq d)), Saxl.IsRegularVector (Hq d) (↥(Vq d)) v

Paper Lemma 6.1: the two-point vector gives a regular Hq d-orbit.

theorem SaxlCounterexamples.EveryBase.hq_faithful (d : ℕ) (hd : Odd d) : FaithfulSMul (Hq d) ↥(Vq d)

Paper Lemma 6.1: the deleted-module action is faithful.

noncomputable def SaxlCounterexamples.EveryBase.hqBadSeedVector (d : ℕ) (hd : Odd d) : ↥(Vq d)

The complement-of-zero vector used in the displayed obstruction.

Equations

• SaxlCounterexamples.EveryBase.hqBadSeedVector d hd = ⟨1 + (Pi.basisFun SaxlCounterexamples.EveryBase.F2 (SaxlCounterexamples.EveryBase.Fq d)) 0, ⋯⟩

@[simp]

theorem SaxlCounterexamples.EveryBase.hqBadSeedVector_apply (d : ℕ) (hd : Odd d) (x : Fq d) : ↑(hqBadSeedVector d hd) x = if x = 0 then 0 else 1

theorem SaxlCounterexamples.EveryBase.hqBadSeedVector_not_regular (d : ℕ) (hd : Odd d) (hd3 : 3 ≤ d) : ¬Saxl.IsRegularVector (Hq d) (↥(Vq d)) (hqBadSeedVector d hd)

The displayed bad seed vector is not regular: every nonidentity square multiplier fixes both 0 and its complement.

noncomputable def SaxlCounterexamples.EveryBase.deletedCoord (d : ℕ) : ↥(Vq d) →+ Fq d → F2

The coordinate map from the deleted module to binary-valued functions.

Equations

• SaxlCounterexamples.EveryBase.deletedCoord d = ↑(SaxlCounterexamples.EveryBase.Vq d).subtype.toAddHom