Multiplication on the one-point extension of ZMod p

TauCeti.mulModEquiv (Data/ZMod/FinEquiv.lean) is multiplication by a unit as a permutation of the residues themselves. This file is its companion on the one-point extension: multiplication by a d coprime to p, acting on OnePoint (ZMod p) and fixing ∞.

p is unrestricted here, so OnePoint (ZMod p) is only the affine line with a point adjoined. It is the projective line exactly when p is prime: for composite p the projective line over ZMod p is larger, carrying p * ∏ (1 + 1 / ℓ) points over the primes ℓ ∣ p rather than p + 1. Nothing below needs the identification, so nothing below assumes p prime.

Main results

• TauCeti.onePointMulPerm: multiplication by d as a permutation of OnePoint (ZMod p).
• TauCeti.onePointMulPerm_coe and TauCeti.onePointMulPerm_infty: its two evaluation rules, on an affine point and at ∞. The first explicit argument is a modulus, not a ZMod value, so these are not dot notation on ZMod and live in TauCeti.

def TauCeti.onePointMulPerm (p : ℕ) {d : ℕ} (hdp : d.Coprime p) : Equiv.Perm (OnePoint (ZMod p))

Multiplication by d on the one-point extension of ZMod p, fixing ∞. The companion of TauCeti.mulModEquiv: d coprime to p is a unit, so multiplying by it permutes the residues, and the permutation is extended by fixing the adjoined point.

Equations

• TauCeti.onePointMulPerm p hdp = Equiv.optionCongr (ZMod.unitOfCoprime d hdp).mulLeft

@[simp]

theorem TauCeti.onePointMulPerm_coe (p : ℕ) {d : ℕ} (hdp : d.Coprime p) (x : ZMod p) : (onePointMulPerm p hdp) ↑x = ↑(↑d * x)

The value of TauCeti.onePointMulPerm at an affine point: it multiplies by d.

@[simp]

theorem TauCeti.onePointMulPerm_infty (p : ℕ) {d : ℕ} (hdp : d.Coprime p) : (onePointMulPerm p hdp) OnePoint.infty = OnePoint.infty

TauCeti.onePointMulPerm fixes the point at infinity.