Affine actions and the regular-difference criterion

This file gives a local affine group whose executable representation is the semidirect product of the additive translation group by a distributive action. It proves the part of paper Lemma 3.1 used by every affine construction.

def Saxl.IsRegularVector (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] (v : V) : Prop

A vector whose stabilizer in the linear group is trivial.

Equations

• Saxl.IsRegularVector H V v = ∀ (h : H), h • v = v → h = 1

def Saxl.regularVectors (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] : Set V

The set of regular vectors for the linear action.

Equations

• Saxl.regularVectors H V = {v : V | Saxl.IsRegularVector H V v}

theorem Saxl.threefold_add_eq_univ_of_card_compl_twofold_lt {A : Type u_3} [AddCommGroup A] [Finite A] (R : Set A) (hcard : (R + R)ᶜ.ncard < R.ncard) : R + R + R = Set.univ

If the complement of the two-fold sumset is smaller than the original set in a finite additive group, then every element is a three-fold sum.

def Saxl.affineLinearAut (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] : H →* MulAut (Multiplicative V)

The action of H on the multiplicative wrapper of the additive group V.

Equations

• Saxl.affineLinearAut H V = (MulAutMultiplicative V).symm.toMonoidHom.comp (DistribMulAction.toAddAut H V)

@[reducible, inline]

abbrev Saxl.AffineGroup (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] : Type (max u_2 u_1)

The affine semidirect product V ⋊ H.

Equations

• Saxl.AffineGroup H V = (Multiplicative V ⋊[Saxl.affineLinearAut H V] H)

@[simp]

theorem Saxl.affineLinearAut_apply (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] (h : H) (v : Multiplicative V) : Multiplicative.toAdd (((affineLinearAut H V) h) v) = h • Multiplicative.toAdd v

@[instance_reducible]

instance Saxl.affineMulAction (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] : MulAction (AffineGroup H V) V

Equations

• Saxl.affineMulAction H V = { smul := fun (g : Saxl.AffineGroup H V) (x : V) => Multiplicative.toAdd g.left + g.right • x, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem Saxl.affine_smul_def (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] (g : AffineGroup H V) (x : V) : g • x = Multiplicative.toAdd g.left + g.right • x

theorem Saxl.affine_isBaseTuple_cons_iff (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] {n : ℕ} (x : V) (w : Fin n → V) : IsBaseTuple (AffineGroup H V) V (Fin.cons x w) ↔ IsBaseTuple H V fun (i : Fin n) => w i - x

After translating the first point to zero, an affine tuple is a base exactly when its difference tuple has trivial kernel in the linear group.

def Saxl.generalizedAffineKernelSet (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] (tail : ℕ) : Set V

The kernel-only neighbourhood of zero for generalized affine adjacency. An element belongs when it can be completed by tail further vectors so that the resulting linear tuple has trivial kernel, while adjoining zero keeps the full affine tuple set-like.

Equations

• Saxl.generalizedAffineKernelSet H V tail = {v : V | ∃ (z : Fin tail → V), Function.Injective (Fin.cons 0 (Fin.cons v z)) ∧ Saxl.IsBaseTuple H V (Fin.cons v z)}

theorem Saxl.generalizedAffineAdjacent_iff_mem_kernelSet (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] (tail : ℕ) (x y : V) : GeneralizedAdjacent (AffineGroup H V) V tail x y ↔ y - x ∈ generalizedAffineKernelSet H V tail

Generalized affine adjacency depends only on the difference of the two displayed vertices, and the condition is entirely a kernel condition for the linear group after translation to zero.

theorem Saxl.generalizedAffine_hasCommonNeighbour_zero_iff (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] (tail : ℕ) (v : V) : HasCommonNeighbour V (GeneralizedAdjacent (AffineGroup H V) V tail) 0 v ↔ ∃ (r₁ : V) (r₂ : V), r₁ ∈ generalizedAffineKernelSet H V tail ∧ r₂ ∈ generalizedAffineKernelSet H V tail ∧ v = r₁ + r₂

The generalized affine common-neighbour criterion: a target is covered precisely by the two-fold sum of the kernel-only zero-neighbourhood.

theorem Saxl.generalizedAffine_hasCommonNeighbour_zero_iff_mem_add (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] (tail : ℕ) (v : V) : HasCommonNeighbour V (GeneralizedAdjacent (AffineGroup H V) V tail) 0 v ↔ v ∈ generalizedAffineKernelSet H V tail + generalizedAffineKernelSet H V tail

Pointwise-set form of the generalized affine sumset criterion.

theorem Saxl.affine_pairBase_iff_regular_sub (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] (x y : V) : Adjacent (AffineGroup H V) V x y ↔ IsRegularVector H V (y - x)

Translation reduces an affine ordered pair to a regular difference.

theorem Saxl.isRegularVector_ne_zero (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] [Nontrivial H] {v : V} (hv : IsRegularVector H V v) : v ≠ 0

A regular vector is nonzero when the linear group is nontrivial.

theorem Saxl.affine_exactBaseSize_two (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] [Nontrivial H] (hregular : ∃ (v : V), IsRegularVector H V v) : ExactBaseSize (AffineGroup H V) V 2

A nontrivial affine action has exact base size two as soon as its linear group has a regular vector.

theorem Saxl.generalizedAffineKernelSet_zero (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] [Nontrivial H] : generalizedAffineKernelSet H V 0 = regularVectors H V

At generalized tail zero, the kernel-only zero-neighbourhood is exactly the ordinary regular-vector set (for a nontrivial linear group).

theorem Saxl.generalizedAffineAdjacent_zero_iff_adjacent (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] [Nontrivial H] (x y : V) : GeneralizedAdjacent (AffineGroup H V) V 0 x y ↔ Adjacent (AffineGroup H V) V x y

For a nontrivial affine linear group, generalized adjacency at exact base-size parameter two (tail = 0) recovers ordinary Saxl adjacency.

theorem Saxl.affine_hasCommonNeighbour_zero_iff (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] (v : V) : HasCommonNeighbour V (Adjacent (AffineGroup H V) V) 0 v ↔ ∃ (r₁ : V) (r₂ : V), IsRegularVector H V r₁ ∧ IsRegularVector H V r₂ ∧ v = r₁ + r₂

The affine common-neighbour criterion in sumset form.

theorem Saxl.affine_hasCommonNeighbour_zero_iff_mem_add (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] (v : V) : HasCommonNeighbour V (Adjacent (AffineGroup H V) V) 0 v ↔ v ∈ regularVectors H V + regularVectors H V

Pointwise-set form of the ordinary affine sumset criterion.

theorem Saxl.affine_core_counterexample (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] (v : V) (hbase : ∃ (r : V), IsRegularVector H V r) (hv : ¬IsRegularVector H V v) (hsum : ∀ (x : V), ¬IsRegularVector H V x ∨ ¬IsRegularVector H V (v - x)) : (∃ (x : V) (y : V), Adjacent (AffineGroup H V) V x y) ∧ ¬Adjacent (AffineGroup H V) V 0 v ∧ ¬HasCommonNeighbour V (Adjacent (AffineGroup H V) V) 0 v

A direct obstruction theorem for affine common neighbours.

theorem Saxl.affine_faithful_of_linear_faithful (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] [FaithfulSMul H V] : FaithfulSMul (AffineGroup H V) V

If the linear action is faithful, then the induced affine action is faithful.

theorem Saxl.affine_primitive_of_irreducible (H : Type u_1) (V : Type u_2) [Group H] [AddCommGroup V] [DistribMulAction H V] (p : ℕ) [Fact (Nat.Prime p)] [Module (ZMod p) V] [SMulCommClass H (ZMod p) V] [(Representation.ofDistribMulAction (ZMod p) H V).IsIrreducible] : MulAction.IsPreprimitive (AffineGroup H V) V

An irreducible linear group over a prime field has a preprimitive affine action.