DeltaSub

formal source

 109namespace LedgerUnits
 110
 111/-- The subgroup of ℤ generated by δ. We specialize to δ = 1 for a clean order isomorphism. -/
 112def DeltaSub (δ : ℤ) := {x : ℤ // ∃ n : ℤ, x = n * δ}
 113
 114/-- Embed ℤ into the δ=1 subgroup. -/
 115def fromZ_one (n : ℤ) : DeltaSub 1 := ⟨n, by exact ⟨n, by simpa using (Int.mul_one n)⟩⟩
 116
 117/-- Project from the δ=1 subgroup back to ℤ by taking its value. -/
 118def toZ_one (p : DeltaSub 1) : ℤ := p.val
 119
 120@[simp] lemma toZ_fromZ_one (n : ℤ) : toZ_one (fromZ_one n) = n := rfl
 121
 122@[simp] lemma fromZ_toZ_one (p : DeltaSub 1) : fromZ_one (toZ_one p) = p := by
 123  cases p with
 124  | mk x hx =>
 125    apply Subtype.ext
 126    rfl
 127
 128/-- Explicit equivalence between the δ=1 subgroup and ℤ (mapping n·1 ↦ n). -/
 129def equiv_delta_one : DeltaSub 1 ≃ ℤ :=
 130{ toFun := toZ_one
 131, invFun := fromZ_one
 132, left_inv := fromZ_toZ_one
 133, right_inv := toZ_fromZ_one }
 134
 135end LedgerUnits
 136
 137/-! Affine maps for unit-to-scale projections -/
 138namespace Scales
 139
 140/-- Affine map from ℤ to ℝ: n ↦ slope·n + offset. -/
 141structure AffineMapZ where
 142  slope : ℝ