The Margulis generators

The Margulis–Gabber–Galil graph on ZMod m × ZMod m is eight-regular: a vertex (x, y) is joined to the images of eight explicit affine maps. The maps come in four inverse pairs, which is what makes the rotation map an involution — the edge leaving by generator i arrives by its partner.

This module sets up the generators and that pairing. The spectral bound is elsewhere.

Main definitions

• Complexity.margGen — the eight generators
• Complexity.margPair — the pairing of a generator with its inverse
• Complexity.margEquiv — Fin (m * m) as ZMod m × ZMod m
• Complexity.margRot — the resulting rotation map

Main results

• Complexity.margGen_pair — partnered generators undo each other
• Complexity.margRot_involutive — the rotation map is an involution

def Complexity.margGen {m : ℕ} (i : Fin 8) (v : ZMod m × ZMod m) : ZMod m × ZMod m

The eight Margulis generators of ZMod m × ZMod m.

Equations

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

def Complexity.margPair (i : Fin 8) : Fin 8

The generator that undoes a given one.

Equations

• Complexity.margPair i = ![1, 0, 3, 2, 5, 4, 7, 6] i

@[simp]

theorem Complexity.margPair_pair (i : Fin 8) : margPair (margPair i) = i

theorem Complexity.margGen_pair {m : ℕ} (i : Fin 8) (v : ZMod m × ZMod m) : margGen (margPair i) (margGen i v) = v

Partnered generators undo each other.

The rotation map

def Complexity.margEquiv (m : ℕ) [NeZero m] : Fin (m * m) ≃ ZMod m × ZMod m

Fin (m * m) viewed as the group ZMod m × ZMod m.

Equations

• Complexity.margEquiv m = finProdFinEquiv.symm.trans ((ZMod.finEquiv m).prodCongr (ZMod.finEquiv m).toEquiv)

def Complexity.margRot (m : ℕ) (p : Fin (m * m) × Fin 8) : Fin (m * m) × Fin 8

The Margulis rotation map: leave by generator i, arrive by its partner. On the empty vertex set (m = 0) it is the identity.

Equations

• Complexity.margRot m p = if h : m = 0 then p else ((Complexity.margEquiv m).symm (Complexity.margGen p.2 ((Complexity.margEquiv m) p.1)), Complexity.margPair p.2)

theorem Complexity.margRot_involutive (m : ℕ) : Function.Involutive (margRot m)

The Margulis rotation map is an involution.