toZ_spec

formal source

  34noncomputable def toZ (δ : ℤ) (p : DeltaSub δ) : ℤ :=
  35  Classical.choose p.property
  36
  37lemma toZ_spec (δ : ℤ) (p : DeltaSub δ) : p.val = toZ δ p * δ :=
  38  Classical.choose_spec p.property
  39
  40lemma rep_unique {δ n m : ℤ} (hδ : δ ≠ 0) (h : n * δ = m * δ) : n = m := by
  41  have h' : (n - m) * δ = 0 := by
  42    calc
  43      (n - m) * δ = n * δ - m * δ := by simpa using sub_mul n m δ
  44      _ = 0 := by simpa [h]
  45  have hnm : n - m = 0 := by
  46    have : n - m = 0 ∨ δ = 0 := by
  47      simpa using (mul_eq_zero.mp h')
  48    cases this with
  49    | inl h0 => exact h0
  50    | inr h0 => exact (hδ h0).elim
  51  exact sub_eq_zero.mp hnm
  52
  53@[simp] lemma toZ_fromZ (δ : ℤ) (hδ : δ ≠ 0) (n : ℤ) : toZ δ (fromZ δ n) = n := by
  54  have hval : (fromZ δ n).val = n * δ := rfl
  55  let k := toZ δ (fromZ δ n)
  56  have hk : (fromZ δ n).val = k * δ := toZ_spec δ (fromZ δ n)
  57  have h_eq : n = k := rep_unique (δ:=δ) hδ (by simpa [hval] using hk)
  58  simpa [k, h_eq.symm]
  59
  60@[simp] lemma fromZ_toZ (δ : ℤ) (p : DeltaSub δ) : fromZ δ (toZ δ p) = p := by
  61  apply Subtype.ext
  62  simpa [fromZ, toZ_spec δ p]
  63
  64/-- One δ-step corresponds to adding 1 on coefficients via `toZ`. -/
  65@[simp] lemma toZ_succ (δ : ℤ) (hδ : δ ≠ 0) (n : ℤ) :
  66  toZ δ (fromZ δ (n + 1)) = toZ δ (fromZ δ n) + 1 := by
  67  simp [toZ_fromZ δ hδ]