Ico_map_valMinAbs_natAbs_eq_Ico_map_id

English

For a prime p and a nonzero a ∈ Z/pZ, the map x ↦ (a·x).valMinAbs.natAbs on the interval Ico(1, p/2).succ has the same image as the identity map on that interval; i.e., it permutes the same set of representatives.

Русский

Пусть p — простое, a ≠ 0 в ZMod p. Отображение x ↦ (a·x) mod p, взятое через нормализованные представления, образует перестановку множества {1, ..., ⌊p/2⌋}.

LaTeX

$$$((Ico\ 1\ (p/2).succ).1.map (\x => (a * x).valMinAbs.natAbs)) = ((Ico\ 1\ (p/2).succ).1.map (\a => a))$$$

Lean4

/-- The image of the map sending a nonzero natural number `x ≤ p / 2` to the absolute value
  of the integer in `(-p/2, p/2]` that is congruent to `a * x mod p` is the set
  of nonzero natural numbers `x` such that `x ≤ p / 2`. -/
theorem Ico_map_valMinAbs_natAbs_eq_Ico_map_id (p : ℕ) [hp : Fact p.Prime] (a : ZMod p) (hap : a ≠ 0) :
    ((Ico 1 (p / 2).succ).1.map fun (x : ℕ) => (a * x).valMinAbs.natAbs) = (Ico 1 (p / 2).succ).1.map fun a => a :=
  by
  have he : ∀ {x}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2 := by
    simp +contextual [Nat.lt_succ_iff, Nat.succ_le_iff, pos_iff_ne_zero]
  have hep : ∀ {x}, x ∈ Ico 1 (p / 2).succ → x < p := fun hx =>
    lt_of_le_of_lt (he hx).2 (Nat.div_lt_self hp.1.pos (by decide))
  have hpe : ∀ {x}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x := fun hx hpx =>
    not_lt_of_ge (le_of_dvd (Nat.pos_of_ne_zero (he hx).1) hpx) (hep hx)
  have hmem : ∀ (x : ℕ) (_ : x ∈ Ico 1 (p / 2).succ), (a * x : ZMod p).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ :=
    by
    intro x hx
    simp [hap, CharP.cast_eq_zero_iff (ZMod p) p, hpe hx, Nat.lt_succ_iff, succ_le_iff, pos_iff_ne_zero,
      natAbs_valMinAbs_le _]
  have hsurj :
    ∀ (b : ℕ) (hb : b ∈ Ico 1 (p / 2).succ), ∃ x, ∃ _ : x ∈ Ico 1 (p / 2).succ, (a * x : ZMod p).valMinAbs.natAbs = b :=
    by
    intro b hb
    refine ⟨(b / a : ZMod p).valMinAbs.natAbs, mem_Ico.mpr ⟨?_, ?_⟩, ?_⟩
    · apply Nat.pos_of_ne_zero
      simp only [div_eq_mul_inv, hap, CharP.cast_eq_zero_iff (ZMod p) p, hpe hb, not_false_iff, valMinAbs_eq_zero,
        inv_eq_zero, Int.natAbs_eq_zero, Ne, _root_.mul_eq_zero, or_self_iff]
    · apply lt_succ_of_le; apply natAbs_valMinAbs_le
    · rw [natCast_natAbs_valMinAbs]
      split_ifs
      ·
        rw [mul_div_cancel₀ _ hap, valMinAbs_def_pos, val_cast_of_lt (hep hb), if_pos (le_of_lt_succ (mem_Ico.1 hb).2),
          Int.natAbs_natCast]
      ·
        rw [mul_neg, mul_div_cancel₀ _ hap, natAbs_valMinAbs_neg, valMinAbs_def_pos, val_cast_of_lt (hep hb),
          if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_natCast]
  exact
    Multiset.map_eq_map_of_bij_of_nodup _ _ (Finset.nodup _) (Finset.nodup _)
      (fun x _ => (a * x : ZMod p).valMinAbs.natAbs) hmem (inj_on_of_surj_on_of_card_le _ hmem hsurj le_rfl) hsurj
      (fun _ _ => rfl)

Похожие утверждения