DeltaSub

formal source

   4namespace LedgerUnits
   5
   6/-- The subgroup of ℤ generated by δ. We specialize to δ = 1 for a clean order isomorphism. -/
   7def DeltaSub (δ : ℤ) := {x : ℤ // ∃ n : ℤ, x = n * δ}
   8
   9/-- Embed ℤ into the δ=1 subgroup. -/
  10def fromZ_one (n : ℤ) : DeltaSub 1 := ⟨n, by exact ⟨n, by simpa using (Int.mul_one n)⟩⟩
  11
  12/-- Project from the δ=1 subgroup back to ℤ by taking its value. -/
  13def toZ_one (p : DeltaSub 1) : ℤ := p.val
  14
  15@[simp] lemma toZ_fromZ_one (n : ℤ) : toZ_one (fromZ_one n) = n := rfl
  16
  17@[simp] lemma fromZ_toZ_one (p : DeltaSub 1) : fromZ_one (toZ_one p) = p := by
  18  cases p with
  19  | mk x hx =>
  20    apply Subtype.ext
  21    rfl
  22
  23/-- Explicit equivalence between the δ=1 subgroup and ℤ (mapping n·1 ↦ n). -/
  24def equiv_delta_one : DeltaSub 1 ≃ ℤ :=
  25{ toFun := toZ_one
  26, invFun := fromZ_one
  27, left_inv := fromZ_toZ_one
  28, right_inv := toZ_fromZ_one }
  29
  30/-! ### General δ ≠ 0: non-canonical equivalence n•δ ↦ n -/
  31
  32noncomputable def fromZ (δ : ℤ) (n : ℤ) : DeltaSub δ := ⟨n * δ, ⟨n, rfl⟩⟩
  33
  34noncomputable def toZ (δ : ℤ) (p : DeltaSub δ) : ℤ :=
  35  Classical.choose p.property
  36
  37lemma toZ_spec (δ : ℤ) (p : DeltaSub δ) : p.val = toZ δ p * δ :=