AffineFibers.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Nonidentity affine-map fibers

The finite-field representation count used immediately before equation tree-affine-coefficient-norm: every nonidentity affine map arising from U_r^* U_s has at most two representations.

def OAI.Ostmann.affineParameters line 17
Source documentation
Slope and translation of the affine map underlying U_r^* U_s. The translation is written in ratio coordinates.
```
def affineParameters {p : ℕ} (r s : (ZMod p)ˣ) : (ZMod p)ˣ × ZMod p :=
…
```
theorem OAI.Ostmann.affineParameters_translation line 22
Source documentation
The ratio-coordinate translation equals the manuscript's s - s²/r.
```
theorem affineParameters_translation {p : ℕ} [Fact p.Prime] (r s : (ZMod p)ˣ) :
    (affineParameters r s).2 = (s : ZMod p) - (s : ZMod p) ^ 2 / (r : ZMod p) := by
…
```
Mentions: OAI.Ostmann.affineParameters
theorem OAI.Ostmann.sub_sq_ne_zero line 27
theorem OAI.Ostmann.ratio_ne_one_of_nonidentity line 38

theorem OAI.Ostmann.affineParameters_ratio_injective line 46

Source documentation

The ratio determines both unit parameters once a nonidentity affine map has been fixed.

theorem affineParameters_ratio_injective {p : ℕ} [Fact p.Prime]
    {r s r' s' : (ZMod p)ˣ}
    (hnon : affineParameters r s ≠ (1, 0))
    (hmap : affineParameters r s = affineParameters r' s')
    (hratio : s / r = s' / r') : r = r' ∧ s = s' := by
…

Mentions: OAI.Ostmann.affineParameters

theorem OAI.Ostmann.affineParameters_fiber_card_le_two line 66

Source documentation

Every nonidentity affine map has at most two ordered unit representations.

theorem affineParameters_fiber_card_le_two {p : ℕ} [Fact p.Prime]
    (a : (ZMod p)ˣ) (b : ZMod p) (hnon : (a, b) ≠ (1, 0)) :
    ((Finset.univ : Finset ((ZMod p)ˣ × (ZMod p)ˣ)).filter
      (fun rs => affineParameters rs.1 rs.2 = (a, b))).card ≤ 2 := by
…

Mentions: OAI.Ostmann.affineParameters