Irreducibility of the odd deleted modules

For odd d, the affine group Hq d has three orbitals on ordered pairs of field points. Thus every equivariant endomorphism of the full binary permutation module has a three-parameter matrix. The all-ones parameter vanishes on the deleted module, leaving a I + b A, where A is the Paley adjacency operator. A two-point vector proves that neither A nor I + A is idempotent. Maschke's theorem then proves irreducibility.

theorem SaxlCounterexamples.EveryBase.f2_eq_zero_or_one (a : F2) : a = 0 ∨ a = 1

Rank-three centralizer algebra

@[instance_reducible]

noncomputable def SaxlCounterexamples.EveryBase.finiteFintype {Ω : Type u_2} [Finite Ω] : Fintype Ω

A local enumeration supplied by finiteness.

Equations

• SaxlCounterexamples.EveryBase.finiteFintype = Fintype.ofFinite Ω

@[instance_reducible]

noncomputable def SaxlCounterexamples.EveryBase.finiteDecidableEq {Ω : Type u_2} : DecidableEq Ω

Local classical decidable equality for matrix coefficients.

Equations

• SaxlCounterexamples.EveryBase.finiteDecidableEq = Classical.decEq Ω

noncomputable def SaxlCounterexamples.EveryBase.matrixCoeff {Ω : Type u_2} [Finite Ω] (E : PermMod Ω →ₗ[F2] PermMod Ω) (x y : Ω) : F2

The (x,y) matrix coefficient, with row x and column y.

Equations

• SaxlCounterexamples.EveryBase.matrixCoeff E x y = E ((Pi.basisFun SaxlCounterexamples.EveryBase.F2 Ω) y) x

theorem SaxlCounterexamples.EveryBase.smul_basisFun {H : Type u_1} {Ω : Type u_2} [Group H] [MulAction H Ω] [Finite Ω] (g : H) (y : Ω) : g • (Pi.basisFun F2 Ω) y = (Pi.basisFun F2 Ω) (g • y)

theorem SaxlCounterexamples.EveryBase.matrixCoeff_smul {H : Type u_1} {Ω : Type u_2} [Group H] [MulAction H Ω] [Finite Ω] (E : PermMod Ω →ₗ[F2] PermMod Ω) (hE : ∀ (g : H) (f : PermMod Ω), E (g • f) = g • E f) (g : H) (x y : Ω) : matrixCoeff E (g • x) (g • y) = matrixCoeff E x y

structure SaxlCounterexamples.EveryBase.RankThreeOrbitals {H : Type u_1} {Ω : Type u_2} [Group H] [MulAction H Ω] (R : Ω → Ω → Prop) : Type u_2

Data saying that the ordered-pair orbitals are the diagonal, R, and its off-diagonal complement.

• diag : Ω

  A representative point for the diagonal orbital.

• relX : Ω

  The first point of a representative pair in R.

• relY : Ω

  The second point of a representative pair in R.

• otherX : Ω

  The first point of a representative off-diagonal pair outside R.

• otherY : Ω

  The second point of a representative off-diagonal pair outside R.

• diag_transport (x : Ω) : ∃ (g : H), g • self.diag = x
• rel_transport (x y : Ω) : x ≠ y → R x y → ∃ (g : H), g • self.relX = x ∧ g • self.relY = y
• other_transport (x y : Ω) : x ≠ y → ¬R x y → ∃ (g : H), g • self.otherX = x ∧ g • self.otherY = y

theorem SaxlCounterexamples.EveryBase.matrixCoeff_rankThree {H : Type u_1} {Ω : Type u_2} [Group H] [MulAction H Ω] [Finite Ω] (R : Ω → Ω → Prop) [DecidableRel R] (K : RankThreeOrbitals R) (E : PermMod Ω →ₗ[F2] PermMod Ω) (hE : ∀ (g : H) (f : PermMod Ω), E (g • f) = g • E f) (x y : Ω) : matrixCoeff E x y = if x = y then matrixCoeff E K.diag K.diag else if R x y then matrixCoeff E K.relX K.relY else matrixCoeff E K.otherX K.otherY

theorem SaxlCounterexamples.EveryBase.apply_eq_sum_matrixCoeff {Ω : Type u_2} [Finite Ω] (E : PermMod Ω →ₗ[F2] PermMod Ω) (f : PermMod Ω) (x : Ω) : E f x = ∑ y : Ω, f y * matrixCoeff E x y

noncomputable def SaxlCounterexamples.EveryBase.rankThreeOp {Ω : Type u_2} [Finite Ω] (R : Ω → Ω → Prop) [DecidableRel R] (α β γ : F2) : PermMod Ω →ₗ[F2] PermMod Ω

The linear operator with constant coefficients on the three orbitals.

Equations

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

theorem SaxlCounterexamples.EveryBase.eq_rankThreeOp_of_matrixCoeff {Ω : Type u_2} [Finite Ω] (E : PermMod Ω →ₗ[F2] PermMod Ω) (R : Ω → Ω → Prop) [DecidableRel R] (α β γ : F2) (hE : ∀ (x y : Ω), matrixCoeff E x y = if x = y then α else if R x y then β else γ) : E = rankThreeOp R α β γ

noncomputable def SaxlCounterexamples.EveryBase.allOnesOp {Ω : Type u_2} [Finite Ω] : PermMod Ω →ₗ[F2] PermMod Ω

The rank-one operator sending a vector to its constant coordinate sum.

Equations

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

@[simp]

theorem SaxlCounterexamples.EveryBase.allOnesOp_deleted {Ω : Type u_2} [Finite Ω] (v : ↥(DeletedModule Ω)) : allOnesOp ↑v = 0

This is the exact point at which the all-ones matrix is killed by restriction to the deleted module.

noncomputable def SaxlCounterexamples.EveryBase.relationSum {Ω : Type u_2} [Finite Ω] (R : Ω → Ω → Prop) [DecidableRel R] (v : PermMod Ω) (x : Ω) : F2

Sum a vector over the R-neighbors of a point.

Equations

• SaxlCounterexamples.EveryBase.relationSum R v x = ∑ y : Ω, if R x y then v y else 0

theorem SaxlCounterexamples.EveryBase.rankThreeOp_apply_deleted {Ω : Type u_2} [Finite Ω] (R : Ω → Ω → Prop) [DecidableRel R] (hdiag : ∀ (x : Ω), ¬R x x) (α β γ : F2) (v : ↥(DeletedModule Ω)) (x : Ω) : (rankThreeOp R α β γ) (↑v) x = (α + γ) * ↑v x + (β + γ) * relationSum R (↑v) x

theorem SaxlCounterexamples.EveryBase.double_sum_eq_diag_of_symmetric {I : Type u_3} {A : Type u_4} [AddCommMonoid A] (hchar2 : ∀ (a : A), a + a = 0) (s : Finset I) (f : I → I → A) (hsymm : ∀ (i j : I), f i j = f j i) : ∑ i ∈ s, ∑ j ∈ s, f i j = ∑ i ∈ s, f i i

Maschke projection

theorem SaxlCounterexamples.EveryBase.exists_equivariant_idempotent_projection {H : Type u_1} {Ω : Type u_2} [Group H] [MulAction H Ω] [Finite Ω] [Finite H] [NeZero ↑(Nat.card H)] (U : Subrepresentation (Representation.ofDistribMulAction F2 H ↥(DeletedModule Ω))) : ∃ (p : ↥(DeletedModule Ω) →ₗ[F2] ↥(DeletedModule Ω)), (∀ (g : H) (v : ↥(DeletedModule Ω)), p (g • v) = g • p v) ∧ p ∘ₗ p = p ∧ p.range = U.toSubmodule

The concrete Paley orbital

def SaxlCounterexamples.EveryBase.SquareDiff (d : ℕ) (x y : Fq d) : Prop

The Paley relation: x - y is a nonzero square.

Equations

• SaxlCounterexamples.EveryBase.SquareDiff d x y = (x ≠ y ∧ IsSquare (x - y))

@[instance_reducible]

noncomputable instance SaxlCounterexamples.EveryBase.squareDiffDecidable (d : ℕ) : DecidableRel (SquareDiff d)

Equations

• SaxlCounterexamples.EveryBase.squareDiffDecidable d x y = Classical.propDecidable (SaxlCounterexamples.EveryBase.SquareDiff d x y)

noncomputable def SaxlCounterexamples.EveryBase.hqRankThreeOrbitals (d : ℕ) (hd : Odd d) : RankThreeOrbitals (SquareDiff d)

Representatives and transport proofs for the three Paley orbitals.

Equations

• SaxlCounterexamples.EveryBase.hqRankThreeOrbitals d hd = { diag := 0, relX := 1, relY := 0, otherX := -1, otherY := 0, diag_transport := ⋯, rel_transport := ⋯, other_transport := ⋯ }

noncomputable def SaxlCounterexamples.EveryBase.squareFinset (d : ℕ) : Finset (Fq d)

The finite set of nonzero squares in Fq d.

Equations

• SaxlCounterexamples.EveryBase.squareFinset d = {z : SaxlCounterexamples.EveryBase.Fq d | z ≠ 0 ∧ IsSquare z}

@[simp]

theorem SaxlCounterexamples.EveryBase.mem_squareFinset (d : ℕ) (z : Fq d) : z ∈ squareFinset d ↔ z ≠ 0 ∧ IsSquare z

theorem SaxlCounterexamples.EveryBase.one_mem_squareFinset (d : ℕ) : 1 ∈ squareFinset d

noncomputable def SaxlCounterexamples.EveryBase.paleyOp (d : ℕ) : PermMod (Fq d) →ₗ[F2] PermMod (Fq d)

The Paley adjacency operator on the binary permutation module.

Equations

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

noncomputable def SaxlCounterexamples.EveryBase.squareRelFinset (d : ℕ) (x : Fq d) : Finset (Fq d)

The finite set of Paley neighbors of x.

Equations

• SaxlCounterexamples.EveryBase.squareRelFinset d x = Finset.filter (SaxlCounterexamples.EveryBase.SquareDiff d x) Finset.univ

@[simp]

theorem SaxlCounterexamples.EveryBase.mem_squareRelFinset (d : ℕ) (x y : Fq d) : y ∈ squareRelFinset d x ↔ SquareDiff d x y

theorem SaxlCounterexamples.EveryBase.relationSum_squareDiff_eq_paley (d : ℕ) (v : PermMod (Fq d)) (x : Fq d) : relationSum (SquareDiff d) v x = (paleyOp d) v x

theorem SaxlCounterexamples.EveryBase.paley_pairVector_zero (d : ℕ) (hd : Odd d) : (paleyOp d) (↑(pairVector d)) 0 = 0

theorem SaxlCounterexamples.EveryBase.char_three_neg_add_self (d : ℕ) (c : Fq d) : -c - c = c

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

The parity witness with the exact relation orientation x-y ∈ Cq: for the two-point vector v, A v (0)=0 but A² v (0)=1.

theorem SaxlCounterexamples.EveryBase.paley_map_add (d : ℕ) (f g : PermMod (Fq d)) : (paleyOp d) (f + g) = (paleyOp d) f + (paleyOp d) g

theorem SaxlCounterexamples.EveryBase.idempotent_rankThree_restriction (d : ℕ) (hd : Odd d) (p : ↥(Vq d) →ₗ[F2] ↥(Vq d)) (hp : p ∘ₗ p = p) (a b : F2) (hform : ∀ (v : ↥(Vq d)) (x : Fq d), ↑(p v) x = a * ↑v x + b * (paleyOp d) (↑v) x) : p = 0 ∨ p = LinearMap.id

theorem SaxlCounterexamples.EveryBase.hq_irreducible (d : ℕ) (hd : Odd d) : (hqRepresentation d).IsIrreducible

The deleted binary permutation module for Hq d is irreducible whenever d is odd.