The odd affine Frobenius groups used by the every-base-size construction

For odd d, this file defines

• Fq d = GF(3^d);
• the subgroup Cq d of nonzero squares; and
• Hq d = Fq d ⋊ Cq d, acting affinely on Fq d.

The deleted permutation module and its irreducibility are deliberately kept in the later files of the construction. Here we prove the elementary finite-field facts and the two-point support calculation needed there.

@[reducible, inline]

abbrev SaxlCounterexamples.EveryBase.Fq (d : ℕ) : Type

The finite field of order 3 ^ d.

Equations

• SaxlCounterexamples.EveryBase.Fq d = GaloisField 3 d

@[instance_reducible]

noncomputable instance SaxlCounterexamples.EveryBase.fqFintype (d : ℕ) : Fintype (Fq d)

Equations

• SaxlCounterexamples.EveryBase.fqFintype d = Fintype.ofFinite (SaxlCounterexamples.EveryBase.Fq d)

@[reducible, inline]

noncomputable abbrev SaxlCounterexamples.EveryBase.Cq (d : ℕ) : Subgroup (Fq d)ˣ

The subgroup of nonzero squares in GF(3^d).

Equations

• SaxlCounterexamples.EveryBase.Cq d = Subgroup.square (SaxlCounterexamples.EveryBase.Fq d)ˣ

@[instance_reducible]

noncomputable instance SaxlCounterexamples.EveryBase.cqFintype (d : ℕ) : Fintype ↥(Cq d)

Equations

• SaxlCounterexamples.EveryBase.cqFintype d = Fintype.ofFinite ↥(SaxlCounterexamples.EveryBase.Cq d)

@[reducible, inline]

abbrev SaxlCounterexamples.EveryBase.Hq (d : ℕ) : Type

The affine Frobenius group GF(3^d) ⋊ Cq.

Equations

• SaxlCounterexamples.EveryBase.Hq d = Saxl.AffineGroup (↥(SaxlCounterexamples.EveryBase.Cq d)) (SaxlCounterexamples.EveryBase.Fq d)

theorem SaxlCounterexamples.EveryBase.three_pow_mod_four_of_odd (d : ℕ) (hd : Odd d) : 3 ^ d % 4 = 3

theorem SaxlCounterexamples.EveryBase.fq_card (d : ℕ) (hd : Odd d) : Nat.card (Fq d) = 3 ^ d

theorem SaxlCounterexamples.EveryBase.fq_card_mod_four (d : ℕ) (hd : Odd d) : Nat.card (Fq d) % 4 = 3

theorem SaxlCounterexamples.EveryBase.fq_odd_card (d : ℕ) (hd : Odd d) : Odd (Nat.card (Fq d))

theorem SaxlCounterexamples.EveryBase.square_subgroup_eq_powRange (G : Type u_1) [CommGroup G] : Subgroup.square G = (powMonoidHom 2).range

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

theorem SaxlCounterexamples.EveryBase.cq_odd_card (d : ℕ) (hd : Odd d) : Odd (Nat.card ↥(Cq d))

theorem SaxlCounterexamples.EveryBase.hq_odd_card (d : ℕ) (hd : Odd d) : Odd (Nat.card (Hq d))

theorem SaxlCounterexamples.EveryBase.neg_one_not_square (d : ℕ) (hd : Odd d) : ¬IsSquare (-1)

theorem SaxlCounterexamples.EveryBase.neg_isSquare_of_not_isSquare (d : ℕ) (hd : Odd d) {z : Fq d} (hz0 : z ≠ 0) (hz : ¬IsSquare z) : IsSquare (-z)

noncomputable def SaxlCounterexamples.EveryBase.squareUnit (d : ℕ) {z : Fq d} (hz0 : z ≠ 0) (hz : IsSquare z) : ↥(Cq d)

Package a nonzero square as an element of Cq.

Equations

• SaxlCounterexamples.EveryBase.squareUnit d hz0 hz = ⟨Units.mk0 z hz0, ⋯⟩

theorem SaxlCounterexamples.EveryBase.cq_isSquare (d : ℕ) (a : ↥(Cq d)) : IsSquare ↑↑a

@[simp]

theorem SaxlCounterexamples.EveryBase.cq_smul_eq_mul (d : ℕ) (a : ↥(Cq d)) (x : Fq d) : a • x = ↑↑a * x

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

The nonzero square field elements, represented without quotient choices as the image of Cq.

Equations

• SaxlCounterexamples.EveryBase.cqValueFinset d = Finset.image (fun (a : ↥(SaxlCounterexamples.EveryBase.Cq d)) => ↑↑a) Finset.univ

theorem SaxlCounterexamples.EveryBase.mem_cqValueFinset_iff (d : ℕ) (x : Fq d) : x ∈ cqValueFinset d ↔ ∃ (a : ↥(Cq d)), ↑↑a = x

theorem SaxlCounterexamples.EveryBase.zero_not_mem_cqValueFinset (d : ℕ) : 0 ∉ cqValueFinset d

theorem SaxlCounterexamples.EveryBase.card_cqValueFinset (d : ℕ) : (cqValueFinset d).card = Nat.card ↥(Cq d)

theorem SaxlCounterexamples.EveryBase.odd_card_cqValueFinset (d : ℕ) (hd : Odd d) : Odd (cqValueFinset d).card

noncomputable def SaxlCounterexamples.EveryBase.affineOfSquare (d : ℕ) (b z : Fq d) (hz0 : z ≠ 0) (hz : IsSquare z) : Hq d

The affine map x ↦ b + z*x, with square multiplier z.

Equations

• SaxlCounterexamples.EveryBase.affineOfSquare d b z hz0 hz = ⟨Multiplicative.ofAdd b, SaxlCounterexamples.EveryBase.squareUnit d hz0 hz⟩

theorem SaxlCounterexamples.EveryBase.affineOfSquare_smul (d : ℕ) (b z : Fq d) (hz0 : z ≠ 0) (hz : IsSquare z) (x : Fq d) : affineOfSquare d b z hz0 hz • x = b + z * x

The regular two-point support

noncomputable def SaxlCounterexamples.EveryBase.twoPointVector (d : ℕ) : Fq d → ZMod 2

The characteristic function of the two-point set {0,1}.

Equations

• SaxlCounterexamples.EveryBase.twoPointVector d x = if x = 0 ∨ x = 1 then 1 else 0

@[simp]

theorem SaxlCounterexamples.EveryBase.twoPointVector_zero (d : ℕ) : twoPointVector d 0 = 1

@[simp]

theorem SaxlCounterexamples.EveryBase.twoPointVector_one (d : ℕ) : twoPointVector d 1 = 1

theorem SaxlCounterexamples.EveryBase.twoPointVector_eq_one_iff (d : ℕ) (x : Fq d) : twoPointVector d x = 1 ↔ x = 0 ∨ x = 1

theorem SaxlCounterexamples.EveryBase.twoPointVector_eq_basisSum (d : ℕ) : twoPointVector d = (Pi.basisFun (ZMod 2) (Fq d)) 0 + (Pi.basisFun (ZMod 2) (Fq d)) 1

theorem SaxlCounterexamples.EveryBase.twoPointVector_coordSum (d : ℕ) : ∑ x : Fq d, twoPointVector d x = 0

The two-point characteristic function belongs to the binary deleted permutation module.

theorem SaxlCounterexamples.EveryBase.hq_eq_one_of_twoPointVector_comp_eq (d : ℕ) (hd : Odd d) (g : Hq d) (hfix : ∀ (x : Fq d), twoPointVector d (g • x) = twoPointVector d x) : g = 1

An affine square map preserving {0,1} pointwise as a characteristic function is the identity. The only other possible setwise stabilizer would have multiplier -1, which is not a square when d is odd.

Odd cycles avoiding the distinguished point

theorem SaxlCounterexamples.EveryBase.char_three_add_self (d : ℕ) (x : Fq d) : x + x = -x

theorem SaxlCounterexamples.EveryBase.char_three_neg_sub_self (d : ℕ) (x : Fq d) : -x - x = x

theorem SaxlCounterexamples.EveryBase.cqValueFinset_invariant_of_left_eq_zero (d : ℕ) (g : Hq d) (hgleft : Multiplicative.toAdd g.left = 0) (x : Fq d) : x ∈ cqValueFinset d ↔ g • x ∈ cqValueFinset d

The action of an element of Hq d whose translation part vanishes preserves the odd set of nonzero square field elements.

noncomputable def SaxlCounterexamples.EveryBase.hqAvoidingCycle (d : ℕ) (hd : Odd d) (hd3 : 3 ≤ d) (g : Hq d) : AvoidingCycle (Hq d) (Fq d) g 0

Every affine element has an odd invariant cycle avoiding zero once d ≥ 3. This lower bound is necessary: a nonzero translation is transitive on GF(3) when d = 1.

Equations

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